/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/
qed-.
-axiom cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2.
-(*
#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ /2 width=3 by ex2_intro/
| /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/
lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2)
[ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ]
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2
- elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0
-(*
- @(ex2_intro … (ⓑ{a,I}V.T0))
- [ @cpys_bind //
- | @(cpxs_bind … HV2) -HV2
+ @(ex2_intro … (ⓑ{a,I}V1.T))
+ [ @cpys_bind //
+ | @cpxs_bind //
- /2 width=5 by cpys_tpxs_trans/
- ]
-*)*)
\ No newline at end of file
+ elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0
+ @(ex2_intro … (ⓑ{a,I}V.T0))
+ [ @cpys_bind //
+ | @(cpxs_trans … (ⓑ{a,I}V.T)) @cpxs_bind // -HT10
+
+
+(*
+ lapply (lsuby_cpys_trans … HT10 (L.ⓑ{I}V) ?) -HT10 /2 width=1 by lsuby_succ/ #HT10
+*)
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 *
+ /3 width=5 by cpys_flat, cpxs_flat, ex2_intro/
\ No newline at end of file
∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/
qed-.
+
+lemma lleq_cpxs_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 →
+ ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+/4 width=6 by lleq_cpxs_conf_dx, lleq_sym/ qed-.
lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
#h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1 by csx_applv_cnx, cnx_sort, simple_atom/ ]
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
#Hkl #Vs elim Vs -Vs /2 width=1 by/
#V #Vs #IHVs #HVVs
(* Advanced properties ******************************************************)
+fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶×[d, e] T1 → e = ∞ →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃T2. ⦃G, L2⦄ ⊢ T ▶×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 &
+ L1 ⋕[T, d] L2 ↔ T1 = T2.
+#h #g #G #L1 #T #T1 #d #e #H elim H -G -L1 -T -T1 -d -e [ * ]
+[ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/
+| #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ]
+ #Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ]
+ #Hdi #e #He #L2 elim (lleq_dec (#i) L1 L2 d) [ /4 width=5 by lpxs_fwd_length, ex3_intro, conj/ ]
+ #HnL12 #HL12 elim (ldrop_O1_lt L1 i) // -Hi #I #K1 #V1 #HLK1
+ elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ elim (lift_total V2 0 (i+1)) #W2 #HVW2
+ @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpy_subst/ -I -K1 -V1 -Hdi
+ @conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be … HVW2) // ]
+| /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/
+| #I #G #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #He #L2 #HL12 destruct
+ elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
+ elim (lift_total V2 0 (i+1)) #W2 #HVW2
+ @(ex3_intro … W2) /2 width=10 by cpxs_lift, cpy_subst/
+
+
+ elim (lleq_dec (#i) L1 L2 d)
+
+|
+]
+
axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
(*
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
(* Advanced forward lemmas **************************************************)
+
+include "basic_2/computation/cpxs_lleq.ma".
+
(*
+lemma lsx_cpxs_conf: ∀h,g,G,L1,T1,T2. G ⊢ ⋕⬊*[h, g, T1] L1 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 →
+ G ⊢ ⋕⬊*[h, g, T2] L2.
+#h #g #G #L1 #T1 #T2 #H @(lsx_ind … H) -L1
+#L1 #HL1 #IHL1 #L2 #HL12 #HT12 @lsx_intro
+#L3 #HL23 #HnL23 elim (lleq_dec T2 L1 L2 0) [| -HnL23 ]
+[ #HT2 @(IHL1 L3) /2 width=3 by lpxs_trans/
+
+ @(lsx_lpxs_trans … HL23)
+| #HnT2 @(lsx_lpxs_trans … HL23) @(IHL1 … L2) //
+ #HT1 @HnT2 @(lleq_cpxs_conf_dx … HT12) //
+]
+*)
+
+lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V1. ⦃G, L1⦄ ⊢ ⬊*[h, g] V1 →
+ ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V1.T] L2 →
+ ∀V2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 →
+ G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V2.
+#h #g #a #I #G #L1 #V1 #H @(csx_ind_alt … H) -V1
+#V1 #_ #IHV1 #L2 #T #H @(lsx_ind … H) -L2
+#L2 #HL2 #IHL2 #V2 #HL12 #HV12 @lsx_intro
+#Y #H #HnT elim (lpxs_inv_pair1 … H) -H
+#L3 #V3 #HL23 #HV23 #H destruct
+lapply (lpxs_trans … HL12 … HL23) #HL13
+elim (eq_term_dec V2 V3)
+[ (* -HV13 -HL2 -IHV1 -HL12 *) #H destruct
+ @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/
+| -IHL2 -HnT #HnV23 elim (eq_term_dec V1 V2)
+ [ #H -HV12 destruct
+ (* @(lsx_lpxs_trans … (L2.ⓑ{I}V2)) /2 width=1 by lpxs_pair/ *)
+ @(IHV1 … HnV23) -IHV1 -HnV23 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13
+ @(lsx_lpxs_trans … HL23)
+
+
lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V. ⦃G, L1⦄ ⊢ ⬊*[h, g] V →
∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V.
elim (eq_term_dec V1 V3)
[ -HV13 -HL2 -IHV1 -HL12 #H destruct
@IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/
-| -IHL2 -HL23 -HnT #HnV13
- @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13 -HV13
- @(lsx_lpxs_trans) … HL2)
-*)
+| -IHL2 -HnT #HnV13
+ @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13
+ @(lsx_lpxs_trans … HL23)
+
(* Advanced inversion lemmas ************************************************)
lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
#h #g #G #L #k #l #Hkl
-lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1 by cnx_sort/
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
qed.
lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →
| /3 width=3 by lleq_bind_repl_O/
]
qed-.
+
+lemma lleq_cpx_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+/4 width=6 by lleq_cpx_conf_dx, lleq_sym/ qed-.
#G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/
qed.
+(* Basic_1: was: subst1_ex *)
lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V →
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2.
#I #G #K #V #T1 elim T1 -T1
I = LRef i.
/2 width=4 by cpy_inv_atom1_aux/ qed-.
+(* Basic_1: was: subst1_gen_sort *)
lemma cpy_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶×[d, e] T2 → T2 = ⋆k.
#G #L #T2 #k #d #e #H
elim (cpy_inv_atom1 … H) -H //
* #I #K #V #i #_ #_ #_ #_ #H destruct
qed-.
+(* Basic_1: was: subst1_gen_lref *)
lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 →
T2 = #i ∨
∃∃I,K,V. d ≤ i & i < d + e &
lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶×[d, 0] T2 → T1 = T2.
/2 width=6 by cpy_inv_refl_O2_aux/ qed-.
+(* Basic_1: was: subst1_gen_lift_eq *)
lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2.
#G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1
/2 width=3 by trans_eq/
]
qed-.
+
+(* Basic_1: removed theorems 25:
+ subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
+ subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
+ subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+ subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
+ subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+ subst0_confluence_lift subst0_tlt
+ subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift
+*)
(* Main properties **********************************************************)
+(* Basic_1: was: subst1_confluence_eq *)
theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 →
∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 →
∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶×[d1, e1] T.
]
qed-.
+(* Basic_1: was: subst1_confluence_neq *)
theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 →
∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 →
(d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
qed-.
(* Note: the constant 1 comes from cpy_subst *)
+(* Basic_1: was: subst1_trans *)
theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 →
∀T2. ⦃G, L⦄ ⊢ T0 ▶×[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2.
#G #L #T1 #T0 #d #e #H elim H -G -L -T1 -T0 -d -e
(* Properties on relocation *************************************************)
+(* Basic_1: was: subst1_lift_lt *)
lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
]
qed-.
+(* Basic_1: was: subst1_lift_ge *)
lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
(* Inversion lemmas on relocation *******************************************)
+(* Basic_1: was: subst1_gen_lift_lt *)
lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
dt + et ≤ d →
]
qed-.
+(* Basic_1: was: subst1_gen_lift_ge *)
lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
yinj d + e ≤ dt →
lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
@ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
- @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
+ @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1/ ]
]
| #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
| #a #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2
;;
let predefined_classes = [
+ ["&"; "⅋"; ];
["!"; "¡"; "⫯"; "⫰"; ];
["?"; "¿"; "⸮"; ];
[":"; "⁝"; ];
projects / helm.git / commitdiff