- lleq now uses ynat

- some bugs fixed

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index 41971c43ea5a0a8630b19ef2879167a951e41579..80688b96309012bbb0e888c7c2041ad70f688ca1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -156,7 +156,7 @@ fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → 
                         T2 = ⓪{J} ∨
                         ∃∃I,K,V,i. d ≤ yinj i & i < d + e &
                                    ⇩[O, i] L ≡ K.ⓑ{I}V &
-                                   ⇧[O, i + 1] V ≡ T2 &
+                                   ⇧[O, i+1] V ≡ T2 &
                                    J = LRef i.
 #G #L #T1 #T2 #d #e * -G -L -T1 -T2 -d -e
 [ #I #G #L #d #e #J #H destruct /2 width=1 by or_introl/
@@ -170,7 +170,7 @@ lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 →
                      T2 = ⓪{I} ∨
                      ∃∃J,K,V,i. d ≤ yinj i & i < d + e &
                                 ⇩[O, i] L ≡ K.ⓑ{J}V &
-                                ⇧[O, i + 1] V ≡ T2 &
+                                ⇧[O, i+1] V ≡ T2 &
                                 I = LRef i.
 /2 width=4 by cpy_inv_atom1_aux/ qed-.
 
@@ -184,7 +184,7 @@ 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 &
                               ⇩[O, i] L ≡ K.ⓑ{I}V &
-                              ⇧[O, i + 1] V ≡ T2.
+                              ⇧[O, i+1] V ≡ T2.
 #G #L #T2 #i #d #e #H
 elim (cpy_inv_atom1 … H) -H /2 width=1 by or_introl/
 * #I #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=5 by ex4_3_intro, or_intror/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index 41c6286d66aed95bc67a8bf1e67607bcbe369287..a63a9001aca2a70de5870057debb2ea54071827e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -164,7 +164,7 @@ fact lsuby_inv_pair2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
 qed-.
 
 lemma lsuby_inv_pair2: ∀I2,K2,L1,V,e. L1 ⊑×[0, e] K2.ⓑ{I2}V → 0 < e →
-                       ∃∃I1,K1. K1 ⊑×[0, e-1] K2 & L1 = K1.ⓑ{I1}V.
+                       ∃∃I1,K1. K1 ⊑×[0, ⫰e] K2 & L1 = K1.ⓑ{I1}V.
 /2 width=6 by lsuby_inv_pair2_aux/ qed-.
 
 fact lsuby_inv_succ2_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
index 033034d53bf1893ef098413f73a823ba1d5a5fbf..594c34062abd5c4f6da806a5bcc0e7a783d1885c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
@@ -60,7 +60,7 @@ lemma cpys_refl: ∀G,L,d,e. reflexive … (cpys d e G L).
 /2 width=1 by cpy_cpys/ qed.
 
 lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
-                 ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d+1, e] T2 →
+                 ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 →
                  ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] ⓑ{a,I}V2.T2.
 #G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2
 [ #I #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_bind/
@@ -120,7 +120,7 @@ qed-.
 
 lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] U2 →
                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 &
-                               ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d+1, e] T2 &
+                               ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 &
                                U2 = ⓑ{a,I}V2.T2.
 #a #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2
 [ /2 width=5 by ex3_2_intro/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
index 045aa44901b8375c6a4c782b3e2b457cf7ce4723..929007118c8ec26e2eaee90a189f6fc3a7c3462d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -21,10 +21,10 @@ include "basic_2/substitution/cpys_lift.ma".
 inductive cpysa: ynat → ynat → relation4 genv lenv term term ≝
 | cpysa_atom : ∀I,G,L,d,e. cpysa d e G L (⓪{I}) (⓪{I})
 | cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d+e →
-               ⇩[0, i] L ≡ K.ⓑ{I}V1 → cpysa 0 (d+e-i-1) G K V1 V2 →
+               ⇩[0, i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
                ⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
 | cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
-               cpysa d e G L V1 V2 → cpysa (d + 1) e G (L.ⓑ{I}V2) T1 T2 →
+               cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
                cpysa d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
 | cpysa_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
                cpysa d e G L V1 V2 → cpysa d e G L T1 T2 →
@@ -86,12 +86,12 @@ qed-.
 lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
                     (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) →
                     (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
-                     ⇩[O, i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, d+e-i-1] V2 →
-                     ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) G K V1 V2 → R d e G L (#i) W2
+                     ⇩[O, i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 →
+                     ⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2
                     ) →
                     (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
-                     ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d + 1, e] T2 → R d e G L V1 V2 →
-                     R (d+1) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+                     ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 →
+                     R (⫯d) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
                     ) →
                     (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
                      ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L V1 V2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
index 36e0b0912f4a852e80973fba620ccf677acbce7b..69683612c42380285216a2c6b9a9f3699dcf87a9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
@@ -36,13 +36,21 @@ lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
 ]
 qed.
 
+lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
+                     d ≤ yinj i →
+                     ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 →
+                     ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, ∞] U2.
+#I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
+@(cpys_subst … HLK … HU12) >yminus_Y_inj //
+qed.
+
 (* Advanced inverion lemmas *************************************************)
 
 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 →
                       T2 = ⓪{I} ∨
                       ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e &
                                     ⇩[O, i] L ≡ K.ⓑ{J}V1 &
-                                     ⦃G, K⦄ ⊢ V1 ▶*×[0, d+e-i-1] V2 &
+                                     ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
                                      ⇧[O, i+1] V2 ≡ T2 &
                                      I = LRef i.
 #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2
@@ -63,7 +71,7 @@ lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
                       T2 = #i ∨
                       ∃∃I,K,V1,V2. d ≤ i & i < d + e &
                                    ⇩[O, i] L ≡ K.ⓑ{I}V1 &
-                                   ⦃G, K⦄ ⊢ V1 ▶*×[0, d+e-i-1] V2 &
+                                   ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
                                    ⇧[O, i+1] V2 ≡ T2.
 #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
 * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
@@ -72,7 +80,7 @@ qed-.
 lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
                             ∀I,K,V1. ⇩[O, i] L ≡ K.ⓑ{I}V1 →
                             ∀V2. ⇧[O, i+1] V2 ≡ T2 →
-                            ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, d+e-i-1] V2
+                            ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2
                              & d ≤ i
                              & i < d + e.
 #G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 495967a888a35686777d51918c9bf1528d753455..7e48dbca0c27f98d18a3fadea23cf14d6d430a26 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -17,7 +17,7 @@ include "basic_2/substitution/cpys.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
