X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fllor%2Flpxs_llor.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fllor%2Flpxs_llor.etc;h=0000000000000000000000000000000000000000;hb=98c91e19a9cc31c77a0151f5df7f7690813cbd07;hp=a94a4779146ed881d9595130ff9b882286f81f3b;hpb=41441a27e7dc2afcd20ffd6159015ee77f37a3d8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc deleted file mode 100644 index a94a47791..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc +++ /dev/null @@ -1,125 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/relocation/llor.ma". -include "basic_2/computation/cpxs_lleq.ma". -include "basic_2/computation/lpxs_ldrop.ma". -include "basic_2/computation/lpxs_cpxs.ma". -include "basic_2/computation/lpxs_lpxs.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2. - -axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → - ∨∨ (|L| ≤ i ∧ L = L2) - | (yinj i < d ∧ L = L2) - | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 & - ⇩[i] L2 ≡ K2.ⓑ{I2}V2 & - ⇩[i] L ≡ K.ⓑ{I2}V1 & - L2 ≃[yinj 0, yinj i] L & - K1 ⩖[V1, yinj 0] K2 ≡ K & - d ≤ yinj i. - - -axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2. - -axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i → - ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L & - K1 ⩖[V1, 0] K2 ≡ K. - -axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2. - -axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L → - ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V. - -axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L → - ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L. - -axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|. - -(* Properties obn lazy union for local environments *************************) - -lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d → - ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d → - ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d. -#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d -[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) // -| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) // -| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s - elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s - elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct - elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s - lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d - lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d - - - - -[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d - elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H - elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct - elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct - lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d - lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d - lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s - elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H - lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY - lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H - lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY - >(leq_inv_O_Y … HL2sY) -HL2sY // - - - - - -lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s → - ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s. -#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d // -[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d - elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H - elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct - elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct - lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d - lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d - lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s - elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H - lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY - lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H - lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY - >(leq_inv_O_Y … HL2sY) -HL2sY // -(* -| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d - elim (lleq_inv_bind … H) -H #HV #HT -*) -| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d - elim (lleq_inv_flat … H) -H #HV #HT - lapply (IHV … HV HL12d) -HV #H1 - lapply (IHT … HT HL12d) #H2 - - - - @(lpxs_trans … LV) /2 width=3 by/ -IHV - lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H - - @(IH … HL12d) -IHT -IHV - - /4 width=5 by lpxs_trans/ - - -lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 → - ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2. -#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d -[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H