--- /dev/null
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
+ ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = ⋆s & n = 0
+ | ∧∧ X2 = ⋆(⫯[h]s) & n =1.
+#h #n #G #L #s #X2 * #c #Hc #H
+elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
+/3 width=1 by or_introl, or_intror, conj/
+qed-.
+
+lemma cpt_inv_zero_sn (h) (n) (G) (L):
+ ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = #0 & n = 0
+ | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
+ | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
+#h #n #G #L #X2 * #c #Hc #H
+elim (cpg_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /3 width=1 by or3_intro0, conj/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+ /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+ elim (ist_inv_plus_SO_dx … H2) -H2 [| // ] #m #Hc #H destruct
+ /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
+]
+qed-.
+
+lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
+ ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = #(↑i) & n = 0
+ | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
+#h #n #G #L #i #X2 * #c #Hc #H
+elim (cpg_inv_lref1 … H) -H *
+[ #H1 #H2 destruct /3 width=1 by or_introl, conj/
+| #I #K #V2 #HV2 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
+ ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 * #c #Hc #H
+elim (cpg_inv_gref1 … H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+
+lemma cpt_inv_sort_sn_iter (h) (n) (G) (L) (s):
+ ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
+ ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
+#h #n #G #L #s #X2 #H
+elim (cpt_inv_sort_sn … H) -H * #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
--- /dev/null
+(* Properties with t-bound rt-transition for terms **************************)
+
+axiom cpt_total (h) (n) (G) (L) (T):
+ ∃U. ⦃G,L⦄ ⊢ T ⬆[h,n] U.
+
+lemma pippo (h) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 → ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T & ⦃G,L⦄ ⊢ T ➡[h] T2.
+#h #G #L #T0 #T1 #H
+@(cpr_ind … H) -G -L -T0 -T1
+[ #I #G #L #n #T2 #HT2
+ /2 width=3 by ex2_intro/
+| #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2
+ elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0
+ [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02
+ elim (IH … HV02) -V0 #V0 #HV10 #HV02
+|
+|
+|
+|
+|
+| #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX
+ elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct
+ elim (cpt_inv_cast_sn … HX) -HX *
+ [ #W2 #V2 #HW02 #HV02 #H destruct
+ elim (cpt_total h n G (L.ⓛW1) T0) #T3 #HT03
+ elim (IHV … HV02) -V0 #V0 #HV10 #HV02
+ elim (IHW … HW02) -W0 #W0 #HW10 #HW02
+ elim (IHT … HT02) -T0 #T0 #HT10 #HT02
+ @(ex2_intro … (ⓐV0.ⓛ{p}W0.T0))
+ [ /3 width=1 by cpt_appl, cpt_bind/
+ | @(cpm_beta … HV02 HW02)
+
+ | #m #_ #H destruct
+ ]
+
+lemma cpm_cpt_cpr (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
+#h #n #G #L #T1 #T2 #H
+@(cpm_ind … H) -n -G -L -T1 -T2
+[ #I #G #L /2 width=3 by ex2_intro/
+| #G #L #s /3 width=3 by cpm_sort, ex2_intro/
+| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
+ elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2
+ [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
+ /3 width=3 by cpt_delta, ex2_intro/
+| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
+ elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
+ lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2
+ [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
+ /3 width=3 by cpt_ell, ex2_intro/
+| #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2
+ elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+ lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2
+ [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02
+ /3 width=3 by cpt_lref, ex2_intro/
+| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
+ /3 width=5 by cpt_bind, cpm_bind, ex2_intro/
+| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
+ /3 width=5 by cpt_appl, cpm_appl, ex2_intro/
+| #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02
+ /3 width=5 by cpt_cast, cpm_cast, ex2_intro/
+| #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02
+ elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1
+ [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10
+ /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/
+| #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02
+| #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02
+ /3 width=3 by cpt_ee, ex2_intro/
+| #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02
+ /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/
+| #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20
+ /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/
+]
+
+(* Forward lemmas with t-bound rt-transition for terms **********************)
+
+lemma pippo (h) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 →
+ ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2.
+#h #G #L #T0 #T1 #H
+@(cpr_ind … H) -G -L -T0 -T1
+[ #I #G #L #n #T2 #HT2
+ /2 width=1 by cpt_fwd_cpm/
+| #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2
+ elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0
+ [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02
+ lapply (IH … HV02) -V0 #HV12
+ /2 width=3 by cpm_delta/
+|
+|
+|
+|
+|
+| #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX
+ elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct
+ elim (cpt_inv_cast_sn … HX) -HX *
+ [ #W2 #V2 #HW02 #HV02 #H destruct
+ elim (cpt_total h n G (L.ⓛW1) T0) #T2 #HT02
+ lapply (IHV … HV02) -V0 #HV12
+ lapply (IHW … HW02) -W0 #HW12
+ lapply (IHT … HT02) -T0 #HT12
+ @(cpm_beta … HV12 HW12) //
+
+ | #m #_ #H destruct
+ ]
--- /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/rt_transition/cpt_drops.ma".
+include "basic_2/rt_transition/cpt_fqu.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
+
+(* Main properties **********************************************************)
+
+theorem cpt_n_O_trans (h) (n) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 →
+ ∀T2. ⦃G,L⦄ ⊢ T0 ⬆[h,0] T2 → ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2.
+#h #n #G #L #T0 #T1 #H
+@(cpt_ind … H) -H
+[ #I #G #L #X2 #HX2 //
+| #G #L #s #X2 #HX2
+ elim (cpt_inv_sort_sn_iter … HX2) -HX2 #H #_ destruct //
+| #n #G #K #V1 #V0 #W0 #_ #IH #HVW0 #W2 #HW02
+ elim (cpt_inv_lifts_sn … HW02 (Ⓣ) … K … HVW0) -W0
+ [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVW2 #HV02
+ /3 width=3 by cpt_delta/
+| #n #G #K #W1 #W0 #V0 #_ #IH #HWV0 #V2 #HV02
+ elim (cpt_inv_lifts_sn … HV02 (Ⓣ) … K … HWV0) -V0
+ [| /3 width=1 by drops_refl, drops_drop/ ] #W2 #HWV2 #HW02
+ /3 width=3 by cpt_ell/
+| #n #I #G #K #T0 #U0 #i #_ #IH #HTU0 #U2 #HU02
+ elim (cpt_inv_lifts_sn … HU02 (Ⓣ) … K … HTU0) -U0
+ [| /3 width=1 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT02
+ /3 width=3 by cpt_lref/
+| #n #p #I #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
+ elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+ @cpt_bind
+ [ /2 width=1 by/
+ | @IHT
+ ]
+| #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
+ elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+ /3 width=1 by cpt_appl/
+| #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
+ elim (cpt_inv_cast_sn … HX2) -HX2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpt_cast/
+ | #m #_ #H destruct
+ ]
+| #n #G #L #V1 #V0 #T1 #_ #IH #V2 #HV02
+ /3 width=1 by cpt_ee/
+]
+
+
+
+
\ No newline at end of file
lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
/3 width=3 by cpg_refl, ex2_intro/ qed.
-(* Advanced properties ******************************************************)
-
-lemma cpt_sort (h) (G) (L):
- ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
-#h #G #L * //
-#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
-qed.
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
+ ∀X2. ⦃G,L⦄ ⊢ ⓪{J} ⬆[h,n] X2 →
+ ∨∨ ∧∧ X2 = ⓪{J} & n = 0
+ | ∃∃s. X2 = ⋆(⫯[h]s) & J = Sort s & n =1
+ | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1 & J = LRef 0
+ | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & J = LRef 0 & n = ↑m
+ | ∃∃I,K,T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I} & J = LRef (↑i).
+#h #n #J #G #L #X2 * #c #Hc #H
+elim (cpg_inv_atom1 … H) -H *
+[ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
+| #s #H1 #H2 #H3 destruct /3 width=3 by or5_intro1, ex3_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
+ /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
+ elim (ist_inv_plus_SO_dx … H3) -H3 [| // ] #m #Hc #H destruct
+ /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/
+| #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct
+ /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/
+]
+qed-.
+
+lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
+ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2
+ & X2 = ⓑ{p,I}V2.T2.
+#h #n #p #I #G #L #V1 #T1 #X2 * #c #Hc #H
+elim (cpg_inv_bind1 … H) -H *
+[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+ elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
+ elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
+ /3 width=5 by ex3_2_intro, ex2_intro/
+| #cT #T2 #_ #_ #_ #_ #H destruct
+ elim (ist_inv_plus_10_dx … H)
+]
+qed-.
+
+lemma cpt_inv_appl_sn (h) (n) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] X2 →
+ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓐV2.T2.
+#h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H *
+[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+ elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
+ elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
+ /3 width=5 by ex3_2_intro, ex2_intro/
+| #cV #cW #cU #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #H destruct
+ elim (ist_inv_plus_10_dx … H)
+| #cV #cW #cU #p #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #_ #H destruct
+ elim (ist_inv_plus_10_dx … H)
+]
+qed-.
+
+lemma cpt_inv_cast_sn (h) (n) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓝV1.T1 ⬆[h,n] X2 →
+ ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓝV2.T2
+ | ∃∃m. ⦃G,L⦄ ⊢ V1 ⬆[h,m] X2 & n = ↑m.
+#h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
+[ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
+ elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
+ <idempotent_max
+ /4 width=5 by or_introl, ex3_2_intro, ex2_intro/
+| #cT #_ #H destruct
+ elim (ist_inv_plus_10_dx … H)
+| #cV #H12 #H destruct
+ elim (ist_inv_plus_SO_dx … H) -H [| // ] #m #Hm #H destruct
+ /4 width=3 by ex2_intro, or_intror/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/cpm_drops.ma".
-include "basic_2/rt_transition/cpt_drops.ma".
+include "basic_2/rt_transition/cpm.ma".
+include "basic_2/rt_transition/cpt_fqu.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
-(* Properties with t-bound rt-transition for terms **************************)
-
-lemma cpm_cpt_cpr (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
- ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
-#h #n #G #L #T1 #T2 #H
-@(cpm_ind … H) -n -G -L -T1 -T2
-[ #I #G #L /2 width=3 by ex2_intro/
-| #G #L #s /3 width=3 by cpm_sort, ex2_intro/
-| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
- elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
- lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2
- [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
- /3 width=3 by cpt_delta, ex2_intro/
-| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2
- elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
- lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2
- [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02
- /3 width=3 by cpt_ell, ex2_intro/
-| #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2
- elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
- lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2
- [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02
- /3 width=3 by cpt_lref, ex2_intro/
-| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
- /3 width=5 by cpt_bind, cpm_bind, ex2_intro/
-| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02
- /3 width=5 by cpt_appl, cpm_appl, ex2_intro/
-| #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02
- /3 width=5 by cpt_cast, cpm_cast, ex2_intro/
-| #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02
- elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1
- [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10
- /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/
-| #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02
-| #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02
- /3 width=3 by cpt_ee, ex2_intro/
-| #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02
- /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/
-| #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20
- /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/
-]
-
(* Forward lemmas with t-bound rt-transition for terms **********************)
lemma cpt_fwd_cpm (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2.
\ No newline at end of file
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2.
+#h #n #G #L #T1 #T2 #H
+@(cpt_ind … H) -n -G -L -T1 -T2
+/3 width=3 by cpm_ee, cpm_cast, cpm_appl, cpm_bind, cpm_lref, cpm_ell, cpm_delta/
+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 "static_2/s_transition/fqu_weight.ma".
+include "basic_2/rt_transition/cpt.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
+
+(* Basic eliminators ********************************************************)
+
+lemma cpt_ind (h) (Q:relation5 …):
+ (∀I,G,L. Q 0 G L (⓪{I}) (⓪{I})) →
+ (∀G,L,s. Q 1 G L (⋆s) (⋆(⫯[h]s))) →
+ (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
+ ⇧*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2
+ ) → (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
+ ⇧*[1] V2 ≘ W2 → Q (↑n) G (K.ⓛV1) (#0) W2
+ ) → (∀n,I,G,K,T,U,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T → Q n G K (#i) T →
+ ⇧*[1] T ≘ U → Q n G (K.ⓘ{I}) (#↑i) (U)
+ ) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 →
+ Q 0 G L V1 V2 → Q n G (L.ⓑ{I}V1) T1 T2 → Q n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ ) → (∀n,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 →
+ Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
+ ) → (∀n,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 → ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 →
+ Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
+ ) → (∀n,G,L,V1,V2,T. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 →
+ Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2
+ ) →
+ ∀n,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → Q n G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #n #G #L #T1
+generalize in match n; -n
+@(fqu_wf_ind (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 * [| * [| * ]]
+[ #I #IH #n #X2 #HX2 -IH6 -IH7 -IH8 -IH9
+ elim (cpt_inv_atom_sn … HX2) -HX2 *
+ [ #H1 #H2 destruct -IH2 -IH3 -IH4 -IH5 //
+ | #s #H1 #H2 #H3 destruct -IH1 -IH3 -IH4 -IH5 //
+ | #K #V1 #V2 #HV12 #HVX2 #H1 #H2 destruct -IH1 -IH2 -IH4 -IH5 /3 width=4 by/
+ | #m #K #W1 #W2 #HW12 #HWX2 #H1 #H2 #H3 destruct -IH1 -IH2 -IH3 -IH5 /3 width=4 by/
+ | #J #K #T2 #i #HT2 #HTX2 #H1 #H2 destruct -IH1 -IH2 -IH3 -IH4 /3 width=4 by/
+ ]
+| #p #I #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH7 -IH8 -IH9
+ elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=1 by fqu_bind_dx/
+| #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
+ elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by/
+| #U1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH7
+ elim (cpt_inv_cast_sn … HX2) -HX2 *
+ [ #U2 #T2 #HU12 #HT12 #H destruct -IH9 /3 width=1 by/
+ | #m #Hm #H destruct -IH8 /3 width=1 by/
+ ]
+]
+qed-.
class "cyan"
[ { "rt-transition" * } {
[ { "context-sensitive parallel t-transition" * } {
- [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_cpm" * ]
+ [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_fqu" + "cpt_cpm" * ]
}
]
[ { "context-sensitive parallel r-transition" * } {
#n #H destruct //
qed-.
+lemma ist_inv_10: ∀n. 𝐓⦃n,𝟙𝟘⦄ → ⊥.
+#h #H destruct
+qed-.
+
(* Main inversion properties ************************************************)
theorem ist_inj: ∀n1,n2,c. 𝐓⦃n1,c⦄ → 𝐓⦃n2,c⦄ → n1 = n2.
elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
/2 width=3 by ex2_intro/
qed-.
+
+lemma ist_inv_plus_10_dx: ∀n,c. 𝐓⦃n,c+𝟙𝟘⦄ → ⊥.
+#n #c #H
+elim (ist_inv_plus … H) -H #n1 #n2 #_ #H #_
+/2 width=2 by ist_inv_10/
+qed-.
projects / helm.git / commitdiff