NF … (RR L) RS T → NF … (RR L0) RS T0.
definition CP3 ≝ λRP:lenv→predicate term.
- ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
+ ∀L,T,k. RP L (ⓐ⋆k.T) → RP L T.
+
+definition CP4 ≝ λRP:lenv→predicate term.
+ ∀L,W,T. RP L W → RP L T → RP L (ⓝW.T).
(* requirements for abstract computation properties *)
record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝
{ cp1: CP1 RR RS;
cp2: CP2 RR RS;
- cp3: CP3 RP
+ cp3: CP3 RP;
+ cp4: CP4 RP
}.
(* Basic properties *********************************************************)
elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
@(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *)
| -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
- #K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct
+ #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
- >(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B
+ lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
+ elim (lift_total V0 0 (i0 +1)) #V3 #HV03
elim (lift_total V2 0 (i0 +1)) #V #HV2
- @(s5 … HB … ◊ … HV2 HLK2)
- @(s8 … HB … HKV2B) //
+ @(s5 … HB … ◊ … (ⓝV3.V) … HLK2) [2: /2 width=1/ ]
+ @(s7 … HB … ◊) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ]
]
| #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
@(s6 … HA … ◊ ◊) // /3 width=5/
| #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
- @(aacr_abst … H1RP H2RP)
- [ lapply (aacr_acr … H1RP H2RP B) #HB
- @(s1 … HB) /2 width=5/
- | -IHB
- #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
- elim (lifts_total des3 W0) #W2 #HW02
- elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W2 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
- @(IHA (L2. ⓛW2) … (des + 1 @@ des3 + 1)) -IHA
- /2 width=3/ /3 width=5/
- ]
+ @(aacr_abst … H1RP H2RP) [ /2 width=5/ ]
+ #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
+ elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
+ lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
+ @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5/
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
/3 width=10/
| #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
- elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+ elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
- lapply (s1 … HA) #H
- @(s7 … HA … ◊) /2 width=5/ /3 width=5/
+ @(s7 … HA … ◊) /2 width=5/
]
qed.
∀L,Vs. all … (RP L) Vs →
∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
-(* Note: this is Tait's ii *)
-definition S3 ≝ λRP,C:lenv→predicate term.
- ∀a,L,Vs,V,T,W. C L (ⒶVs. ⓓ{a}V. T) → RP L W → C L (ⒶVs. ⓐV. ⓛ{a}W. T).
+(* Note: this generalizes Tait's ii *)
+definition S3 ≝ λC:lenv→predicate term.
+ ∀a,L,Vs,V,T,W. C L (ⒶVs.ⓓ{a}ⓝW.V.T) → C L (ⒶVs.ⓐV.ⓛ{a}W.T).
definition S4 ≝ λRP,C:lenv→predicate term.
∀L,Vs. all … (RP L) Vs → ∀k. C L (ⒶVs.⋆k).
-definition S5 ≝ λRP,C:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i.
- C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 →
- ⇩[0, i] L ≡ K. ⓑ{I}V1 → C L (Ⓐ Vs. #i).
+definition S5 ≝ λC:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i.
+ C L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 →
+ ⇩[0, i] L ≡ K.ⓑ{I}V1 → C L (Ⓐ Vs.#i).
definition S6 ≝ λRP,C:lenv→predicate term.
∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀a,V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓ{a}V. T).
+ ∀a,V,T. C (L.ⓓV) (ⒶV2s.T) → RP L V → C L (ⒶV1s.ⓓ{a}V.T).
-definition S7 ≝ λRP,C:lenv→predicate term.
- ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T).
+definition S7 ≝ λC:lenv→predicate term.
+ ∀L,Vs,T,W. C L (ⒶVs.T) → C L (ⒶVs.W) → C L (ⒶVs.ⓝW.T).
definition S8 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝
{ s1: S1 RP C;
s2: S2 RR RS RP C;
- s3: S3 RP C;
+ s3: S3 C;
s4: S4 RP C;
- s5: S5 RP C;
+ s5: S5 C;
s6: S6 RP C;
- s7: S7 RP C;
+ s7: S7 C;
s8: S8 C
}.
λT. match A with
[ AAtom ⇒ RP L T
| APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
- aacr RP A L0 (ⓐV0. T0)
+ aacr RP A L0 (ⓐV0.T0)
].
interpretation
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
@(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
-| #a #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
+| #a #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
- @(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+ @(s3 … IHA … (V0 @ V0s)) /5 width=5/
| #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
>(lifts_inv_sort1 … HY) -Y
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
- @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/
+ @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /3 width=6 by rp_lifts/
@(HA … (des + 1)) /2 width=1/
[ @(s8 … IHB … HB … HV120) /2 width=1/
| @lifts_applv //
| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s7 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/
+ @(s7 … IHA … (V0 @ V0s)) /3 width=4/
| /3 width=7/
]
qed.
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀a,L,W,T,A,B. RP L W → (
- ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
- ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛
+ ∀a,L,W,T,A,B. ⦃L, W⦄ ϵ[RP] 〚B〛 → (
+ ∀L0,V0,W0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
+ ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0, W0⦄ ϵ[RP] 〚B〛 → ⦃L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
) →
- ⦃L, ⓛ{a}W. T⦄ ϵ[RP] 〚②B. A〛.
+ ⦃L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
#RR #RS #RP #H1RP #H2RP #a #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
lapply (aacr_acr … H1RP H2RP A) #HCA
lapply (aacr_acr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-lapply (s1 … HCB) -HCB #HCB
-@(s3 … HCA … ◊) /2 width=6 by rp_lifts/
-@(s6 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
+lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s8 … HCB) ] #HW0
+@(s3 … HCA … ◊)
+@(s6 … HCA … ◊ ◊) //
+[ @(HA … HL0) //
+| lapply (s1 … HCB) -HCB #HCB
+ @(cp4 … H1RP) /2 width=1/
+]
qed.
(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/csn.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
-
-definition cpe: lenv → relation term ≝
- λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄.
-
-interpretation "context-sensitive parallel evaluation (term)"
- 'PEval L T1 T2 = (cpe L T1 T2).
-
-(* Basic_properties *********************************************************)
-
-(* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: ∀L,T1. L ⊢ ⬊* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
-#L #T1 #H @(csn_ind … H) -T1
-#T1 #_ #IHT1
-elim (cnf_dec L T1) /3 width=3/
-* #T #H1T1 #H2T1
-elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/cpe.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
-
-(* Main properties *********************************************************)
-
-(* Basic_1: was: nf2_pr3_confluence *)
-theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
-#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
-elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
->(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2
->(cprs_inv_cnf1 … HT2 H2T2) -T2 //
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
+
+definition cpre: lenv → relation term ≝
+ λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄.
+
+interpretation "context-sensitive parallel evaluation (term)"
+ 'PEval L T1 T2 = (cpre L T1 T2).
+
+(* Basic_properties *********************************************************)
+
+(* Basic_1: was just: nf2_sn3 *)
+axiom csn_cpre: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
+(*
+#h #g #L #T1 #H @(csn_ind … H) -T1
+#T1 #_ #IHT1
+elim (cnr_dec L T1) /3 width=3/
+* #T #H1T1 #H2T1
+elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
+qed.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/cpre.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
+
+(* Main properties *********************************************************)
+
+(* Basic_1: was: nf2_pr3_confluence *)
+theorem cpre_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
+#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
+elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
+>(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2
+>(cprs_inv_cnr1 … HT2 H2T2) -T2 //
+qed-.
lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
/3 width=3/ qed-.
-lemma cprs_lsubr_trans: lsubr_trans … cprs.
-/3 width=3 by cpr_lsubr_trans, TC_lsubr_trans/
+lemma cprs_lsubr_trans: lsub_trans … cprs lsubr.
+/3 width=5 by cpr_lsubr_trans, TC_lsub_trans/
qed-.
(* Basic_1: was: pr3_pr1 *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/cpxs.ma".
+include "basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************)
+
+definition cpxe: ∀h. sd h → lenv → relation term ≝
+ λh,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 ∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃T2⦄.
+
+interpretation "context-sensitive extended parallel evaluation (term)"
+ 'PEval h g L T1 T2 = (cpxe h g L T1 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma csn_cpxe: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 → ∃T2. ⦃h, L⦄ ⊢ T1 ➡*[g] 𝐍⦃T2⦄.
+#h #g #L #T1 #H @(csn_ind … H) -T1
+#T1 #_ #IHT1
+elim (cnx_dec h g L T1) /3 width=3/
+* #T #H1T1 #H2T1
+elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
+qed-.
∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
normalize /2 width=3/ qed.
-lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+lemma lsubx_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubx.
+/3 width=5 by lsubx_cpx_trans, TC_lsub_trans/
+qed-.
+
+axiom cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+(*
#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
qed.
-
+*)
lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 →
∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
#h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
qed.
-lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W,T1,T2.
- ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 →
- ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2.
-#h #g #a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/
-/4 width=6 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *)
+lemma cpxs_ti: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 → ∀T. ⦃h, L⦄ ⊢ ⓝV1.T ➡*[g] V2.
+#h #g #L #V1 #V2 #H elim H -V2 /2 width=3/ /3 width=1/
+qed.
+
+lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
+ ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡[g] W2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2.
+#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /3 width=1/
+/4 width=7 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *)
qed.
lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
elim (cpx_inv_sort1 … HU2) -HU2
[ #H destruct /2 width=4/
| * #l0 #Hkl0 #H destruct -l
- @(ex2_2_intro … (n+1) l0) /2 width=1/ >iter_SO //
- ]
-]
-qed-.
-
-lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 →
- ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 &
- U2 = ⓐV2. T2
- | ∃∃a,V2,W,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 &
- ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}V2.T ➡*[g] U2
- | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 &
- ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2.
-#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
-#U #U2 #_ #HU2 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpx_inv_appl1 … HU2) -HU2 *
- [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
- | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
- lapply (cpxs_strap1 … HV10 … HV02) -V0 /5 width=7/
- | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
- @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ @(ex2_2_intro … (n+1) l0) /2 width=1 by deg_inv_prec/ >iter_SO //
]
-| /4 width=9/
-| /4 width=11/
]
qed-.
-lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → ⦃h, L⦄ ⊢ T1 ➡*[g] U2 ∨
- ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2.
+lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 →
+ ∨∨ ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2
+ | ⦃h, L⦄ ⊢ T1 ➡*[g] U2
+ | ⦃h, L⦄ ⊢ W1 ➡*[g] U2.
#h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
#U2 #U #_ #HU2 * /3 width=3/ *
#W #T #HW1 #HT1 #H destruct
elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ *
-#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+#W2 #T2 #HW2 #HT2 #H destruct
+lapply (cpxs_strap1 … HW1 … HW2) -W
+lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5/
qed-.
lemma cpxs_inv_cnx1: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T ➡*[g] U → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → T = U.
@(cpxs_trans … IHV1) -IHV1 /2 width=1/
qed.
-theorem cpxs_beta: ∀h,g,a,L,V1,V2,W,T1,T2.
- ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
- ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2.
-#h #g #a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+theorem cpxs_beta_rc: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
+ ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2.
+#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/
+#W #W2 #_ #HW2 #IHW1
+@(cpxs_trans … IHW1) -IHW1 /3 width=1/
+qed.
+
+theorem cpxs_beta: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
+ ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2.
+#h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
-@(cpxs_trans … IHV1) /2 width=1/
+@(cpxs_trans … IHV1) -IHV1 /3 width=1/
qed.
theorem cpxs_theta_rc: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 →
- ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
- ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+ ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
#W #W2 #_ #HW2 #IHW1
-@(cpxs_trans … IHW1) /2 width=1/
+@(cpxs_trans … IHW1) -IHW1 /2 width=1/
qed.
theorem cpxs_theta: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
⇧[0, 1] V ≡ V2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
- ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V →
- ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+ ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
#V1 #V0 #HV10 #_ #IHV0
-@(cpxs_trans … IHV0) /2 width=1/
+@(cpxs_trans … IHV0) -IHV0 /2 width=1/
qed.
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,W,T. ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡*[g] U2
+ | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 &
+ ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2.
+#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpx_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
+ lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12
+ lapply (lsubx_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
+ @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ ]
+| /4 width=9/
+| /4 width=11/
+]
+qed-.
+
(* Properties on sn extended parallel reduction for local environments ******)
lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g).
lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/
| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
-|5,7: /3 width=1/
+|5,7,8: /3 width=1/
| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
-| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
- lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/
+| #a #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓛW1) ?) -IHT12 /2 width=1/ /3 width=1/
| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
]
>(cpxs_inv_cnx1 … H HT) -L -T //
qed-.
+lemma cpxs_fwd_sort: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U →
+ ⋆k ≃ U ∨ ⦃h, L⦄ ⊢ ⋆(next h k) ➡*[g] U.
+#h #g #L #U #k #H
+elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n
+[ #k #_ #H -l destruct /2 width=1/
+| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct
+ lapply (deg_next_SO … Hnl) -Hnl #Hnl
+ elim (IHn … Hnl) -IHn
+ [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1/
+ | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n /2 width=1/
+ #n #_ /4 width=3/
+ | >iter_SO >iter_n_Sm //
+ ]
+]
+qed-.
+
(* Basic_1: was just: pr3_iso_beta *)
lemma cpxs_fwd_beta: ∀h,g,a,L,V,W,T,U. ⦃h, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[g] U →
- ⓐV.ⓛ{a}W.T ≃ U ∨
- ∃∃T0. ⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⓓ{a}V.T0 ➡*[g] U.
+ ⓐV.ⓛ{a}W.T ≃ U ∨ ⦃h, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[g] U.
#h #g #a #L #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
- elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1
- @or_intror @(ex2_intro … HT1) -W (**) (* explicit constructors *)
- @(cpxs_trans … HU) -U /2 width=1/
+| #b #W0 #T0 #HT0 #HU
+ elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
+ lapply (lsubx_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
+ @or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
]
#h #g #a #L #V1 #V #T #U #H #V2 #HV12
elim (cpxs_inv_appl1 … H) -H *
[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W #T0 #HV10 #HT0 #HU
+| #b #W #T0 #HT0 #HU
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V3 #T3 #_ #_ #H destruct
| #X #HT2 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
@(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2
- @(cpxs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/
+ @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1/ ]
+ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (**) (* auto too slow without trace *)
]
| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
@(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 (**) (* auto too slow without trace *)
@(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
]
]
qed-.
-lemma cpxs_fwd_tau: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U →
- ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ T ➡*[g] U.
+lemma cpxs_fwd_cast: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U →
+ ∨∨ ⓝW. T ≃ U | ⦃h, L⦄ ⊢ T ➡*[g] U | ⦃h, L⦄ ⊢ W ➡*[g] U.
#h #g #L #W #T #U #H
elim (cpxs_inv_cast1 … H) -H /2 width=1/ *
#W0 #T0 #_ #_ #H destruct /2 width=1/
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #a #V0 #W0 #T0 #HV0 #HT0 #HU
+| #a #W0 #T0 #HT0 #HU
lapply (IHVs … HT0) -IHVs -HT0 #HT0
elim (tstc_inv_bind_appls_simple … HT0) //
| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
]
qed-.
+lemma cpxs_fwd_sort_vector: ∀h,g,L,k,Vs,U. ⦃h, L⦄ ⊢ ⒶVs.⋆k ➡*[g] U →
+ ⒶVs.⋆k ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[g] U.
+#h #g #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
+#V #Vs #IHVs #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
+| #a #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tstc_inv_bind_appls_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) [ /2 width=1/ ] -Vs /3 width=1/
+ ]
+| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tstc_inv_bind_appls_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) [ /2 width=1/ ] -Vs /3 width=3/
+ ]
+]
+qed-.
+
+
(* Basic_1: was just: pr3_iso_appls_beta *)
lemma cpxs_fwd_beta_vector: ∀h,g,a,L,Vs,V,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[g] U →
- ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨
- ∃∃T0.⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}V.T0 ➡*[g] U.
+ ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[g] U.
#h #g #a #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
#V0 #Vs #IHVs #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
-| #b #V1 #W1 #T1 #HV01 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1
- [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) //
- | * #T0 #HT0 #HT01
- @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *)
+| #b #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tstc_inv_bind_appls_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/
+ @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -Vs -T /3 width=1/
]
| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1
- [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) //
- | * #T0 #HT0 #HT01
- @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *)
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tstc_inv_bind_appls_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
@(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/
]
#V #Vs #IHVs #U #H -K -V1
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
+| #b #W0 #T0 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
| @or_intror -i (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V2 -Vs /3 width=1/
]
| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0a #W0 #T0 #HV10a #HT0 #HU
+| #b #W0 #T0 #HT0 #HU
elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
- [ -HV12a -HV12b -HV10a -HU
+ [ -HV12a -HV12b -HU
elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
| @or_intror -V1s (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
elim (cpxs_inv_abbr1 … HT0) -HT0 *
- [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct
+ [ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct
| -V1b #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
@(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1
- @(cpxs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/
+ @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [2: /2 width=1/ ]
+ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (* auto too slow without trace *)
]
]
| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
lapply (cpxs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a
@(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1
+ @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 (* auto too slow without trace *)
@(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
]
]
qed-.
(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_tau_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U →
- ⒶVs. ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U.
-#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_tau/
+lemma cpxs_fwd_cast_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U →
+ ∨∨ ⒶVs. ⓝW. T ≃ U
+ | ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U
+ | ⦃h, L⦄ ⊢ ⒶVs.W ➡*[g] U.
+#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
#V #Vs #IHVs #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
+| #b #W0 #T0 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
- | @or_intror -W (**) (* explicit constructor *)
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/
+ | @or3_intro2 -T (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/
]
| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
- | @or_intror -W (**) (* explicit constructor *)
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /2 width=3/
+ | @or3_intro2 -T (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/
]
]
qed-.
⦃h, L⦄ ⊢ ⬊*[g] T1.
/4 width=1/ qed.
-(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T.
-/2 width=1/ qed.
-
lemma csn_cpx_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2.
#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
| -HT1 -HT2 /3 width=4/
qed-.
+(* Basic_1: was just: sn3_nf2 *)
+lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T.
+/2 width=1/ qed.
+
+lemma cnx_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ ⬊*[g] ⋆k.
+#h #g #L #k elim (deg_total h g k)
+#l generalize in match k; -k @(nat_ind_plus … l) -l /3 width=1/
+#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
+#Hkl @csn_intro #X #H #HX elim (cpx_inv_sort1 … H) -H
+[ #H destruct elim HX //
+| -HX * #l0 #_ #H destruct -l0 /2 width=1/
+]
+qed.
+
(* Basic_1: was just: sn3_cast *)
lemma csn_cast: ∀h,g,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W →
∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓝW.T.
-#h #g #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
+#h #g #L #W #HW @(csn_ind … HW) -W #W #HW #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpx_inv_cast1 … H1) -H1
[ * #W0 #T0 #HLW0 #HLT0 #H destruct
[ /3 width=3 by csn_cpx_trans/
| -HLW0 * #H destruct /3 width=1/
]
-| /3 width=3 by csn_cpx_trans/
+|2,3: /3 width=3 by csn_cpx_trans/
]
qed.
include "basic_2/computation/acp_aaa.ma".
include "basic_2/computation/csn_tstc_vector.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* Main properties concerning atomic arity assignment ***********************)
-theorem csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T.
-#L #T #A #H
-@(acp_aaa … csn_acp csn_acr … H)
+theorem csn_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ⦃h, L⦄ ⊢ ⬊*[g] T.
+#h #g #L #T #A #H
+@(acp_aaa … (csn_acp h g) (csn_acr h g) … H)
qed.
#l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/
| @cnx_lift
| /2 width=3 by csn_fwd_flat_dx/
+| /2 width=1/
]
qed.
]
qed.
-fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 → ∀V. ⦃h, L⦄ ⊢ ⬊*[g] V →
- ∀W,T1. U1 = ⓛ{a}W.T1 → (
- ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2
- ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #L #X1 #H @(csn_ind … H) -X1
-#X1 #HT1 #IHT1 #X2 #H @(csn_ind … H) -X2
-#V #HV #IHV #W #T1 #H1 #IHT2 destruct
+fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 →
+ ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1.
+#h #g #a #L #X #H @(csn_ind … H) -X
+#X #HT1 #IHT1 #V #W #T1 #H1 destruct
@csn_intro #X #H1 #H2
elim (cpx_inv_appl1 … H1) -H1 *
-[ #V0 #Y #HLV0 #H #H0 destruct
+[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_tpair_dx … H2) -H2
- [ lapply (csn_cpx_trans … HV … HLV0) -HV #HV0 #HWT0
- @IHT1 -IHT1 [4,5: // |1: skip |2,3: /2 width=1/ ] -HWT0 -HV0 #T2 #HT02
- lapply (lpx_cpxs_trans … HT02 (L.ⓛW) ?) [ /2 width=1/ ] -W0 #HT02
- lapply (cpxs_strap2 … HLT0 … HT02) -T0 #HT12
- lapply (IHT2 … HT12) -T1 #HT2
- @(csn_cpx_trans … HT2) -HT2 /2 width=1/
- | -HV -HT1 -IHT1 -HLW0 -HLT0 * #H #HV0 destruct
- @IHV -IHV [1,3: // |2: /2 width=1/ ] -HV0 #T2 #HT02
- lapply (IHT2 … HT02) -IHT2 -HT02 #HT2
- @(csn_cpx_trans … HT2) -HT2 /2 width=1/
- ]
-| -HT1 -IHT1 -HV -IHV -H2 #b #V0 #W0 #T0 #T3 #HLV0 #HLT01 #H1 #H2 destruct
- lapply (IHT2 T3 ?) [ /2 width=1/ ] -IHT2 -HLT01 #HT3
- @(csn_cpx_trans … HT3) -HT3 /2 width=1/
-| -HT1 -IHT1 -HV -IHV -IHT2 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
+ @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1/ ] -H2
+ lapply (lsubx_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/
+| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
+ lapply (lsubx_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02
+ @(csn_cpx_trans … HT1) -HT1 /3 width=1/
+| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
]
qed-.
(* Basic_1: was just: sn3_beta *)
-lemma csn_appl_beta: ∀h,g,a,L,W,T1. ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T1 → ∀V. (
- ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2
- ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1.
-#h #g #a #L #W #T1 #HWT1 #V #IHT2 lapply (IHT2 T1 ?) //
-#HVT1 lapply (csn_fwd_pair_sn … HVT1) -HVT1
-/3 width=3 by csn_appl_beta_aux/ qed.
+lemma csn_appl_beta: ∀h,g,a,L,V,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}ⓝW.V.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T.
+/2 width=3 by csn_appl_beta_aux/ qed.
fact csn_appl_theta_aux: ∀h,g,a,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T.
lapply (csn_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
@(csn_cpx_trans … HVY) /2 width=1/
]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
@csn_abbr /2 width=3 by csn_cpx_trans/ -HV
𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1.
#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
@csn_intro #X #HL #H
-elim (cpx_inv_appl1_simple … HL ?) -HL //
+elim (cpx_inv_appl1_simple … HL) -HL //
#V0 #T0 #HLV0 #HLT10 #H0 destruct
elim (eq_false_inv_tpair_sn … H) -H
[ -IHT1 #HV0
(**************************************************************************)
include "basic_2/computation/acp_cr.ma".
-include "basic_2/computation/cprs_tstc_vector.ma".
-include "basic_2/computation/csn_lpr.ma".
+include "basic_2/computation/cpxs_tstc_vector.ma".
+include "basic_2/computation/csn_lpx.ma".
include "basic_2/computation/csn_vector.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
(* Advanced properties ******************************************************)
-(* Basic_1: was only: sn3_appls_lref *)
-lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ →
- ∀Vs. L ⊢ ⬊* Vs → L ⊢ ⬊* ⒶVs.T.
-#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
+(* Basic_1: was just: sn3_appls_lref *)
+lemma csn_applv_cnx: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ →
+ ∀Vs. ⦃h, L⦄ ⊢ ⬊*[g] Vs → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.T.
+#h #g #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csn … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
elim (csnv_inv_cons … H) -H #HV #HVs
@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs
#X #H #H0
-lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H
-elim (H0 ?) -H0 //
+lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
+elim (H0) -H0 //
qed.
-(* Basic_1: was: sn3_appls_beta *)
-lemma csn_applv_beta: ∀a,L,W. L ⊢ ⬊* W →
- ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓ{a}V.T →
- L ⊢ ⬊* ⒶVs. ⓐV.ⓛ{a}W. T.
-#a #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
-#V0 #Vs #IHV #V #T #H1T
+lemma csn_applv_sort: ∀h,g,L,k,Vs. ⦃h, L⦄ ⊢ ⬊*[g] Vs → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.⋆k.
+#h #g #L #k elim (deg_total h g k)
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1/ ]
+#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
+#Hkl #Vs elim Vs -Vs /2 width=1/
+#V #Vs #IHVs #HVVs
+elim (csnv_inv_cons … HVVs) #HV #HVs
+@csn_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs
+#X #H #H0
+elim (cpxs_fwd_sort_vector … H) -H #H
+[ elim H0 -H0 //
+| -H0 @(csn_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/
+]
+qed.
+
+(* Basic_1: was just: sn3_appls_beta *)
+lemma csn_applv_beta: ∀h,g,a,L,Vs,V,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.ⓓ{a}ⓝW.V.T →
+ ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs. ⓐV.ⓛ{a}W.T.
+#h #g #a #L #Vs elim Vs -Vs /2 width=1/
+#V0 #Vs #IHV #V #W #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV0
lapply (csn_fwd_flat_dx … H1T) #H2T
@csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T
#X #H #H0
-elim (cprs_fwd_beta_vector … H) -H #H
-[ -H1T elim (H0 ?) -H0 //
-| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+elim (cpxs_fwd_beta_vector … H) -H #H
+[ -H1T elim H0 -H0 //
+| -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/
]
qed.
-lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
+lemma csn_applv_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀Vs.L ⊢ ⬊* (ⒶVs. V2) → L ⊢ ⬊* (ⒶVs. #i).
-#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+ ∀Vs. ⦃h, L⦄ ⊢ ⬊*[g] (ⒶVs.V2) → ⦃h, L⦄ ⊢ ⬊*[g] (ⒶVs.#i).
+#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
[ #H
lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
- lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=4/
+ lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/
| #V #Vs #IHV #H1T
lapply (csn_fwd_pair_sn … H1T) #HV
lapply (csn_fwd_flat_dx … H1T) #H2T
@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T
#X #H #H0
- elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
- [ -H1T elim (H0 ?) -H0 //
- | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+ elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
+ [ -H1T elim H0 -H0 //
+ | -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/
]
]
qed.
-(* Basic_1: was: sn3_appls_abbr *)
-lemma csn_applv_theta: ∀a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. L ⊢ ⬊* ⓓ{a}V. ⒶV2s. T → L ⊢ ⬊* V →
- L ⊢ ⬊* ⒶV1s. ⓓ{a}V. T.
-#a #L #V1s #V2s * -V1s -V2s /2 width=1/
+(* Basic_1: was just: sn3_appls_abbr *)
+lemma csn_applv_theta: ∀h,g,a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.ⒶV2s.T →
+ ⦃h, L⦄ ⊢ ⬊*[g] ⒶV1s.ⓓ{a}V.T.
+#h #g #a #L #V1s #V2s * -V1s -V2s /2 width=1/
#V1s #V2s #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
elim H -V1s -V2s /2 width=3/
-#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV
+#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H
lapply (csn_appl_theta … HW12 … H) -H -HW12 #H
lapply (csn_fwd_pair_sn … H) #HW1
lapply (csn_fwd_flat_dx … H) #H1
-@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
-elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
-[ -H #H elim (H2 ?) -H2 //
-| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
+@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -H1 #X #H1 #H2
+elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+[ -H #H elim H2 -H2 //
+| -H2 #H1 @(csn_cpxs_trans … H) -H /2 width=1/
]
qed.
-(* Basic_1: was: sn3_appls_cast *)
-lemma csn_applv_tau: ∀L,W. L ⊢ ⬊* W →
- ∀Vs,T. L ⊢ ⬊* ⒶVs. T →
- L ⊢ ⬊* ⒶVs. ⓝW. T.
-#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
-#V #Vs #IHV #T #H1T
-lapply (csn_fwd_pair_sn … H1T) #HV
+(* Basic_1: was just: sn3_appls_cast *)
+lemma csn_applv_cast: ∀h,g,L,Vs,W,T. ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.W → ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.T →
+ ⦃h, L⦄ ⊢ ⬊*[g] ⒶVs.ⓝW.T.
+#h #g #L #Vs elim Vs -Vs /2 width=1/
+#V #Vs #IHV #W #T #H1W #H1T
+lapply (csn_fwd_pair_sn … H1W) #HV
+lapply (csn_fwd_flat_dx … H1W) #H2W
lapply (csn_fwd_flat_dx … H1T) #H2T
-@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T
+@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T
#X #H #H0
-elim (cprs_fwd_tau_vector … H) -H #H
-[ -H1T elim (H0 ?) -H0 //
-| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+elim (cpxs_fwd_cast_vector … H) -H #H
+[ -H1W -H1T elim H0 -H0 //
+| -H1W -H0 @(csn_cpxs_trans … H1T) -H1T /2 width=1/
+| -H1T -H0 @(csn_cpxs_trans … H1W) -H1W /2 width=1/
]
qed.
-theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬊* T).
-@mk_acr //
+theorem csn_acr: ∀h,g. acr (cpx h g) (eq …) (csn h g) (λL,T. ⦃h, L⦄ ⊢ ⬊*[g] T).
+#h #g @mk_acr //
[ /3 width=1/
-| /2 width=1/
-| /2 width=6/
-| #L #V1 #V2 #HV12 #a #V #T #H #HVT
- @(csn_applv_theta … HV12) -HV12 //
+|2,3,6: /2 width=1/
+| /2 width=7/
+| #L #V1s #V2s #HV12s #a #V #T #H #HV
+ @(csn_applv_theta … HV12s) -HV12s
@(csn_abbr) //
-| /2 width=1/
| @csn_lift
]
qed.
include "basic_2/grammar/term_vector.ma".
include "basic_2/computation/csn.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
-definition csnv: lenv → predicate (list term) ≝
- λL. all … (csn L).
+definition csnv: ∀h. sd h → lenv → predicate (list term) ≝
+ λh,g,L. all … (csn h g L).
interpretation
"context-sensitive strong normalization (term vector)"
- 'SN L Ts = (csnv L Ts).
+ 'SN h g L Ts = (csnv h g L Ts).
(* Basic inversion lemmas ***************************************************)
-lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts.
+lemma csnv_inv_cons: ∀h,g,L,T,Ts. ⦃h, L⦄ ⊢ ⬊*[g] T @ Ts →
+ ⦃h, L⦄ ⊢ ⬊*[g] T ∧ ⦃h, L⦄ ⊢ ⬊*[g] Ts.
normalize // qed-.
(* Basic forward lemmas *****************************************************)
-lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T.
-#L #T #Vs elim Vs -Vs /2 width=1/
+lemma csn_fwd_applv: ∀h,g,L,T,Vs. ⦃h, L⦄ ⊢ ⬊*[g] Ⓐ Vs.T →
+ ⦃h, L⦄ ⊢ ⬊*[g] Vs ∧ ⦃h, L⦄ ⊢ ⬊*[g] T.
+#h #g #L #T #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHVs #HVs
lapply (csn_fwd_pair_sn … HVs) #HV
lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
∃∃T. ⦃h, L⦄ ⊢ T1 •*[g] T & L ⊢ T ➡* T2.
interpretation "decomposed extended parallel computation (term)"
- 'DecomposedXPRedStar h g L T1 T2 = (dxprs h g L T1 T2).
+ 'DecomposedPRedStar h g L T1 T2 = (dxprs h g L T1 T2).
(* Basic properties *********************************************************)
(**************************************************************************)
include "basic_2/unfold/sstas_aaa.ma".
-include "basic_2/computation/cprs_aaa.ma".
+include "basic_2/computation/cpxs_aaa.ma".
include "basic_2/computation/dxprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
(* Basic properties *********************************************************)
-lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+axiom lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+(*
/3 width=3/ qed.
-
+*)
lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
/2 width=1/ qed.
inductive lsubc (RP:lenv→predicate term): relation lenv ≝
| lsubc_atom: lsubc RP (⋆) (⋆)
| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
- lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW)
+| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → ⦃L1, W⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
+ lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2. ⓛW)
.
interpretation
#RP #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
]
-qed.
+qed-.
-(* Basic_1: was: csubc_gen_sort_r *)
+(* Basic_1: was just: csubc_gen_sort_r *)
lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆.
-/2 width=4/ qed-.
+/2 width=4 by lsubc_inv_atom1_aux/ qed-.
-fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
- K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & I = Abbr.
+fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
+ L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
#RP #L1 #L2 * -L1 -L2
[ #I #K1 #V #H destruct
| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10/
]
-qed.
+qed-.
(* Basic_1: was: csubc_gen_head_r *)
-lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V ⊑[RP] L2 →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
- K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & I = Abbr.
-/2 width=3/ qed-.
+lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 →
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
+ L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+/2 width=3 by lsubc_inv_pair1_aux/ qed-.
fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
#RP #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
]
-qed.
+qed-.
-(* Basic_1: was: csubc_gen_sort_l *)
+(* Basic_1: was just: csubc_gen_sort_l *)
lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
-/2 width=4/ qed-.
+/2 width=4 by lsubc_inv_atom2_aux/ qed-.
fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
(∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L1 = K1. ⓓV & I = Abst.
+ L1 = K1. ⓓⓝW.V & I = Abst.
#RP #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8/
]
-qed.
+qed-.
-(* Basic_1: was: csubc_gen_head_l *)
+(* Basic_1: was just: csubc_gen_head_l *)
lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W →
- (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ (∃∃K1. K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨
+ ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L1 = K1. ⓓV & I = Abst.
-/2 width=3/ qed-.
+ L1 = K1.ⓓⓝW.V & I = Abst.
+/2 width=3 by lsubc_inv_pair2_aux/ qed-.
(* Basic properties *********************************************************)
-(* Basic_1: was: csubc_refl *)
+(* Basic_1: was just: csubc_refl *)
lemma lsubc_refl: ∀RP,L. L ⊑[RP] L.
#RP #L elim L -L // /2 width=1/
qed.
[ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=3/
| elim (IHL12 … H) -L2 /3 width=3/
]
-| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #X #e #H
+| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
- [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=7/
+ [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=8/
| elim (IHL12 … H) -L2 /3 width=3/
]
qed-.
| #L1 #I #V1 #X #H
elim (lsubc_inv_pair1 … H) -H *
[ #K1 #HLK1 #H destruct /3 width=3/
- | #K1 #W1 #A #HV1 #HW1 #HLK1 #H1 #H2 destruct /3 width=3/
+ | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct /3 width=4/
]
| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
elim (IHLK1 … HK12) -K1 /3 width=5/
elim (lsubc_inv_pair1 … H) -H *
[ #K2 #HK12 #H destruct
elim (IHLK1 … HK12) -K1 /3 width=5/
- | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
+ | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
+ elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
- lapply (s8 … HA … HV2 … HLK1 HV21) -HV2
- elim (lift_total W2 d e) /4 width=9/
+ lapply (s8 … HA … HV2 … HLK1 HV3) -HV2
+ lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=10/
]
]
qed-.
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* properties concerning lenv refinement for atomic arity assignment ********)
-
-lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+(*
+lamma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2.
#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
// /2 width=1/ /3 width=4/
qed.
+*)
\ No newline at end of file
]
qed-.
-lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → L ⊢ ⬊* T.
+lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ⦃h, L⦄ ⊢ ⬊*[g] T.
#h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/cprs_aaa.ma".
+include "basic_2/computation/cpxs_aaa.ma".
include "basic_2/equivalence/cpcs_cpcs.ma".
(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
-lemma eq_false_inv_beta: ∀a,V1,V2,W1,W2,T1,T2.
- (ⓐV1. ⓛ{a}W1. T1 = ⓐV2. ⓛ{a}W2 .T2 → ⊥) →
- (W1 = W2 → ⊥) ∨
- (W1 = W2 ∧ (ⓓ{a}V1. T1 = ⓓ{a}V2. T2 → ⊥)).
-#a #V1 #V2 #W1 #W2 #T1 #T2 #H
-elim (eq_false_inv_tpair_sn … H) -H
-[ #HV12 elim (term_eq_dec W1 W2) /3 width=1/
- #H destruct @or_intror @conj // #H destruct /2 width=1/
-| * #H1 #H2 destruct
- elim (eq_false_inv_tpair_sn … H2) -H2 /3 width=1/
- * #H #HT12 destruct
- @or_intror @conj // #H destruct /2 width=1/
-]
-qed.
-
(* Basic_1: removed theorems 3:
not_void_abst not_abbr_void not_abst_void
*)
- forth letter (if present)
-p: non-reflexive transitive closure (plus)
-q: reflexive closure (question)
-s: reflexive transitive closure (star)
+e: reflexive transitive closure to normal form (evaluation)
+p: non-reflexive transitive closure (plus)
+q: reflexive closure (question)
+s: reflexive transitive closure (star)
notation "hvbox( L1 ⊑ break term 46 L2 )"
non associative with precedence 45
- for @{ 'SubEq $L1 $L2 }.
+ for @{ 'CrSubEq $L1 $L2 }.
notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )"
non associative with precedence 45
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
+notation "hvbox( L1 ⓝ ⊑ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqT $L1 $L2 }.
+
notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
non associative with precedence 45
for @{ 'DecomposedPRedStar $h $g $L $T1 $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PEval $L $T1 $T2 }.
-
notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )"
non associative with precedence 45
for @{ 'SN $h $g $L $T }.
non associative with precedence 45
for @{ 'SNAlt $h $g $L $T }.
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PEval $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PEval $h $g $L $T1 $T2 }.
+
(* Conversion ***************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
]
qed-.
-lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥.
+axiom cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥.
+(*
#h #g #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/
]
qed-.
-
+*)
lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ →
∧∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ & 𝐒⦃T⦄.
#h #g #L #V1 #T1 #HVT1 @and3_intro
| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
- | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+ | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
]
qed-.
qed-.
(* Basic forward lemmas *****************************************************)
-
-lemma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄.
+(*
+lamma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄.
#h #g #L #T #H #U #HTU
@H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *)
qed-.
-
+*)
(* Basic properties *********************************************************)
lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄.
(* Basic properties *********************************************************)
-lemma cpr_lsubr_trans: lsubr_trans … cpr.
+lemma cpr_lsubr_trans: lsub_trans … cpr lsubr.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
include "basic_2/static/ssta.ma".
include "basic_2/reduction/cpr.ma".
+include "basic_2/reduction/lsubx.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g K V V2 →
⇧[0, i + 1] V2 ≡ W2 → cpx h g L (#i) W2
| cpx_bind : ∀a,I,L,V1,V2,T1,T2.
- cpx h g L V1 V2 → cpx h g (L. ⓑ{I} V1) T1 T2 →
- cpx h g L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+ cpx h g L V1 V2 → cpx h g (L. ⓑ{I}V1) T1 T2 →
+ cpx h g L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
| cpx_flat : ∀I,L,V1,V2,T1,T2.
cpx h g L V1 V2 → cpx h g L T1 T2 →
- cpx h g L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+ cpx h g L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
| cpx_zeta : ∀L,V,T1,T,T2. cpx h g (L.ⓓV) T1 T →
- ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV. T1) T2
-| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV. T1) T2
-| cpx_beta : ∀a,L,V1,V2,W,T1,T2.
- cpx h g L V1 V2 → cpx h g (L.ⓛW) T1 T2 →
- cpx h g L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
+ ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV.T1) T2
+| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV.T1) T2
+| cpx_ti : ∀L,V1,V2,T. cpx h g L V1 V2 → cpx h g L (ⓝV1.T) V2
+| cpx_beta : ∀a,L,V1,V2,W1,W2,T1,T2.
+ cpx h g L V1 V2 → cpx h g L W1 W2 → cpx h g (L.ⓛW1) T1 T2 →
+ cpx h g L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
| cpx_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → cpx h g (L.ⓓW1) T1 T2 →
- cpx h g L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2)
+ cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 →
+ cpx h g (L.ⓓW1) T1 T2 →
+ cpx h g L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2)
.
interpretation
(* Basic properties *********************************************************)
+lemma lsubx_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubx.
+#h #g #L1 #T1 #T2 #H elim H -L1 -T1 -T2
+[ //
+| /2 width=2/
+| #I #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (lsubx_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+ [ /3 width=7/ | /4 width=7/ ]
+|4,9: /4 width=1/
+|5,7,8: /3 width=1/
+|6,10: /4 width=3/
+]
+qed-.
+
(* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *)
lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
#h #g #T elim T -T // * /2 width=1/
qed.
-
-lemma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+(*
+lamma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
#h #g #L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=3/ /2 width=7/
qed.
-
+*)
fact ssta_cpx_aux: ∀h,g,L,T1,T2,l0. ⦃h, L⦄ ⊢ T1 •[g] ⦃l0, T2⦄ →
∀l. l0 = l+1 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
#h #g #L #T1 #T2 #l0 #H elim H -L -T1 -T2 -l0 /2 width=2/ /2 width=7/ /3 width=2/ /3 width=7/
∀T. ⦃h, L⦄ ⊢ ②{I}V1.T ➡[g] ②{I}V2.T.
#h #g * /2 width=1/ qed.
-lemma cpx_delift: ∀h,g,L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
+lemma cpx_delift: ∀h,g,I,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
∃∃T2,T. ⦃h, L⦄ ⊢ T1 ➡[g] T2 & ⇧[d, 1] T ≡ T2.
-#h #g #L #K #V #T1 #d #HLK
-elim (cpr_delift … HLK) -HLK /3 width=4/
+#h #g #I #K #V #T1 elim T1 -T1
+[ * #i #L #d #HLK /2 width=4/
+ elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4/ ]
+ destruct
+ elim (lift_total V 0 (i+1)) #W #HVW
+ elim (lift_split … HVW i i) // /3 width=7/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
+ elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+ [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/
+ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
+ ]
+]
qed-.
lemma cpx_append: ∀h,g. l_appendable_sn … (cpx h g).
| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
| #L #V #T1 #T #T2 #_ #_ #J #H destruct
| #L #V #T1 #T2 #_ #J #H destruct
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #J #H destruct
+| #L #V1 #V2 #T #_ #J #H destruct
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #J #H destruct
| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct
]
qed-.
fact cpx_inv_bind1_aux: ∀h,g,L,U1,U2. ⦃h, L⦄ ⊢ U1 ➡[g] U2 →
∀a,J,V1,T1. U1 = ⓑ{a,J} V1. T1 → (
- ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 &
- U2 = ⓑ{a,J} V2. T2
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓑ{a,J} V2. T2
) ∨
∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
a = true & J = Abbr.
| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
| #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W1 #U1 #H destruct /3 width=3/
| #L #V #T1 #T2 #_ #b #J #W1 #U1 #H destruct
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #L #V1 #V2 #T #_ #b #J #W1 #U1 #H destruct
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W1 #U1 #H destruct
| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W1 #U1 #H destruct
]
qed-.
lemma cpx_inv_bind1: ∀h,g,a,I,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡[g] U2 → (
- ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 &
- U2 = ⓑ{a,I} V2. T2
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓑ{a,I} V2. T2
) ∨
∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
a = true & I = Abbr.
∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓓ V1⦄ ⊢ T1 ➡[g] T2 &
U2 = ⓓ{a} V2. T2
) ∨
- ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true.
+ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true.
#h #g #a #L #V1 #T1 #U2 #H
elim (cpx_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
qed-.
lemma cpx_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡[g] U2 →
- ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 &
- U2 = ⓛ{a} V2. T2.
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓛ{a} V2. T2.
#h #g #a #L #V1 #T1 #U2 #H
elim (cpx_inv_bind1 … H) -H *
[ /3 width=5/
fact cpx_inv_flat1_aux: ∀h,g,L,U,U2. ⦃h, L⦄ ⊢ U ➡[g] U2 →
∀J,V1,U1. U = ⓕ{J} V1. U1 →
∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
- U2 = ⓕ{J} V2. T2
+ U2 = ⓕ{J} V2.T2
| (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ J = Cast)
- | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
- U1 = ⓛ{a}W. T1 &
- U2 = ⓓ{a}V2. T2 & J = Appl
+ | (⦃h, L⦄ ⊢ V1 ➡[g] U2 ∧ J = Cast)
+ | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 &
+ ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W1.T1 &
+ U2 = ⓓ{a}ⓝW2.V2.T2 & J = Appl
| ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
U1 = ⓓ{a}W1. T1 &
| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/
| #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct
| #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/
-| #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=9/
+| #L #V1 #V2 #T #HV12 #J #W1 #U1 #H destruct /3 width=1/
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=11/
| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=13/
]
qed-.
∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
U2 = ⓕ{I} V2. T2
| (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ I = Cast)
- | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
- U1 = ⓛ{a}W. T1 &
- U2 = ⓓ{a}V2. T2 & I = Appl
+ | (⦃h, L⦄ ⊢ V1 ➡[g] U2 ∧ I = Cast)
+ | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 &
+ ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W1.T1 &
+ U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl
| ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
U1 = ⓓ{a}W1. T1 &
lemma cpx_inv_appl1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓐ V1.U1 ➡[g] U2 →
∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
U2 = ⓐ V2. T2
- | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
- U1 = ⓛ{a}W. T1 & U2 = ⓓ{a}V2. T2
+ | ∃∃a,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ W1 ➡[g] W2 &
+ ⦃h, L.ⓛW1⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2
| ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
U1 = ⓓ{a}W1. T1 & U2 = ⓓ{a}W2. ⓐV2. T2.
#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
[ /3 width=5/
-| #_ #H destruct
-| /3 width=9/
+|2,3: #_ #H destruct
+| /3 width=11/
| /3 width=13/
]
qed-.
#h #g #L #V1 #T1 #U #H #HT1
elim (cpx_inv_appl1 … H) -H *
[ /2 width=5/
-| #a #V2 #W #U1 #U2 #_ #_ #H #_ destruct
+| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
elim (simple_inv_bind … HT1)
| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
elim (simple_inv_bind … HT1)
]
qed-.
-lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 → (
- ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
- U2 = ⓝ V2. T2
- ) ∨ ⦃h, L⦄ ⊢ U1 ➡[g] U2.
+lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+ U2 = ⓝ V2. T2
+ | ⦃h, L⦄ ⊢ U1 ➡[g] U2
+ | ⦃h, L⦄ ⊢ V1 ➡[g] U2.
#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
[ /3 width=5/
-| /2 width=1/
-| #a #V2 #W #T1 #T2 #_ #_ #_ #_ #H destruct
+|2,3: /2 width=1/
+| #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct
| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
]
qed-.
elim (cix_inv_ri2 … H) /2 width=1/
| #L #V1 #T1 #T2 #_ #_ #H
elim (cix_inv_ri2 … H) /2 width=1/
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+| #L #V1 #V2 #T #_ #_ #H
+ elim (cix_inv_ri2 … H) /2 width=1/
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
elim (cix_inv_appl … H) -H #_ #_ #H
elim (simple_inv_bind … H)
| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
-| #a #K #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+| #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2
+ elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
+| #a #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
- elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /4 width=5/
+ elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
+ elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/
| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
| #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #K #d #e #HLK #X #HX
+| #L #V1 #V2 #U1 #_ #IHV12 #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3/
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
- elim (IHV12 … HLK … HV01) -V1
- elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ /3 width=5/
+ elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
+ elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
+ elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
+ @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *)
| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2.
/3 width=1 by lpx_sn_append, cpx_append/ qed.
-
-lemma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2.
+(*
+lamma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
qed.
-
+*)
(* Basic forward lemmas *****************************************************)
lemma lpx_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → |L1| = |L2|.
| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_appl1 … H) -H *
[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
- | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct
+ | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
- lapply (IHT1 (ⓛ{b}W1.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
+ lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- lapply (lsuba_aaa_trans … HU2 (L2.ⓓV2) ?) -HU2 /2 width=2/ /2 width=3/
+ lapply (lsuba_aaa_trans … HU2 (L2.ⓓⓝW2.V2) ?) -HU2 /3 width=3/
| #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2
lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
elim (cpx_inv_cast1 … H) -H
[ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
| -IHV1 /2 width=1/
+ | -IHT1 /2 width=1/
]
]
qed-.
lemma aaa_lpx_conf: ∀h,g,L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T ⁝ A.
/2 width=7 by aaa_cpx_lpx_conf/ qed-.
-
-lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
+(*
+lamma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
-lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
+lamma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************)
+
+inductive lsubx: relation lenv ≝
+| lsubx_sort: ∀L. lsubx L (⋆)
+| lsubx_bind: ∀I,L1,L2,V. lsubx L1 L2 → lsubx (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubx_abst: ∀L1,L2,V,W. lsubx L1 L2 → lsubx (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+ "local environment refinement (extended reduction)"
+ 'CrSubEqT L1 L2 = (lsubx L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsubx_refl: ∀L. L ⓝ⊑ L.
+#L elim L -L // /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubx_inv_atom1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+[ #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #_ #H destruct
+]
+qed-.
+
+lemma lsubx_inv_atom1: ∀L2. ⋆ ⓝ⊑ L2 → L2 = ⋆.
+/2 width=3 by lsubx_inv_atom1_aux/ qed-.
+
+fact lsubx_inv_abst1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W #H destruct /2 width=1/
+| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
+]
+qed-.
+
+lemma lsubx_inv_abst1: ∀K1,L2,W. K1.ⓛW ⓝ⊑ L2 →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
+/2 width=3 by lsubx_inv_abst1_aux/ qed-.
+
+fact lsubx_inv_abbr2_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
+ ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W #H destruct
+| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+]
+qed-.
+
+lemma lsubx_inv_abbr2: ∀L1,K2,W. L1 ⓝ⊑ K2.ⓓW →
+ ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubx_inv_abbr2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubx_fwd_length: ∀L1,L2. L1 ⓝ⊑ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubx_fwd_lsubr: ∀L1,L2. L1 ⓝ⊑ L2 → L1 ⊑ L2.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubx_fwd_ldrop2_bind: ∀L1,L2. L1 ⓝ⊑ L2 →
+ ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #I #K2 #W #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=3/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ ]
+| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=4/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/lsubx.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************)
+
+(* Auxiliary inversion lemmas ***********************************************)
+
+fact lsubx_inv_bind1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓑ{I}X
+ | ∃∃K2,V,W. K1 ⓝ⊑ K2 & L2 = K2.ⓛW &
+ I = Abbr & X = ⓝW.V.
+#L1 #L2 * -L1 -L2
+[ #L #J #K1 #X #H destruct /2 width=1/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
+| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/
+]
+qed-.
+
+lemma lsubx_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⓝ⊑ L2 →
+ ∨∨ L2 = ⋆
+ | ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓑ{I}X
+ | ∃∃K2,V,W. K1 ⓝ⊑ K2 & L2 = K2.ⓛW &
+ I = Abbr & X = ⓝW.V.
+/2 width=3 by lsubx_inv_bind1_aux/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem lsubx_trans: Transitive … lsubx.
+#L1 #L #H elim H -L1 -L
+[ #L1 #X #H
+ lapply (lsubx_inv_atom1 … H) -H //
+| #I #L1 #L #V #_ #IHL1 #X #H
+ elim (lsubx_inv_bind1 … H) -H // *
+ #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1/
+| #L1 #L #V1 #W #_ #IHL1 #X #H
+ elim (lsubx_inv_abst1 … H) -H // *
+ #L2 #HL2 #H destruct /3 width=1/
+]
+qed-.
]
].
-(* Basic properties *********************************************************)
+(* Basic inversion lemmas ***************************************************)
-lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
-#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ <minus_n_O // ]
-#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
-qed.
-
-lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2).
+lemma deg_inv_pred: ∀h,g,k,l. deg h g (next h k) (l+1) → deg h g k (l+2).
#h #g #k #l #H1
elim (deg_total h g k) #l0 #H0
lapply (deg_next … H0) #H2
lapply (deg_mono … H1 H2) -H1 -H2 #H
<(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
-qed.
+qed-.
-lemma deg_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
+lemma deg_inv_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
#h #g #k #l @(nat_ind_plus … l) -l //
#l #IHl #l0 >iter_SO #H
-lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H
+lapply (deg_inv_pred … H) -H <(associative_plus l0 1 1) #H
lapply (IHl … H) -IHl -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
+#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ <minus_n_O // ]
+#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
qed.
+lemma deg_next_SO: ∀h,g,k,l. deg h g k (l+1) → deg h g (next h k) l.
+#h #g #k #l #Hkl
+lapply (deg_next … Hkl) -Hkl <minus_plus_m_m //
+qed-.
+
lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
#h #k #l <plus_n_Sm <plus_n_Sm //
qed.
lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
-#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1/
+#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1 by deg_inv_pred/
qed.
(* Basic properties *********************************************************)
-lemma cpss_lsubr_trans: lsubr_trans … cpss.
+lemma cpss_lsubr_trans: lsub_trans … cpss lsubr.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
interpretation
"local environment refinement (substitution)"
- 'SubEq L1 L2 = (lsubr L1 L2).
-
-definition lsubr_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
- ∀L2,s1,s2. R L2 s1 s2 → ∀L1. L1 ⊑ L2 → R L1 s1 s2.
+ 'CrSubEq L1 L2 = (lsubr L1 L2).
(* Basic properties *********************************************************)
#L elim L -L // /2 width=1/
qed.
-lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (LTC … R).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=3/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #HL12
- lapply (HR … Hs2 … HL12) -HR -Hs2 /3 width=3/
-]
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+(* Auxiliary inversion lemmas ***********************************************)
+
fact lsubr_inv_abbr1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓓW →
∨∨ L2 = ⋆
| ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW
(* Basic properties *********************************************************)
-lemma cpqs_lsubr_trans: lsubr_trans … cpqs.
+lemma cpqs_lsubr_trans: lsub_trans … cpqs lsubr.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
for native type assignment.
</news>
<news date="In progress.">
- Closure of extended context-sensitive computation
+ Closure of context-sensitive extended computation
for native validity.
</news>
<news date="In progress.">
- Extended context-sensitive strong normalization
+ Reaxiomatized β-reductum as in extended β-reduction
+ </news>
+ <news date="2013 July 20.">
+ Context-sensitive extended strong normalization
for simply typed terms.
</news>
<news date="2013 April 16.">
</news>
<news date="2013 March 16.">
Mutual recursive preservation of stratified native validity
- for hyper computation on closures.
+ for hyper computation on closures.
</news>
<news date="2012 October 16.">
Confluence for context-free parallel reduction on closures.
</news>
<news date="2012 July 26.">
- Term binders polarized to control ζ reduction.
+ Term binders polarized to control ζ-reduction.
</news>
<news date="2012 April 16.">
Context-sensitive subject equivalence
]
class "cyan"
[ { "computation" * } {
- [ { "decomposed extended computation" * } {
- [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ [ { "context-sensitive extended evaluation" * } {
+ [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ )" * ]
}
]
- [ { "weakly normalizing computation" * } {
- [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
+ [ { "context-sensitive evaluation" * } {
+ [ "cpre ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
}
]
[ { "strongly normalizing computation" * } {
[ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ]
}
]
+ [ { "decomposed extended computation" * } {
+ [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ }
+ ]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
[ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ]
}
]
+ [ { "local env. ref. for extended reduction" * } {
+ [ "lsubx ( ? ⓝ⊑ ? )" "lsubx_lsubx" * ]
+ }
+ ]
[ { "context-sensitive normal forms" * } {
[ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
class "yellow"
[ { "substitution" * } {
- [ { "parallel substitution" * } {
+ [ { "parallel substitution" * } {
[ "lpss ( ? ⊢ ▶* ? )" "lpss_ldrop" + "lpss_cpss" + "lpss_lpss" * ]
[ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
}
definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
λA,B,R,a. TC … (R a).
+definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
+ ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2.
+
definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2.
]
qed-.
+lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S.
+#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
+#T #T2 #_ #HT2 #IHT1 #L1 #HL12
+lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/
+qed-.
+
lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S.
#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ]
#T #T2 #_ #HT2 #IHT1 #L1 #HL12
<key name="ex">5 3</key>
<key name="ex">5 4</key>
<key name="ex">5 5</key>
+ <key name="ex">5 6</key>
+ <key name="ex">6 3</key>
<key name="ex">6 4</key>
<key name="ex">6 5</key>
<key name="ex">6 6</key>
<key name="ex">6 7</key>
+ <key name="ex">7 4</key>
<key name="ex">7 7</key>
<key name="ex">8 5</key>
<key name="or">3</key>
<key name="or">4</key>
+ <key name="or">5</key>
<key name="and">3</key>
<key name="and">4</key>
</section>
interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4).
+(* multiple existental quantifier (5, 6) *)
+
+inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
+ | ex5_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → ex5_6 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4).
+
+(* multiple existental quantifier (6, 3) *)
+
+inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝
+ | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5).
+
(* multiple existental quantifier (6, 4) *)
inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
+(* multiple existental quantifier (7, 4) *)
+
+inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
(* multiple existental quantifier (7, 7) *)
inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+(* multiple disjunction connective (5) *)
+
+inductive or5 (P0,P1,P2,P3,P4:Prop) : Prop ≝
+ | or5_intro0: P0 → or5 ? ? ? ? ?
+ | or5_intro1: P1 → or5 ? ? ? ? ?
+ | or5_intro2: P2 → or5 ? ? ? ? ?
+ | or5_intro3: P3 → or5 ? ? ? ? ?
+ | or5_intro4: P4 → or5 ? ? ? ? ?
+.
+
+interpretation "multiple disjunction connective (5)" 'Or P0 P1 P2 P3 P4 = (or5 P0 P1 P2 P3 P4).
+
(* multiple conjunction connective (3) *)
inductive and3 (P0,P1,P2:Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }.
+(* multiple existental quantifier (5, 6) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) }.
+
+(* multiple existental quantifier (6, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }.
+
(* multiple existental quantifier (6, 4) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }.
+(* multiple existental quantifier (7, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }.
+
(* multiple existental quantifier (7, 7) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
non associative with precedence 30
for @{ 'Or $P0 $P1 $P2 $P3 }.
+(* multiple disjunction connective (5) *)
+
+notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3 break | term 29 P4)"
+ non associative with precedence 30
+ for @{ 'Or $P0 $P1 $P2 $P3 $P4 }.
+
(* multiple conjunction connective (3) *)
notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
projects / helm.git / commitdiff