--- /dev/null
+ D I
+sort * *
+lref ldef *
+lref ldec *
+lref lref *
+lref ldef drops *
+lref ldec drops *
+bind * *
+appl appl * *
+appl beta *
+appl pure *
+cast new * *
+cast old * *
+conv *
/3 width=5 by cprs_div, cprs_trans/
qed-.
+lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
+ ∨∨ ∃∃p,W,T0,U0. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L⦄ ⊢ ⓛ{p}W.T0 :*[h] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ T ➡*[h] ⓛ{p}W.T0 & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U0 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]
+ | ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h].
+#h #G #L #X2 #V #T #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H
+elim (cnv_inv_appl … H1) -H1 * [| #n ] #p #W0 #T0 #_ #HV #HT #HW0 #HT0
+lapply (cnv_cpms_trans … HT … HT0) #H
+elim (cnv_inv_bind … H) -H #_ #H1T0
+[ elim (cpms_inv_appl_sn_decompose … H) -H #U #HTU #HUX1
+
+
+ [ #V0 #U0 #HV0 #HU0 #H destruct
+ elim (cnv_cpms_conf … HT … HT0 … HU0)
+ <minus_O_n <minus_n_O #X #H #HU0X
+ elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #HU01 #H destruct
+ @or_introl
+ @(ex5_4_intro … U1 … HT0 … HX2) -HX2
+ [ /2 width=1 by cnv_cpms_nta/
+ | @nta_bind_cnv /2 width=4 by cnv_cpms_trans/ /2 width=3 by cnv_cpms_nta/
+ | @(cpcs_cprs_div … HX21) -HX21
+ @(cprs_div … (ⓐV0.ⓛ{p}W1.U1))
+ /3 width=1 by cpms_appl, cpms_appl_dx, cpms_bind/
+ ]
+
(* Basic_2A1: uses: nta_inv_cast1 *)
lemma nta_inv_cast_sn (a) (h) (G) (L) (X2):
∀U,T. ⦃G,L⦄ ⊢ ⓝU.T :[a,h] X2 →
--- /dev/null
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+(*
+theorem cpm_cpm_trans_swap (h) (G) (L) (T1):
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → n1 ≤ n2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2.
+#h #G #L #T1 #n1 #T #H
+@(cpm_ind … H) -n1 -G -L -T1 -T
+[ #I #G #L #n2 #T2 #HT2 #_ /2 width=3 by ex2_intro/
+| #G #L #s #n2 #X2 #H #_
+ elim (cpm_inv_sort1 … H) -H #H #Hn2 destruct >iter_n_Sm
+ /3 width=3 by cpm_sort, ex2_intro/
+| #n1 #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2 #Hn
+ elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+ elim (IH … HV2) -V [| // ] #V0 #HV10 #HV02
+ elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+ /3 width=3 by cpm_delta, ex2_intro/
+| #n1 #G #K #V1 #V #W #_ #IH #HVW #m2 #T2 #HT2 #H
+ elim (le_inv_S1 … H) -H #n2 #Hn #H destruct
+ elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+ elim (IH … HV2) -V [| /2 width=1 by le_S/ ] #V0 #HV10 #HV02
+ elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVT0 … HVT2) -V2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+ /3 width=5 by cpm_ell, ex2_intro/
+*)
+
+(* Note: cpm_cpm_trans_swap does not hold: take L = K.ⓛV1, T1 = #0, n2 = 0 *)
+theorem cpr_cpm_trans_swap (h) (G) (L):
+ ∀T1,T. ⦃G,L⦄ ⊢ T1 ➡[h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
+#h #G #L #T1 #T #H
+@(cpr_ind … H) -G -L -T1 -T
+[ #I #G #L #n2 #T2 #HT2 /2 width=3 by ex2_intro/
+| #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
+ elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+ elim (IH … HV2) -V #V0 #HV10 #HV02
+ elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+ /3 width=3 by cpm_delta, ex2_intro/
+| #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
+ elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
+ elim (IH … HT2) -T #T0 #HT0 #HT02
+ elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+ lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+ /3 width=3 by cpm_lref, ex2_intro/
+| #p #I #G #L #V1 #V #T1 #T #_ #_ #IHV #IHT #n2 #X2 #H
+ elim (cpm_inv_bind1 … H) -H *
+ [ #V2 #T2 #HV2 #HT2 #H destruct
\ No newline at end of file
/3 width=3 by cpms_trans, cpms_cast_sn/
]
qed.
+
+theorem cpms_trans_swap (h) (G) (L) (T1):
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡*[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡*[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T2.
+#h #G #L #T1 #n1 #T #HT1 #n2 #T2 #HT2
+lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
+/2 width=1 by cpms_inv_plus/
+qed-.
+
+(* More advanced inversion lemmas *******************************************)
+(*
+lemma cpms_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡*[n,h] X2 →
+ ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡*[h] X2.
+#h #n #G #L #V1 #T1 #X2 #H
+@(cpms_ind_dx … H) -n -X2
+[ /2 width=3 by ex2_intro/
+| #n1 #n2 #X #X2 #_ * #X1 #HTX1 #HX1 #HX2
+ elim (pippo … HX1 … HX2) -X #X #HX1 #HX2
+ elim (cpm_inv_appl_sn_decompose … HX1) -HX1 #U1 #HXU1 #HU1X
+ /3 width=5 by cprs_step_sn, cpms_step_dx, ex2_intro/
+]
+qed-.
+*)
--- /dev/null
+
+include "basic_2/rt_computation/cpms_lpr.ma".
+
+theorem cpr_cpm_trans_swap_lpr (h) (G) (L1) (T1):
+ ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
+ ∃∃T0. ⦃G,L1⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L1⦄ ⊢ T0 ➡*[h] T2.
+#h #G #L1 #T1 #T #H
+@(cpr_ind … H) -G -L1 -T1 -T
+[ (* #I #G #L1 #L2 #HL12 #n2 #T2 #HT2 /2 width=3 by ex2_intro/ *)
+| (*
+ #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
+ elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+ elim (IH … HV2) -V #V0 #HV10 #HV02
+ elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+ /3 width=3 by cpm_delta, ex2_intro/
+*)
+| (*
+ #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
+ elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
+ [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
+ elim (IH … HT2) -T #T0 #HT0 #HT02
+ elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+ lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
+ [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+ /3 width=3 by cpm_lref, ex2_intro/
+*)
+| #p #I #G #L1 #V1 #V #T1 #T #HV1 #_ #_ #IHT #L2 #HL12 #n2 #X2 #H
+ elim (cpm_inv_bind1 … H) -H *
+ [ #V2 #T2 #HV2 #HT2 #H destruct
+ elim (IHT … HT2) -T [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
+ lapply (lpr_cpm_trans … HV2 … HL12) -L2 #HV2
+ /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/
+ | #X #HXT #HX2 #H1 #H2 destruct
+ elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2
+ [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2
+ elim (IHT … HT2) -HT2 -IHT [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
+ /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
+ ]
+|
\ No newline at end of file
]
qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpm_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡[n,h] X2 →
+ ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡[h] X2.
+#h #n #G #L #V1 #T1 #X2 #H
+elim (cpm_inv_appl1 … H) -H *
+[ #V2 #T2 #HV12 #HT12 #H destruct
+ /3 width=3 by cpm_appl, ex2_intro/
+| #p #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
+ /3 width=5 by cpm_beta, cpm_bind, ex2_intro/
+| #p #V2 #V0 #W1 #W2 #U1 #U2 #HV12 #HV20 #HW12 #HU12 #H1 #H2 destruct
+ /3 width=5 by cpm_theta, cpm_bind, ex2_intro/
+]
+qed-.
+
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: includes: cpr_fwd_bind1_minus *)
projects / helm.git / commitdiff