-definition lleq: relation4 nat term lenv lenv ≝
+definition lleq: relation4 ynat term lenv lenv ≝
                  λd,T,L1,L2. |L1| = |L2| ∧
                              (∀U. ⦃⋆, L1⦄ ⊢ T ▶*×[d, ∞] U ↔ ⦃⋆, L2⦄ ⊢ T ▶*×[d, ∞] U).
 
@@ -38,7 +38,7 @@ lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] L2.
 qed.
 
 lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
-                 L1 ⋕[V, d] L2 → L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V →
+                 L1 ⋕[V, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
                  L1 ⋕[ⓑ{a,I}V.T, d] L2.
 #a #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
 #X @conj #H elim (cpys_inv_bind1 … H) -H
@@ -78,7 +78,7 @@ lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
 qed-.
 
 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d.
-                        L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V.
+                        L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V.
 #a #I #L1 #L2 #V #T #d * #HL12 #H @conj [ normalize // ] -HL12
 #U elim (H (ⓑ{a,I}V.U)) -H
 #H1 #H2 @conj
@@ -113,7 +113,7 @@ qed-.
 (* Basic inversion lemmas ***************************************************)
 
 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[ⓑ{a,I}V.T, d] L2 →
-                     L1 ⋕[V, d] L2 ∧ L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V.
+                     L1 ⋕[V, d] L2 ∧ L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V.
 /3 width=4 by lleq_fwd_bind_sn, lleq_fwd_bind_dx, conj/ qed-.
 
 lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[ⓕ{I}V.T, d] L2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
index 115a8a9fd87258aec4b1c6c32adc878b0a2efd70..69c0f84b12ba4d5d74daeaad8929fc06a9a2ca03 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
@@ -19,14 +19,13 @@ include "basic_2/substitution/lleq.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma lleq_skip: ∀L1,L2,d,i. i < d → |L1| = |L2| → L1 ⋕[#i, d] L2.
+lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2.
 #L1 #L2 #d #i #Hid #HL12 @conj // -HL12
 #U @conj #H elim (cpys_inv_lref1 … H) -H // *
-#I #Z #Y #X #H elim (ylt_yle_false … H) -H
-/2 width=1 by ylt_inj/
+#I #Z #Y #X #H elim (ylt_yle_false … Hid … H)
 qed.
 
-lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ i →
+lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
                  ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
                  K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2.
 #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ]
@@ -34,9 +33,10 @@ lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ i →
   lapply (ldrop_fwd_length … HLK2) -HLK2 #H2
   >H1 >H2 -H1 -H2 normalize //
 | #U @conj #H elim (cpys_inv_lref1 … H) -H // *
-  #I #K #X #W #_ #_ #H #HVW #HWU
-  [ lapply (ldrop_mono … H … HLK1) | lapply (ldrop_mono … H … HLK2) ] -H
-  #H destruct elim (IH W) /3 width=7 by cpys_subst, yle_inj/
+  >yminus_Y_inj #I #K #X #W #_ #_ #H #HVW #HWU
+  [ letin HLK ≝ HLK1 | letin HLK ≝ HLK2 ]
+  lapply (ldrop_mono … H … HLK) -H #H destruct elim (IH W)
+  /3 width=7 by cpys_subst_Y2/
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index ea10429970bb1268aff64b1cd3953de3ceec374b..7405011e040a2489d26b998b71ab07c5d6e75051 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -17,14 +17,14 @@ include "basic_2/substitution/lleq.ma".
 
 (* Advanced forward lemmas **************************************************)
 
-lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
+lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 →
                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
-                      | i < d
+                      | yinj i < d
                       | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V &
                                          ⇩[0, i] L2 ≡ K2.ⓑ{I2}V &
-                                         K1 ⋕[V, 0] K2 & d ≤ i.
+                                         K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
-elim (lt_or_ge i d) /2 width=1 by or3_intro1/ #Hdi #Hi
+elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi
 elim (ldrop_O1_lt … Hi) #I1 #K1 #V1 #HLK1
 elim (ldrop_O1_lt L2 i) // -Hi #I2 #K2 #V2 #HLK2
 lapply (ldrop_fwd_length_minus2 … HLK2) #H
@@ -42,5 +42,5 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
 #W #HVW elim (IH W) -IH #H12 #H21 @conj #H
 [ elim (cpys_inv_lref1_ldrop … (H12 ?) … HLK2 … HVW) -H12 -H21
 | elim (cpys_inv_lref1_ldrop … (H21 ?) … HLK1 … HVW) -H21 -H12
-] /3 width=7 by cpys_subst, yle_inj/
+] [1,3: >yminus_Y_inj ] /3 width=7 by cpys_subst_Y2, yle_inj/
 qed-.