From: Ferruccio Guidi Date: Thu, 10 Apr 2014 20:50:46 +0000 (+0000) Subject: - some work on extensions: X-Git-Tag: make_still_working~939 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=890a19d326338d96879dedce1eadc7c91a3beac2;p=helm.git - some work on extensions: the alternative definition of lpx_sn and llpx_sn is useless since it is recursive llor seems to contain a bug in the referred components - some work pointwise extended reduction: we restore the "full" version and use it for the normaliztion of extended reduction we still use "lazy" version for the "big-tree" theorem --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index e52104665..9e6cfcd24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/reduction/lpx_ldrop.ma". include "basic_2/computation/cpxs_lift.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) @@ -92,47 +93,36 @@ qed-. (* Properties on sn extended parallel reduction for local environments ******) -lemma llpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpx h g G 0). +lemma lpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpx h g G). #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 [ /2 width=3 by/ | /3 width=2 by cpx_cpxs, cpx_sort/ | #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (llpx_inv_lref_ge_dx … HL12 … HLK2) -L2 - /5 width=8 by cpxs_delta, cpxs_strap2, llpx_cpx_conf/ -| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (llpx_inv_bind_O … HL12) -HL12 /4 width=1 by cpxs_bind/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (llpx_inv_flat … HL12) -HL12 /3 width=1 by cpxs_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 - elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_zeta/ -| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12 - elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_tau/ -| #G #L2 #V1 #V2 #T2 #HV12 #IHV12 #L1 #HL12 - elim (llpx_inv_flat … HL12) /3 width=1 by cpxs_ti/ -| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12 - elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12 - elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_beta/ -| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 - elim (llpx_inv_flat … HL12) -HL12 #HV1 #HL12 - elim (llpx_inv_bind_O … HL12) /3 width=3 by cpxs_theta/ + elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + /4 width=7 by cpxs_delta, cpxs_strap2/ +|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/ +|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/ +| /4 width=3 by cpxs_zeta, lpx_pair/ +| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ ] qed-. lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. -/4 width=9 by llpx_cpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed. +/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed. (* Advanced properties ******************************************************) -lemma cpxs_llpx_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpx h g G 0). -#h #g #G @s_r_trans_LTC1 /2 width=3 by llpx_cpx_trans, llpx_cpx_conf/ (**) (* full auto fails here but works in cprs_cprs *) +lemma lpx_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpx h g G). +#h #g #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) qed-. lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. -/4 width=9 by cpxs_llpx_trans, cpxs_bind_dx, llpx_bind_repl_O/ qed. +/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed. (* Properties on supclosure *************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 92b694f91..de9a897b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -14,7 +14,7 @@ include "basic_2/substitution/fqus_fqus.ma". include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/reduction/llpx_ldrop.ma". +include "basic_2/reduction/cpx_lift.ma". include "basic_2/computation/cpxs.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) @@ -42,9 +42,6 @@ lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. ] qed. -lemma cpxs_llpx_conf: ∀h,g,G. s_r_confluent1 … (cpxs h g G) (llpx h g G 0). -/3 width=5 by llpx_cpx_conf, s_r_conf1_LTC1/ qed-. - (* Advanced inversion lemmas ************************************************) lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma index eabda3146..53fe83271 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/computation/fpbs.ma". +include "basic_2/computation/csx_lift.ma". (* added *) include "basic_2/computation/csx_llpx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma index b21b7bf51..c14492f21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma @@ -12,128 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/grammar/tstc_tstc.ma". -include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/cpxs_llpx.ma". include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/csx_lift.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -(* Advanced properties ******************************************************) +(* Properties on lazy sn extended reduction for local environments **********) lemma csx_llpx_conf: ∀h,g,G,L1,T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. #h #g #G #L1 #T #H @(csx_ind_alt … H) -T -/5 width=3 by csx_intro_cpxs, cpxs_llpx_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *) +/5 width=3 by csx_intro_cpxs, llpx_cpxs_trans, cpxs_llpx_conf/ (* 2 cpxs_llpx_trans *) qed-. - -lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → - ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T. -#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abst1 … H1) -H1 -#W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair_sn … H2) -H2 -[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT - #HT0 lapply (csx_llpx_conf … HT0 (L.ⓛW0)) -HT0 - /4 width=4 by llpx_bind_repl_O/ -| -IHW -HLW0 -HT * #H destruct /3 width=1 by/ -] -qed. - -lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → - ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T. -#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abbr1 … H1) -H1 * -[ #V1 #T1 #HLV1 #HLT1 #H destruct - elim (eq_false_inv_tpair_sn … H2) -H2 - [ /4 width=9 by csx_cpx_trans, csx_llpx_conf, llpx_bind_repl_O/ - | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/ - ] -| -IHV -IHT -H2 - /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/ -] -qed. - -fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → - ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1. -#h #g #a #G #L #X #H @(csx_ind … H) -X -#X #HT1 #IHT1 #V #W #T1 #H1 destruct -@csx_intro #X #H1 #H2 -elim (cpx_inv_appl1 … H1) -H1 * -[ -HT1 #V0 #Y #HLV0 #H #H0 destruct - elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct - @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 - lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/ -| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct - lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 - /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/ -| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was just: sn3_beta *) -lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T. -/2 width=3 by csx_appl_beta_aux/ qed. - -fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csx_fwd_pair_sn … HVT) #HV -lapply (csx_fwd_bind_dx … HVT) -HVT #HVT -@csx_intro #X #HL #H -elim (cpx_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpx_inv_abbr1 … HL) -HL * - [ #V3 #T3 #HV3 #HLT3 #H0 destruct - elim (lift_total V0 0 1) #V4 #HV04 - elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV04) -V4 - #H elim H // - | * #_ #H elim H // - ] - | -H -HVT #H - lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24 - @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 - lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0 - /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct - lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23 - @csx_abbr /2 width=3 by csx_cpx_trans/ -HV - @(csx_llpx_conf … (L.ⓓW0)) /2 width=4 by llpx_bind_repl_O/ -W1 - /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ -] -qed-. - -lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -/2 width=5 by csx_appl_theta_aux/ qed. - -(* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → - 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. -#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csx_intro #X #HL #H -elim (cpx_inv_appl1_simple … HL) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (eq_false_inv_tpair_sn … H) -H -[ -IHT1 #HV0 - @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 - @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ -| -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ - | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma new file mode 100644 index 000000000..f8bf3c475 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -0,0 +1,138 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc_tstc.ma". +include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/csx_alt.ma". +include "basic_2/computation/csx_lift.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Advanced properties ******************************************************) + +lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T +/4 width=3 by csx_intro, lpx_cpx_trans/ +qed-. + +lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → + ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T. +#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 +elim (cpx_inv_abst1 … H1) -H1 +#W0 #T0 #HLW0 #HLT0 #H destruct +elim (eq_false_inv_tpair_sn … H2) -H2 +[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT + #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/ +| -IHW -HLW0 -HT * #H destruct /3 width=1 by/ +] +qed. + +lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → + ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T. +#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 +elim (cpx_inv_abbr1 … H1) -H1 * +[ #V1 #T1 #HLV1 #HLT1 #H destruct + elim (eq_false_inv_tpair_sn … H2) -H2 + [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/ + | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/ + ] +| -IHV -IHT -H2 + /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/ +] +qed. + +fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → + ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1. +#h #g #a #G #L #X #H @(csx_ind … H) -X +#X #HT1 #IHT1 #V #W #T1 #H1 destruct +@csx_intro #X #H1 #H2 +elim (cpx_inv_appl1 … H1) -H1 * +[ -HT1 #V0 #Y #HLV0 #H #H0 destruct + elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct + @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 + lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/ +| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct + lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 + /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/ +| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was just: sn3_beta *) +lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T. +/2 width=3 by csx_appl_beta_aux/ qed. + +fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. +#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csx_fwd_pair_sn … HVT) #HV +lapply (csx_fwd_bind_dx … HVT) -HVT #HVT +@csx_intro #X #HL #H +elim (cpx_inv_appl1 … HL) -HL * +[ -HV #V0 #Y #HLV10 #HL #H0 destruct + elim (cpx_inv_abbr1 … HL) -HL * + [ #V3 #T3 #HV3 #HLT3 #H0 destruct + elim (lift_total V0 0 1) #V4 #HV04 + elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV04) -V4 + #H elim H // + | * #_ #H elim H // + ] + | -H -HVT #H + lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24 + @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 + lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0 + /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/ + ] +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct +| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct + lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23 + @csx_abbr /2 width=3 by csx_cpx_trans/ -HV + @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1 + /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ +] +qed-. + +lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. +/2 width=5 by csx_appl_theta_aux/ qed. + +(* Basic_1: was just: sn3_appl_appl *) +lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → + (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → + 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. +#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csx_intro #X #HL #H +elim (cpx_inv_appl1_simple … HL) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (eq_false_inv_tpair_sn … H) -H +[ -IHT1 #HV0 + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 + @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ +| -IHV -H1T1 -HLV0 * #H #H1T10 destruct + elim (tstc_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ + | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma new file mode 100644 index 000000000..d49b6e7ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/csx_lpx.ma". +include "basic_2/computation/lpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) + +(* Properties on sn extended parallel computation for local environments ****) + +lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index a20455c9c..5e9ea06c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -14,7 +14,7 @@ include "basic_2/computation/acp_cr.ma". include "basic_2/computation/cpxs_tstc_vector.ma". -include "basic_2/computation/csx_llpx.ma". +include "basic_2/computation/csx_lpx.ma". include "basic_2/computation/csx_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index bf05fb03c..cf39bffcc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -37,7 +37,7 @@ lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L [ elim (fquq_cpxs_trans … HT0 … HG1) -T /3 width=7 by fqus_strap2, ex3_2_intro/ | /3 width=5 by cpxs_strap2, ex3_2_intro/ -| lapply (cpxs_llpx_trans … HT0 … HL1) -HT0 #HT10 +| lapply (llpx_cpxs_trans … HT0 … HL1) -HT0 #HT10 lapply (cpxs_llpx_conf … HT10 … HL1) -HL1 #HL1 elim (llpx_fqus_trans … HG2 … HL1) -L /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index 8bcc50cd1..4895dccf5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/reduction/fpb_lift.ma". include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbs.ma". @@ -23,8 +24,7 @@ lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. /3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. -(* Note: this should be moved *) lemma ssta_fpbs: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed. +/4 width=2 by fpb_fpbs, ssta_fpb/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma index 1ac05bce3..35472d7e5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/llpx_sn_tc.ma". -include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/cpxs_llpx.ma". include "basic_2/computation/llpxs.ma". (* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************) @@ -27,11 +27,11 @@ lemma llpxs_pair_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → (* Properties on context-sensitive extended parallel computation for terms **) lemma llpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (llpxs h g G 0). -/3 width=5 by s_r_trans_LTC2, cpxs_llpx_trans/ qed-. +/3 width=5 by s_r_trans_LTC2, llpx_cpxs_trans/ qed-. lemma llpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (llpxs h g G 0). #h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2 -/3 width=5 by cpxs_llpx_trans, s_rs_trans_TC1/ (**) (* full auto too slow *) +/3 width=5 by llpx_cpxs_trans, s_rs_trans_TC1/ (**) (* full auto too slow *) qed-. (* Note: this is an instance of a general theorem *) @@ -40,7 +40,7 @@ lemma llpxs_cpxs_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 #h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 // #L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2 lapply (llpxs_cpxs_trans … HTU2 … HL2) -L2 #HTU2 -/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/ +/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/ qed-. (* Note: this is an instance of a general theorem *) @@ -49,7 +49,7 @@ lemma llpxs_cpx_conf_dx: ∀h,g,G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 #h #g #G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llpxs_ind_dx … H) -L0 // #L0 #L #HL0 #HL2 #IHL2 @(llpxs_strap2 … IHL2) -IHL2 lapply (llpxs_cpx_trans … HTU2 … HL2) -L2 #HTU2 -/3 width=3 by cpxs_llpx_trans, cpxs_llpx_conf/ +/3 width=3 by llpx_cpxs_trans, cpxs_llpx_conf/ qed-. lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → @@ -138,7 +138,7 @@ lemma llpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1 [ /2 width=5 by ex3_2_intro/ | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1 + lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1 lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1 elim (llpx_fquq_trans … HT2 … HK1) -K /3 width=7 by llpxs_strap2, cpxs_strap1, ex3_2_intro/ @@ -151,7 +151,7 @@ lemma llpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1 [ /2 width=5 by ex3_2_intro/ | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1 + lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1 lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1 elim (llpx_fqup_trans … HT2 … HK1) -K /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/ @@ -164,7 +164,7 @@ lemma llpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(llpxs_ind_dx … H) -K1 [ /2 width=5 by ex3_2_intro/ | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (cpxs_llpx_trans … HT1 … HK1) -HT1 #HT1 + lapply (llpx_cpxs_trans … HT1 … HK1) -HT1 #HT1 lapply (cpxs_llpx_conf … HT1 … HK1) -HK1 #HK1 elim (llpx_fqus_trans … HT2 … HK1) -K /3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma index 28a941508..33767f56c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/computation/csx_lift.ma". (* added *) include "basic_2/computation/csx_llpxs.ma". include "basic_2/computation/llsx_ldrop.ma". include "basic_2/computation/llsx_llpx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma new file mode 100644 index 000000000..ee557e438 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predsnstar_5.ma". +include "basic_2/reduction/lpx.ma". +include "basic_2/computation/lprs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝ + λh,g,G. TC … (lpx h g G). + +interpretation "extended parallel computation (local environment, sn variant)" + 'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2. +#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1. +#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/3 width=3 by lpr_lpx, monotonic_TC/ qed. + +lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/2 width=1 by inj/ qed. + +lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L. +/2 width=1 by lprs_lpxs/ qed. + +lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/2 width=3 by step/ qed. + +lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/2 width=3 by TC_strap/ qed. + +lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma new file mode 100644 index 000000000..89122eb55 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/lpx_aaa.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +#h #g #G #L1 #T #A #HT #L2 #HL12 +@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/ +qed-. + +lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma new file mode 100644 index 000000000..8a6b30a57 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predsnstaralt_5.ma". +include "basic_2/computation/cpxs_cpxs.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* alternative definition *) +definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝ + λh,g,G. lpx_sn … (cpxs h g G). + +interpretation "extended parallel computation (local environment, sn variant) alternative" + 'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2). + +(* Main properties on the alternative definition ****************************) + +theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. + +(* Main inversion lemmas on the alternative definition **********************) + +theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2. +/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-. + +(* Alternative eliminators **************************************************) + +lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma new file mode 100644 index 000000000..1dfb297e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -0,0 +1,150 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cpxs_cpxs.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Advanced properties ******************************************************) + +lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 → + ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2. +/2 width=1 by TC_lpx_sn_pair/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2. +/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. + +lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1. +/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. + +(* Properties on context-sensitive extended parallel computation for terms **) + +lemma lpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpxs h g G). +/3 width=5 by s_r_trans_LTC2, lpx_cpxs_trans/ qed-. + +(* Note: alternative proof: /3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ *) +lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpxs h g G). +#h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2 +@s_rs_trans_TC1 /2 width=3 by lpx_cpxs_trans/ (**) (* full auto too slow *) +qed-. + +lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. +/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. + +(* Inversion lemmas on context-sensitive ext parallel computation for terms *) + +lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 & + U2 = ⓛ{a}V2.T2. +#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ +#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct +elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct +lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ +qed-. + +lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & + U2 = ⓓ{a}V2.T2 + ) ∨ + ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true. +#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ + | #T2 #HT02 #HUT2 + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/ + ] +| #U1 #HTU1 #HU01 + elim (lift_total U2 0 1) #U #HU2 + /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/ +] +qed-. + +(* More advanced properties *************************************************) + +lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2. +/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. + +(* Properties on supclosure *************************************************) + +lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 + /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 + #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L + #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T + /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/ +] +qed-. + +lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T +/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ +qed-. + +lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 +[ /2 width=5 by ex3_2_intro/ +| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 + lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 + elim (lpx_fquq_trans … HT2 … HK1) -K + /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ +] +qed-. + +lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 +[ /2 width=5 by ex3_2_intro/ +| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 + lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 + elim (lpx_fqup_trans … HT2 … HK1) -K + /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ +] +qed-. + +lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T +/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma new file mode 100644 index 000000000..d8c489017 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/lpx_ldrop.ma". +include "basic_2/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Properies on local environment slicing ***********************************) + +lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G). +/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-. + +lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G). +/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-. + +lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G). +/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma new file mode 100644 index 000000000..2f9b322db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_leq.ma". +include "basic_2/reduction/lpx_lleq.ma". +include "basic_2/computation/cpxs_leq.ma". +include "basic_2/computation/lpxs_ldrop.ma". +include "basic_2/computation/lpxs_cpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. +#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ +#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2 +#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K +/3 width=3 by lpxs_strap1, ex2_intro/ +qed-. + +lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (ldrop_O1_le (e+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e +[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct +| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + lapply (ysucc_inv_Y_dx … He) -He #He + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/ +] +qed-. + +lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +/2 width=1 by leq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma new file mode 100644 index 000000000..1d287d368 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/lpxs.ma". + +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) + +(* Main properties **********************************************************) + +theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G). +/2 width=3 by trans_TC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc deleted file mode 100644 index f8bf3c475..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc +++ /dev/null @@ -1,138 +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/grammar/tstc_tstc.ma". -include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/csx_lift.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Advanced properties ******************************************************) - -lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → - ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T -/4 width=3 by csx_intro, lpx_cpx_trans/ -qed-. - -lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W → - ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T. -#h #g #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abst1 … H1) -H1 -#W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair_sn … H2) -H2 -[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT - #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/ -| -IHW -HLW0 -HT * #H destruct /3 width=1 by/ -] -qed. - -lemma csx_abbr: ∀h,g,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → - ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V. T. -#h #g #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_abbr1 … H1) -H1 * -[ #V1 #T1 #HLV1 #HLT1 #H destruct - elim (eq_false_inv_tpair_sn … H2) -H2 - [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/ - | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/ - ] -| -IHV -IHT -H2 - /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/ -] -qed. - -fact csx_appl_beta_aux: ∀h,g,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, g] U1 → - ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T1. -#h #g #a #G #L #X #H @(csx_ind … H) -X -#X #HT1 #IHT1 #V #W #T1 #H1 destruct -@csx_intro #X #H1 #H2 -elim (cpx_inv_appl1 … H1) -H1 * -[ -HT1 #V0 #Y #HLV0 #H #H0 destruct - elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct - @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 - lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/ -| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct - lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 - /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/ -| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was just: sn3_beta *) -lemma csx_appl_beta: ∀h,g,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.ⓛ{a}W.T. -/2 width=3 by csx_appl_beta_aux/ qed. - -fact csx_appl_theta_aux: ∀h,g,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -#h #g #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csx_fwd_pair_sn … HVT) #HV -lapply (csx_fwd_bind_dx … HVT) -HVT #HVT -@csx_intro #X #HL #H -elim (cpx_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpx_inv_abbr1 … HL) -HL * - [ #V3 #T3 #HV3 #HLT3 #H0 destruct - elim (lift_total V0 0 1) #V4 #HV04 - elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV04) -V4 - #H elim H // - | * #_ #H elim H // - ] - | -H -HVT #H - lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_drop/ #HV24 - @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 - lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0 - /3 width=5 by csx_cpx_trans, cpx_pair_sn, ldrop_drop, lift_flat/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct - lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23 - @csx_abbr /2 width=3 by csx_cpx_trans/ -HV - @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1 - /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/ -] -qed-. - -lemma csx_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV1.ⓓ{a}V.T. -/2 width=5 by csx_appl_theta_aux/ qed. - -(* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≃ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) → - 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1. -#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csx_intro #X #HL #H -elim (cpx_inv_appl1_simple … HL) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (eq_false_inv_tpair_sn … H) -H -[ -IHT1 #HV0 - @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 - @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ -| -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/ - | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc deleted file mode 100644 index d49b6e7ae..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc +++ /dev/null @@ -1,25 +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/computation/csx_lpx.ma". -include "basic_2/computation/lpxs.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) - -(* Properties on sn extended parallel computation for local environments ****) - -lemma csx_lpxs_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc deleted file mode 100644 index 55c37a8fd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )" - non associative with precedence 45 - for @{ 'LazyCoSN $h $g $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc deleted file mode 100644 index b10b13a28..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc +++ /dev/null @@ -1,65 +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/notation/relations/predsn_5.ma". -include "basic_2/reduction/lpr.ma". -include "basic_2/reduction/cpx.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,g,G. lpx_sn (cpx h g G). - -interpretation "extended parallel reduction (local environment, sn variant)" - 'PRedSn h g G L1 L2 = (lpx h g G L1 L2). - -(* Basic inversion lemmas ***************************************************) - -lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & - L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & - L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 → - ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2. -/2 width=1 by lpx_sn_inv_pair/ qed-. - -(* Basic properties *********************************************************) - -lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L. -/2 width=1 by lpx_sn_refl/ qed. - -lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 → - ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2. -/2 width=1 by lpx_sn_pair/ qed. - -lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2. -#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|. -/2 width=2 by lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc deleted file mode 100644 index f9c2374c2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc +++ /dev/null @@ -1,83 +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/static/aaa_lift.ma". -include "basic_2/static/lsuba_aaa.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on atomic arity assignment for terms **************************) - -(* Note: lemma 500 *) -lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. -#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A -[ #g #L1 #k #X #H - elim (cpx_inv_sort1 … H) -H // * // -| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 - elim (cpx_inv_lref1 … H) -H - [ #H destruct - elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 - elim (lpx_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/ - | * #J #Y #Z #V2 #H #HV12 #HV2 - lapply (ldrop_mono … H … HLK1) -H #H destruct - elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 - elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - /3 width=8 by aaa_lift, ldrop_fwd_drop2/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abbr1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/ - | #T2 #HT12 #HT2 #H destruct -IHV1 - /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/ - ] -| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=1 by lpx_pair, aaa_abst/ -| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_appl1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ - | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct - lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 - lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct - /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ - | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct - lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2 - lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H - elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ - ] -| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 - elim (cpx_inv_cast1 … H) -H - [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ - | -IHV1 /2 width=1 by/ - | -IHT1 /2 width=1 by/ - ] -] -qed-. - -lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/2 width=7 by aaa_cpx_lpx_conf/ qed-. - -lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/2 width=7 by aaa_cpx_lpx_conf/ qed-. - -lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. - -lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc deleted file mode 100644 index 188e8d11b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc +++ /dev/null @@ -1,78 +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/ldrop_lpx_sn.ma". -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/reduction/lpx.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properies on local environment slicing ***********************************) - -lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G). -/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. - -lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G). -/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-. - -lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G). -/2 width=3 by lpx_sn_dropable/ qed-. - -(* Properties on supclosure *************************************************) - -lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/ -[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H - #K2 #W2 #HLK2 #HVW2 #H destruct - /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 - elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 - /3 width=7 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/ -[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H - #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) - /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01 - elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1 - /3 width=5 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H -[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc deleted file mode 100644 index 353f810c3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc +++ /dev/null @@ -1,108 +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/lleq_ldrop.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on lazy equivalence for local environments ********************) -(* -lamma pippo: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1. |L1| = |L2| → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & |K1| = |K2| & - (∀T,d. L1 ⋕[T, d] L2 ↔ K1 ⋕[T, d] K2). -#h #g #G #L2 #K2 #H elim H -L2 -K2 -[ #L1 #H >(length_inv_zero_dx … H) -L1 /3 width=5 by ex3_intro, conj/ -| #I2 #L2 #K2 #V2 #W2 #_ #HVW2 #IHLK2 #Y #H - elim (length_inv_pos_dx … H) -H #I #L1 #V1 #HL12 #H destruct - elim (IHLK2 … HL12) -IHLK2 #K1 #HLK1 #HK12 #IH - elim (eq_term_dec V1 V2) #H destruct - [ @(ex3_intro … (K1.ⓑ{I}W2)) normalize /2 width=1 by / -*) -axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → - ∀L1,T,d. L1 ⋕[T, d] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. -(* -#h #g #G #L2 #K2 #H elim H -L2 -K2 -[ #L1 #T #d #H lapply (lleq_fwd_length … H) -H - #H >(length_inv_zero_dx … H) -L1 /2 width=3 by ex2_intro/ -| #I2 #L2 #K2 #V2 #W2 #HLK2 #HVW2 #IHLK2 #Y #T #d #HT - lapply (lleq_fwd_length … HT) #H - elim (length_inv_pos_dx … H) -H #I1 #L1 #V1 #HL12 #H destruct - elim (eq_term_dec V1 V2) #H destruct - [ @ex2_intro … -*) - -lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 - #K0 #V0 #H1KL1 #_ #H destruct - elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct - /2 width=4 by fqu_lref_O, ex3_intro/ -| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (ldrop_O1_le (e+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc deleted file mode 100644 index 35a8cb482..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc +++ /dev/null @@ -1,74 +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/notation/relations/predsnstar_5.ma". -include "basic_2/reduction/lpx.ma". -include "basic_2/computation/lprs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,g,G. TC … (lpx h g G). - -interpretation "extended parallel computation (local environment, sn variant)" - 'PRedSnStar h g G L1 L2 = (lpxs h g G L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lpxs_ind: ∀h,g,G,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L2. -#h #g #G #L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lpxs_ind_dx: ∀h,g,G,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1. -#h #g #G #L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/3 width=3/ qed. - -lemma lpx_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/2 width=1/ qed. - -lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L. -/2 width=1/ qed. - -lemma lpxs_strap1: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L → ⦃G, L⦄ ⊢ ➡[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/2 width=3/ qed. - -lemma lpxs_strap2: ∀h,g,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L → ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/2 width=3/ qed. - -lemma lpxs_pair_refl: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V. -/2 width=1 by TC_lpx_sn_pair_refl/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lpxs_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, g] L2 → L2 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. - -lemma lpxs_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, g] ⋆ → L1 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpxs_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → |L1| = |L2|. -/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc deleted file mode 100644 index 80c43c731..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc +++ /dev/null @@ -1,32 +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/reduction/lpx_aaa.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -#h #g #G #L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/ -qed-. - -lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → - ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -#G #L1 #T #A #HT #L2 #HL12 -@(aaa_lpxs_conf … HT) -A -T /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc deleted file mode 100644 index 8a6b30a57..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc +++ /dev/null @@ -1,47 +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/notation/relations/predsnstaralt_5.ma". -include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* alternative definition *) -definition lpxsa: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,g,G. lpx_sn … (cpxs h g G). - -interpretation "extended parallel computation (local environment, sn variant) alternative" - 'PRedSnStarAlt h g G L1 L2 = (lpxsa h g G L1 L2). - -(* Main properties on the alternative definition ****************************) - -theorem lpxsa_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. - -(* Main inversion lemmas on the alternative definition **********************) - -theorem lpxs_inv_lpxsa: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ ➡➡*[h, g] L2. -/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-. - -(* Alternative eliminators **************************************************) - -lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv. - R (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - ⦃G, K1⦄ ⊢ ➡*[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc deleted file mode 100644 index 2f21a8d70..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc +++ /dev/null @@ -1,147 +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/computation/cpxs_cpxs.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Advanced properties ******************************************************) - -lemma lpxs_pair: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h, g] V2 → - ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2. -/2 width=1 by TC_lpx_sn_pair/ qed. - -(* Advanced inversion lemmas ************************************************) - -lemma lpxs_inv_pair1: ∀h,g,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L2 = K2.ⓑ{I}V2. -/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. - -lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, g] V2 & L1 = K1.ⓑ{I}V1. -/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. - -(* Properties on context-sensitive extended parallel computation for terms **) - -lemma lpxs_cpx_trans: ∀h,g,G. s_r_trans … (cpx h g G) (lpxs h g G). -/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-. - -lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_trans … (cpx h g G) (lpxs h g G). -/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-. - -lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2. -/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. - -(* Inversion lemmas on context-sensitive ext parallel computation for terms *) - -lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 & - U2 = ⓛ{a}V2.T2. -#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ -#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct -elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct -lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) -/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ -qed-. - -lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & - U2 = ⓓ{a}V2.T2 - ) ∨ - ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true. -#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ -#U0 #U2 #_ #HU02 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpx_inv_abbr1 … HU02) -HU02 * - [ #V2 #T2 #HV02 #HT02 #H destruct - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) - /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ - | #T2 #HT02 #HUT2 - lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 - /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/ - ] -| #U1 #HTU1 #HU01 - elim (lift_total U2 0 1) #U #HU2 - /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/ -] -qed-. - -(* More advanced properties *************************************************) - -lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2. -/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. - -(* Properties on supclosure *************************************************) - -lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 - /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/ -| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 - #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L - #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T - /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/ -] -qed-. - -lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ -#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T -/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ -qed-. - -lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 -[ /2 width=5 by ex3_2_intro/ -| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 - elim (lpx_fquq_trans … HT2 … HK1) -K - /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ -] -qed-. - -lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 -[ /2 width=5 by ex3_2_intro/ -| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 - lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 - elim (lpx_fqup_trans … HT2 … HK1) -K - /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ -] -qed-. - -lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ -#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T -/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc deleted file mode 100644 index d8c489017..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc +++ /dev/null @@ -1,29 +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/reduction/lpx_ldrop.ma". -include "basic_2/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Properies on local environment slicing ***********************************) - -lemma lpxs_ldrop_conf: ∀h,g,G. dropable_sn (lpxs h g G). -/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-. - -lemma ldrop_lpxs_trans: ∀h,g,G. dedropable_sn (lpxs h g G). -/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-. - -lemma lpxs_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpxs h g G). -/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc deleted file mode 100644 index e21c79912..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.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/lleq_leq.ma". -include "basic_2/reduction/lpx_lleq.ma". -include "basic_2/computation/cpxs_leq.ma". -include "basic_2/computation/lpxs_ldrop.ma". -include "basic_2/computation/lpxs_cpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → - ∀L1,T,d. L1 ⋕[T, d] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. -#h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ -#K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2 -#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K -/3 width=3 by lpxs_strap1, ex2_intro/ -qed-. - -lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 - #K0 #V0 #H1KL1 #_ #H destruct - elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct - /2 width=4 by fqu_lref_O, ex3_intro/ -| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (ldrop_O1_le (e+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → - ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). -#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e -[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H - /3 width=5 by ex3_intro, conj/ -| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct -| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H - elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct - lapply (ysucc_inv_Y_dx … He) -He #He - elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/ -| #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H - elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct - elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/ -] -qed-. - -lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → - ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). -/2 width=1 by leq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc deleted file mode 100644 index 998f89e14..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc +++ /dev/null @@ -1,22 +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/computation/lpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -(* Main properties **********************************************************) - -theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G). -/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc deleted file mode 100644 index 206566071..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSn $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc deleted file mode 100644 index aef4f2707..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStar $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc deleted file mode 100644 index 9682647cd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma new file mode 100644 index 000000000..55c37a8fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )" + non associative with precedence 45 + for @{ 'LazyCoSN $h $g $d $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma new file mode 100644 index 000000000..206566071 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSn $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma new file mode 100644 index 000000000..aef4f2707 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStar $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma new file mode 100644 index 000000000..9682647cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStarAlt $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma new file mode 100644 index 000000000..b10b13a28 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predsn_5.ma". +include "basic_2/reduction/lpr.ma". +include "basic_2/reduction/cpx.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝ + λh,g,G. lpx_sn (cpx h g G). + +interpretation "extended parallel reduction (local environment, sn variant)" + 'PRedSn h g G L1 L2 = (lpx h g G L1 L2). + +(* Basic inversion lemmas ***************************************************) + +lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & + L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & + L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +lemma lpx_inv_pair: ∀h,g,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ➡[h, g] L2.ⓑ{I2}V2 → + ∧∧ ⦃G, L1⦄ ⊢ ➡[h, g] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h, g] V2 & I1 = I2. +/2 width=1 by lpx_sn_inv_pair/ qed-. + +(* Basic properties *********************************************************) + +lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L. +/2 width=1 by lpx_sn_refl/ qed. + +lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 → + ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2. +/2 width=1 by lpx_sn_pair/ qed. + +lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2. +#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|. +/2 width=2 by lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma new file mode 100644 index 000000000..f9c2374c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa_lift.ma". +include "basic_2/static/lsuba_aaa.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on atomic arity assignment for terms **************************) + +(* Note: lemma 500 *) +lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #g #L1 #k #X #H + elim (cpx_inv_sort1 … H) -H // * // +| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 + elim (cpx_inv_lref1 … H) -H + [ #H destruct + elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 + elim (lpx_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/ + | * #J #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2 + elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + /3 width=8 by aaa_lift, ldrop_fwd_drop2/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpx_inv_abbr1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/ + | #T2 #HT12 #HT2 #H destruct -IHV1 + /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=1 by lpx_pair, aaa_abst/ +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpx_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ + | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct + lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 + lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct + /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ + | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct + lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2 + lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ + ] +| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (cpx_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ + | -IHV1 /2 width=1 by/ + | -IHT1 /2 width=1 by/ + ] +] +qed-. + +lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/2 width=7 by aaa_cpx_lpx_conf/ qed-. + +lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/2 width=7 by aaa_cpx_lpx_conf/ qed-. + +lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. + +lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma new file mode 100644 index 000000000..e24b05283 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpx_sn_ldrop.ma". +include "basic_2/reduction/cpx_lift.ma". +include "basic_2/reduction/lpx.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properies on local environment slicing ***********************************) + +lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G). +/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. + +lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G). +/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-. + +lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G). +/2 width=3 by lpx_sn_dropable/ qed-. + +(* Properties on supclosure *************************************************) + +lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/ +[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H + #K2 #W2 #HLK2 #HVW2 #H destruct + /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12 + elim (ldrop_lpx_trans … HLK1 … HK12) -HK12 + /3 width=7 by fqu_drop, ex3_2_intro/ +] +qed-. + +lemma fquq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/ +[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H + #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1) + /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01 + elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1 + /3 width=5 by fqu_drop, ex3_2_intro/ +] +qed-. + +lemma lpx_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H +[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma new file mode 100644 index 000000000..d3f594317 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_ldrop.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on lazy equivalence for local environments ********************) + +axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → + ∀L1,T,d. L1 ⋕[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. + +lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (ldrop_O1_le (e+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (ldrop_fwd_length_le2 … HL1) -L -T1 -g + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma index 7dec554c7..a2f332a69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/xoa/xoa2.ma". include "basic_2/notation/relations/lazyor_4.ma". include "basic_2/relocation/lpx_sn_alt.ma". @@ -56,45 +57,84 @@ qed-. (* Alternative definition ***************************************************) -lemma llor_intro_alt_eq: ∀T,L2,L1,L. |L1| = |L2| → |L1| = |L| → - (∀I1,I,K1,K,V1,V,U,i. ⇧[i, 1] U ≡ T → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → - ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K - ) → - (∀I1,I2,I,K1,K2,K,V1,V2,V,i. (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ⇩[i] L ≡ K.ⓑ{I}V → ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K - ) → L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 #L #HL12 #HL1 #IH1 #IH2 @lpx_sn_intro_alt // -HL1 +(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) +lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. +#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // +qed-. + +fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y. +/2 width=1 by plus_minus_minus_be/ qed-. + +lemma llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| → + (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → + (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → + ∧∧ I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K + ) ∧ + (∀I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) → + ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K + ) + ) → L1 ⩖[T] L2 ≡ L. +#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK lapply (ldrop_fwd_length_minus4 … HLK1) lapply (ldrop_fwd_length_le4 … HLK1) -normalize >HL12 HL12