From: Ferruccio Guidi Date: Mon, 6 Jan 2014 21:17:44 +0000 (+0000) Subject: - lleq now uses ynat X-Git-Tag: make_still_working~1005 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7b7b9a4666ec1e50c64a20fb89bd2fc49f3870f;p=helm.git - 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 41971c43e..80688b963 100644 --- 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 41c6286d6..a63a9001a 100644 --- 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 033034d53..594c34062 100644 --- 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 045aa4490..929007118 100644 --- 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 36e0b0912..69683612c 100644 --- 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 495967a88..7e48dbca0 100644 --- 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 115a8a9fd..69c0f84b1 100644 --- 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 ea1042997..7405011e0 100644 --- 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-.