From: Ferruccio Guidi Date: Sun, 5 Jan 2014 21:13:55 +0000 (+0000) Subject: - new definition of lazy equivalence for local environments, X-Git-Tag: make_still_working~1006 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e761a2c61e9c69f045ca6fc82838beaf31894a4;p=helm.git - new definition of lazy equivalence for local environments, driven by extended multiple substitution for terms - minor corrections --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index e62507f9b..dbdbfd24f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". -include "basic_2/computation/fpbs_lift.ma". include "basic_2/computation/fpbg_fpns.ma". include "basic_2/equivalence/cpes_cpds.ma". include "basic_2/dynamic/snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 0716d4512..60e0d2619 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_fpbs.ma". include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index 2ff0d940c..d43f443ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/computation/cpds_cpds.ma". -include "basic_2/computation/fpbs_fpbs.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lsstas.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma index ade7b790b..955d59e0d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⋕ break [ term 46 d , break term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ⋕ break [ term 46 T , break term 46 d ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEq $d $T $L1 $L2 }. + for @{ 'LazyEq $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma index 9cd39df3e..b89d7844c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⋕ ⋕ break [ term 46 d , break term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ⋕ ⋕ break [ term 46 T , break term 46 d ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEqAlt $d $T $L1 $L2 }. + for @{ 'LazyEqAlt $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma index a1e78fb6c..321ff3737 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma @@ -28,7 +28,7 @@ lemma lleq_cpx_trans_leq: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → >yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 #H destruct /3 width=7 by cpx_delta/ | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/ - #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 + yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 #H destruct /3 width=7 by cpx_delta/ ] | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma index eeb5ac231..17c2dc14d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma @@ -36,17 +36,21 @@ lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ] #H destruct /2 width=1 by lleq_sort/ | #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/ #Y #H1 #HY + elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/ + yminus_inj #Y #H1 #HY lapply (ldrop_mono … HY … HLK1d) -HY #H destruct elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct - elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/ #Z #Y #X #HK12s #H + elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/ + >yplus_O1 yminus_inj #Z #Y #X #HK12s #H lapply (ldrop_mono … H … HLK2s) -H #H destruct - elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/ #Z #Y #X #HK12d #H + elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/ + >yplus_O1 yminus_inj #Z #Y #X #HK12d #H lapply (ldrop_mono … H … HLK2d) -H #H destruct - elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/ #Y #H3 #HY + elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/ + yminus_inj #Y #H3 #HY lapply (ldrop_mono … HY … HLK2d) -HY #H destruct elim (cpx_inv_lref1 … H2) -H2 -L1s [ -L1d #H destruct /3 width=15 by lleq_skip/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma index 47ac4653d..179bb5f05 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -55,7 +55,7 @@ lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → [ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct | #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O_sn >yplus_O_sn +| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1 #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] [ #_ lapply (ldrop_inv_O2 … H) -H #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index a8567a4b2..41c6286d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -200,7 +200,7 @@ lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → elim (ldrop_inv_atom1 … H) -H #H destruct | #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #i #_ #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #i #H #_ >yplus_O_sn +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #i #H #_ >yplus_O1 elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] [ #_ destruct -I2 >ypred_succ /2 width=4 by ldrop_pair, ex2_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma index 41ab4081d..aec0c7913 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/cpy_cpy.ma". -include "basic_2/substitution/cpys_lift.ma". +include "basic_2/substitution/cpys_alt.ma". (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) @@ -93,3 +93,25 @@ theorem cpys_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 → ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2. normalize /3 width=3 by cpy_trans_down, TC_transitive2/ qed-. + +theorem cpys_antisym_eq: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶*×[d, e] T2 → + ∀L2. ⦃G, L2⦄ ⊢ T2 ▶*×[d, e] T1 → T1 = T2. +#G #L1 #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L1 -T1 -T2 // +[ #I1 #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #_ #_ #HVW2 #_ #L2 #HW2 + elim (lt_or_ge (|L2|) (i+1)) #Hi [ -Hdi -Hide | ] + [ lapply (cpys_weak_full … HW2) -HW2 #HW2 + lapply (cpys_weak … HW2 0 (i+1) ? ?) -HW2 // + [ >yplus_O1 >yplus_O1 /3 width=1 by ylt_fwd_le, ylt_inj/ ] -Hi + #HW2 >(cpys_inv_lift1_eq … HW2) -HW2 // + | elim (ldrop_O1_le … Hi) -Hi #K2 #HLK2 + elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2 + /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide + #X #_ #H elim (lift_inv_lref2_be … H) -H // + ] +| #a #I #G #L1 #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #H elim (cpys_inv_bind1 … H) -H + #V #T #HV2 #HT2 #H destruct + lapply (IHV12 … HV2) #H destruct -IHV12 -HV2 /3 width=2 by eq_f2/ +| #I #G #L1 #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #H elim (cpys_inv_flat1 … H) -H + #V #T #HV2 #HT2 #H destruct /3 width=2 by eq_f2/ +] +qed-. 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 3cf6f8b31..36e0b0912 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -32,7 +32,7 @@ lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e. lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02 lapply (cpy_weak … HU02 d e ? ?) -HU02 [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ] - >yplus_O_sn ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/ + >yplus_O1 ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ/ ] qed. @@ -69,6 +69,21 @@ lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/ 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 + & d ≤ i + & i < d + e. +#G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H +[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK // +| * #Z #Y #X1 #X2 #Hdi #Hide #HLY #HX12 #HXT2 + lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct + lapply (ldrop_mono … HLY … HLK) -L #H destruct + /2 width=1 by and3_intro/ +] +qed-. + (* Relocation properties ****************************************************) lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma new file mode 100644 index 000000000..495967a88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/lazyeq_4.ma". +include "basic_2/substitution/cpys.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +definition lleq: relation4 nat term lenv lenv ≝ + λd,T,L1,L2. |L1| = |L2| ∧ + (∀U. ⦃⋆, L1⦄ ⊢ T ▶*×[d, ∞] U ↔ ⦃⋆, L2⦄ ⊢ T ▶*×[d, ∞] U). + +interpretation + "lazy equivalence (local environment)" + 'LazyEq T d L1 L2 = (lleq d T L1 L2). + +(* Basic properties *********************************************************) + +lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2. +#L1 #L2 #d #k #HL12 @conj // -HL12 +#U @conj #H >(cpys_inv_sort1 … H) -H // +qed. + +lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] L2. +#L1 #L2 #d #k #HL12 @conj // -HL12 +#U @conj #H >(cpys_inv_gref1 … H) -H // +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 ⋕[ⓑ{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 +#W #U #HVW #HTU #H destruct +elim (IHV W) -IHV #H1VW #H1WV +elim (IHT U) -IHT #H1TU #H1UT +@cpys_bind /2 width=1 by/ -HVW -H1VW -H1WV +[ @(lsuby_cpys_trans … (L2.ⓑ{I}V)) +| @(lsuby_cpys_trans … (L1.ⓑ{I}V)) +] /4 width=5 by lsuby_cpys_trans, lsuby_succ/ (**) (* full auto too slow *) +qed. + +lemma lleq_flat: ∀I,L1,L2,V,T,d. + L1 ⋕[V, d] L2 → L1 ⋕[T, d] L2 → L1 ⋕[ⓕ{I}V.T, d] L2. +#I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12 +#X @conj #H elim (cpys_inv_flat1 … H) -H +#W #U #HVW #HTU #H destruct +elim (IHV W) -IHV elim (IHT U) -IHT +/3 width=1 by cpys_flat/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|. +#L1 #L2 #T #d * // +qed-. + +lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d. + L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2. +#a #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12 +#U elim (H (ⓑ{a,I}U.T)) -H +#H1 #H2 @conj +#H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2 +/2 width=1 by cpys_bind/ -H +#H elim (cpys_inv_bind1 … H) -H +#X #Y #H1 #H2 #H destruct // +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. +#a #I #L1 #L2 #V #T #d * #HL12 #H @conj [ normalize // ] -HL12 +#U elim (H (ⓑ{a,I}V.U)) -H +#H1 #H2 @conj +#H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2 +/2 width=1 by cpys_bind/ -H +#H elim (cpys_inv_bind1 … H) -H +#X #Y #H1 #H2 #H destruct // +qed-. + +lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d. + L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[V, d] L2. +#I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12 +#U elim (H (ⓕ{I}U.T)) -H +#H1 #H2 @conj +#H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2 +/2 width=1 by cpys_flat/ -H +#H elim (cpys_inv_flat1 … H) -H +#X #Y #H1 #H2 #H destruct // +qed-. + +lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d. + L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[T, d] L2. +#I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12 +#U elim (H (ⓕ{I}V.U)) -H +#H1 #H2 @conj +#H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2 +/2 width=1 by cpys_flat/ -H +#H elim (cpys_inv_flat1 … H) -H +#X #Y #H1 #H2 #H destruct // +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. +/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 → + L1 ⋕[V, d] L2 ∧ L1 ⋕[T, d] L2. +/3 width=3 by lleq_fwd_flat_sn, lleq_fwd_flat_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma new file mode 100644 index 000000000..8257394cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/lazyeqalt_4.ma". +include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/substitution/lleq_lleq.ma". + +inductive lleqa: relation4 nat term lenv lenv ≝ +| lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2 +| lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → i < d → lleqa d (#i) L1 L2 +| lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ i → + ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V → + lleqa 0 V K1 K2 → lleqa d (#i) L1 L2 +| lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2 +| lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2 +| lleqa_bind: ∀a,I,L1,L2,V,T,d. + lleqa d V L1 L2 → lleqa (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → + lleqa d (ⓑ{a,I}V.T) L1 L2 +| lleqa_flat: ∀I,L1,L2,V,T,d. + lleqa d V L1 L2 → lleqa d T L1 L2 → lleqa d (ⓕ{I}V.T) L1 L2 +. + +interpretation + "lazy equivalence (local environment) alternative" + 'LazyEqAlt T d L1 L2 = (lleqa d T L1 L2). + +(* Main inversion lemmas ****************************************************) + +theorem lleqa_inv_lleq: ∀L1,L2,T,d. L1 ⋕⋕[T, d] L2 → L1 ⋕[T, d] L2. +#L1 #L2 #T #d #H elim H -L1 -L2 -T -d +/2 width=8 by lleq_flat, lleq_bind, lleq_gref, lleq_free, lleq_lref, lleq_skip, lleq_sort/ +qed-. + +(* Main properties **********************************************************) + +theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2. +#L1 #T @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * /3 width=3 by lleqa_gref, lleqa_sort, lleq_fwd_length/ +[ #i #Hn #L2 #d #H elim (lleq_fwd_lref … H) [ * || * ] + /4 width=9 by lleqa_free, lleqa_lref, lleqa_skip, lleq_fwd_length, ldrop_fwd_rfw/ +| #a #I #V #T #Hn #L2 #d #H elim (lleq_inv_bind … H) -H /3 width=1 by lleqa_bind/ +| #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma new file mode 100644 index 000000000..115a8a9fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpys_lift.ma". +include "basic_2/substitution/lleq.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Advanced properties ******************************************************) + +lemma lleq_skip: ∀L1,L2,d,i. 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/ +qed. + +lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ 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 ] +[ lapply (ldrop_fwd_length … HLK1) -HLK1 #H1 + 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/ +] +qed. + +lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ⋕[#i, d] L2. +#L1 #L2 #d #i #HL1 #HL2 #HL12 @conj // -HL12 +#U @conj #H elim (cpys_inv_lref1 … H) -H // * +#I #Z #Y #X #_ #_ #H lapply (ldrop_fwd_length_lt2 … H) -H +#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ +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 new file mode 100644 index 000000000..ea1042997 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/cpys_cpys.ma". +include "basic_2/substitution/lleq.ma". + +(* Advanced forward lemmas **************************************************) + +lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → + ∨∨ |L1| ≤ i ∧ |L2| ≤ i + | 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. +#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 (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 +lapply (ldrop_fwd_length_minus2 … HLK1) >HL12 yplus_comm // qed. (* Basic inversion lemmas ***************************************************)