From 82fc9726cbd3363dcd08695dbe0179653e6a18a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 30 Mar 2014 19:47:08 +0000 Subject: [PATCH] update of the partial commit: we move lleq to the "substitution" component --- .../lpx_sn/btpredsnstar_8.etc} | 0 .../basic_2/etc/lpx_sn/csx_lpx.etc | 138 ++++++++++++++++ .../basic_2/etc/lpx_sn/csx_lpxs.etc | 25 +++ .../basic_2/etc/lpx_sn/fpbu_fpns.etc | 77 +++++++++ .../lambdadelta/basic_2/etc/lpx_sn/fpns.etc | 39 +++++ .../fquq_lleq.ma => etc/lpx_sn/fpns_fpns.etc} | 20 ++- .../basic_2/etc/lpx_sn/lprs_cprs.etc | 136 ++++++++++++++++ .../lambdadelta/basic_2/etc/lpx_sn/lpxs.etc | 74 +++++++++ .../fqup_lleq.ma => etc/lpx_sn/lpxs_aaa.etc} | 28 ++-- .../basic_2/etc/lpx_sn/lpxs_alt.etc | 47 ++++++ .../basic_2/etc/lpx_sn/lpxs_cpxs.etc | 147 ++++++++++++++++++ .../lpx_sn/lpxs_ldrop.etc} | 24 +-- .../basic_2/etc/lpx_sn/lpxs_lleq.etc | 125 +++++++++++++++ .../basic_2/etc/lpx_sn/lpxs_lpxs.etc | 22 +++ .../basic_2/notation/relations/lazyeq_7.ma | 19 +++ .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 2 +- .../lambdadelta/basic_2/reduction/fpb.ma | 6 +- .../basic_2/reduction/llpx_lleq.ma | 3 + .../basic_2/relocation/llpx_sn_tc.ma | 26 ++++ .../lambdadelta/basic_2/substitution/fleq.ma | 43 +++++ .../basic_2/substitution/fleq_fleq.ma | 34 ++++ .../{relocation => substitution}/lleq.ma | 6 + .../fqu_lleq.ma => substitution/lleq_fqus.ma} | 38 ++++- .../lleq_ldrop.ma | 2 +- .../{relocation => substitution}/lleq_leq.ma | 2 +- .../{relocation => substitution}/lleq_lleq.ma | 2 +- .../contribs/lambdadelta/ground_2/lib/star.ma | 22 +++ 27 files changed, 1059 insertions(+), 48 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/btpredsnstar_8.ma => etc/lpx_sn/btpredsnstar_8.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc rename matita/matita/contribs/lambdadelta/basic_2/{relocation/fquq_lleq.ma => etc/lpx_sn/fpns_fpns.etc} (62%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution/fqup_lleq.ma => etc/lpx_sn/lpxs_aaa.etc} (57%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc rename matita/matita/contribs/lambdadelta/basic_2/{substitution/fqus_lleq.ma => etc/lpx_sn/lpxs_ldrop.etc} (61%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lleq.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/fqu_lleq.ma => substitution/lleq_fqus.ma} (55%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lleq_ldrop.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lleq_leq.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/lleq_lleq.ma (97%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredsnstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredsnstar_8.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc 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 new file mode 100644 index 000000000..f8bf3c475 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc @@ -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/etc/lpx_sn/csx_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc new file mode 100644 index 000000000..d49b6e7ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc @@ -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/etc/lpx_sn/fpbu_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc new file mode 100644 index 000000000..863b08196 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lleq.ma". +include "basic_2/computation/cpxs_lleq.ma". +include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/computation/lpxs_lpxs.ma". +include "basic_2/computation/fpns.ma". +include "basic_2/computation/fpbs_alt.ma". +include "basic_2/computation/fpbu.ma". + +(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +lemma fpns_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⊢ ⋕➡*[h, g] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, U2⦄. +#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 +#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2 +[ #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2 + /3 width=5 by fpbu_fqup, fpns_intro, ex2_3_intro/ +| /4 width=9 by fpbu_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/ +| /5 width=5 by fpbu_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/ +] +qed-. + +lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨ + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H + [ /4 width=1 by fpbu_fqup, fqu_fqup, or_intror/ + | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/ + ] +| #T2 #HT12 elim (eq_term_dec T1 T2) + #HnT12 destruct /4 width=1 by fpbu_cpxs, cpx_cpxs, or_intror, or_introl/ +| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0) + /4 width=3 by fpbu_lpxs, fpns_intro, lpx_lpxs, or_intror, or_introl/ +] +qed-. + +lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +(* ALTERNATIVE PROOF +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 +[ /2 width=1 by or_introl/ +| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] + elim (fpb_fpbu … H1) -H1 #H1 + [ /3 width=1 by +*) +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H +#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #HT2 @or_intror + /5 width=9 by fpbsa_inv_fpbs, fpbu_fqup, ex3_2_intro, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H + [ /3 width=1 by fpns_intro, or_introl/ + | /5 width=5 by fpbu_lpxs, ex2_3_intro, or_intror/ + ] + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=9 by fpbsa_inv_fpbs, fpbu_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc new file mode 100644 index 000000000..dce46b065 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btpredsnstar_8.ma". +include "basic_2/relocation/lleq.ma". +include "basic_2/computation/lpxs.ma". + +(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) + +inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝ +| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, 0] L2 → fpns h g G L1 T G L2 T +. + +interpretation + "computation for 'big tree' normal forms (closure)" + 'BTPRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g). +/2 width=1 by fpns_intro/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1, 0] L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc similarity index 62% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc index 880c387e4..deaa7a967 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc @@ -12,18 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/relocation/fqu_lleq.ma". -include "basic_2/relocation/fquq_alt.ma". +include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/computation/lpxs_lpxs.ma". +include "basic_2/computation/fpns.ma". -(* OPTIONAL SUPCLOSURE ******************************************************) +(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) -(* Properties on lazy equivalence for local environments ********************) +(* Main properties **********************************************************) -lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H -[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] +theorem fpns_trans: ∀h,g. tri_transitive … (fpns h g). +#h #g #G1 #G #L1 #L #T1 #T * -G -L -T +#L #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 +/3 width=3 by lpxs_trans, lleq_trans, fpns_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc new file mode 100644 index 000000000..70345be5c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc @@ -0,0 +1,136 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cprs_cprs.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Advanced properties ******************************************************) + +lemma lprs_pair: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → + ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2. +/2 width=1 by TC_lpx_sn_pair/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lprs_inv_pair1: ∀I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡* L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 & + L2 = K2.ⓑ{I}V2. +/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-. + +lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 & + L1 = K1.ⓑ{I}V1. +/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-. + +(* Properties on context-sensitive parallel computation for terms ***********) + +lemma lprs_cpr_trans: ∀G. s_r_trans … (cpr G) (lprs G). +/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-. + +(* Basic_1: was just: pr3_pr3_pr3_t *) +lemma lprs_cprs_trans: ∀G. s_rs_trans … (cpr G) (lprs G). +/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-. + +lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1 +[ #L1 #HL01 + elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3 by ex2_intro/ +| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0 + elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12 + elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03 + elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3 + lapply (cprs_trans … HT03 … HT3) -T3 + lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3 by ex2_intro/ +] +qed-. + +lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-. + +lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #HT01 #L1 #HL01 +elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1 +lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3 by ex2_intro/ +qed-. + +lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-. + +lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by lprs_pair, cprs_bind/ +qed. + +(* Inversion lemmas on context-sensitive parallel computation for terms *****) + +(* Basic_1: was: pr3_gen_abst *) +lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 → + ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 & + U2 = ⓛ{a}W2.T2. +#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/ +#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct +elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct +lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 +lapply (cprs_strap1 … HV10 … HV02) -V0 +lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5 by ex3_2_intro/ +qed-. + +lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 → + ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2. +#a #G #L #W1 #W2 #T1 #T2 #H +elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/ +qed-. + +(* Basic_1: was pr3_gen_abbr *) +lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & + U2 = ⓓ{a}V2.T2 + ) ∨ + ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. +#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 + lapply (cprs_strap1 … HV10 … HV02) -V0 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5 by ex3_2_intro, or_introl/ + | #T2 #HT02 #HUT2 + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1 by lprs_pair/ -V0 #HT02 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3 by ex3_intro, or_intror/ + ] +| #U1 #HTU1 #HU01 + elim (lift_total U2 0 1) #U #HU2 + lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 + /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/ +] +qed-. + +(* More advanced properties *************************************************) + +lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → + ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2. +/3 width=3 by lprs_pair, lprs_cprs_trans/ 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 new file mode 100644 index 000000000..35a8cb482 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc @@ -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/ 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/substitution/fqup_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc similarity index 57% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc index c0bfa41fe..80c43c731 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc @@ -12,21 +12,21 @@ (* *) (**************************************************************************) -include "basic_2/relocation/fqu_lleq.ma". -include "basic_2/substitution/fqup.ma". +include "basic_2/reduction/lpx_aaa.ma". +include "basic_2/computation/lpxs.ma". -(* PLUS-ITERATED SUPCLOSURE *************************************************) +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) -(* Properties on lazy equivalence for local environments ********************) +(* Properties about atomic arity assignment on terms ************************) -lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U -[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 - /3 width=3 by fqu_fqup, ex2_intro/ -| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 - #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K - /3 width=5 by fqup_strap1, ex2_intro/ -] +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 new file mode 100644 index 000000000..8a6b30a57 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc @@ -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/etc/lpx_sn/lpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc new file mode 100644 index 000000000..2f21a8d70 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc @@ -0,0 +1,147 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/fqus_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc index ae209399f..d8c489017 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc @@ -12,18 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fqup_lleq.ma". -include "basic_2/substitution/fqus_alt.ma". +include "basic_2/reduction/lpx_ldrop.ma". +include "basic_2/computation/lpxs.ma". -(* STAR-ITERATED SUPCLOSURE *************************************************) +(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) -(* Properties on lazy equivalence for local environments ********************) +(* Properies on local environment slicing ***********************************) -lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H -[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] -qed-. +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 new file mode 100644 index 000000000..e21c79912 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc @@ -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/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 new file mode 100644 index 000000000..998f89e14 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc @@ -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/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma new file mode 100644 index 000000000..3c6f5e75e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.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 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 d ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyEq $d $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index 77dce4631..b34d4e955 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_ldrop.ma". +include "basic_2/substitution/lleq_ldrop.ma". include "basic_2/reduction/cpx_llpx_sn.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 7c65dcfa9..0a7705e3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -21,7 +21,7 @@ include "basic_2/reduction/llpx.ma". inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 | fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 -| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_llpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation @@ -36,5 +36,5 @@ lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g). lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. /3 width=1 by fpb_cpx, cpr_cpx/ qed. -lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpb_lpx, llpr_llpx/ qed. +lemma llpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpb_llpx, llpr_llpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma index bc8619d66..e936cc531 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma @@ -19,6 +19,9 @@ include "basic_2/reduction/llpx.ma". (* Properties on lazy equivalence for local environments ********************) +lemma llpx_lrefl: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2. +/2 width=1 by llpx_sn_lrefl/ qed-. + lemma lleq_llpx_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀L.⦃G, L2⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L. /3 width=3 by lleq_cpx_trans, lleq_llpx_sn_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma new file mode 100644 index 000000000..e09fe8889 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llpx_sn_ldrop.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Properties about transitive closure **************************************) + +lemma llpx_sn_TC_pair_dx: ∀R. (∀L. reflexive … (R L)) → + ∀I,L,V1,V2,T. LTC … R L V1 V2 → + LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2). +#R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2 +/4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma new file mode 100644 index 000000000..bb55c859f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyeq_7.ma". +include "basic_2/grammar/genv.ma". +include "basic_2/substitution/lleq.ma". + +(* LAZY EQUIVALENCE FOR CLOSURES ********************************************) + +inductive fleq (d) (G) (L1) (T): relation3 genv lenv term ≝ +| fleq_intro: ∀L2. L1 ⋕[T, d] L2 → fleq d G L1 T G L2 T +. + +interpretation + "lazy equivalence (closure)" + 'LazyEq d G1 L1 T1 G2 L2 T2 = (fleq d G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma fleq_refl: ∀d. tri_reflexive … (fleq d). +/2 width=1 by fleq_intro/ qed. + +lemma fleq_sym: ∀d. tri_symmetric … (fleq d). +#d #G1 #L1 #T1 #G2 #L2 #T2 * /3 width=1 by fleq_intro, lleq_sym/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma fleq_inv_gen: ∀G1,G2,L1,L2,T1,T2,d. ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ⋕[T1, d] L2 & T1 = T2. +#G1 #G2 #L1 #L2 #T1 #T2 #d * -G2 -L2 -T2 /2 width=1 by and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma new file mode 100644 index 000000000..36885f0e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lleq.ma". +include "basic_2/substitution/fleq.ma". + +(* LAZY EQUIVALENCE FOR CLOSURES *******************************************) + +(* Main properties **********************************************************) + +theorem fleq_trans: ∀d. tri_transitive … (fleq d). +#d #G1 #G #L1 #L #T1 #T * -G -L -T +#L #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 +/3 width=3 by lleq_trans, fleq_intro/ +qed-. + +theorem fleq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2,d. + ⦃G, L, T⦄ ⋕[d] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ⋕[d] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄. +/3 width=5 by fleq_trans, fleq_sym/ qed-. + +theorem fleq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T,d. + ⦃G1, L1, T1⦄ ⋕[d] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ⋕[d] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄. +/3 width=5 by fleq_trans, fleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index b431e0d18..7d0f68927 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -152,3 +152,9 @@ lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → L1 ⋕[ⓑ{a,I}V.T, 0] L2. /2 width=1 by llpx_sn_bind_O/ qed-. + +(* Advancded properties on lazy pointwise exyensions ************************) + +lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2,T,d. L1 ⋕[T, d] L2 → llpx_sn R d T L1 L2. +/2 width=3 by llpx_sn_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma similarity index 55% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma index b4235ba93..b02d065da 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_ldrop.ma". -include "basic_2/relocation/fqu.ma". +include "basic_2/substitution/fqus_alt.ma". +include "basic_2/substitution/lleq_ldrop.ma". -(* SUPCLOSURE ***************************************************************) +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -(* Properties on lazy equivalence for local environments ********************) +(* Properties on supclosure *************************************************) lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ → ∀L1. L1 ⋕[T, 0] L2 → @@ -43,3 +43,33 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ ] ] qed-. + +lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H +[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U +[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 + /3 width=3 by fqu_fqup, ex2_intro/ +| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 + #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K + /3 width=5 by fqup_strap1, ex2_intro/ +] +qed-. + +lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H +[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma index 299412217..27b16110d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/llpx_sn_ldrop.ma". -include "basic_2/relocation/lleq.ma". +include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma index 081301a52..01bde31ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/relocation/llpx_sn_leq.ma". -include "basic_2/relocation/lleq.ma". +include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma index a99b1e2f3..a3a276ff3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_ldrop.ma". +include "basic_2/substitution/lleq_ldrop.ma". (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index 50fda9065..9bbecddca 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -178,6 +178,28 @@ lemma s_r_trans_LTC2: ∀A,B,S,R. s_rs_transitive A B S R → s_r_transitive A B #A #B #S #R #HSR #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /3 width=3 by inj/ qed-. +lemma s_r_to_s_rs_trans: ∀A,B,S,R. s_r_transitive A B (LTC … S) R → + s_rs_transitive A B S R. +#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1 +elim (TC_idem … (S L1) … T1 T2) +#_ #H @H @HSR // +qed-. + +lemma s_rs_to_s_r_trans: ∀A,B,S,R. s_rs_transitive A B S R → + s_r_transitive A B (LTC … S) R. +#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1 +elim (TC_idem … (S L1) … T1 T2) +#H #_ @H @HSR // +qed-. + +lemma s_rs_trans_TC1: ∀A,B,S,R. s_rs_transitive A B S R → + s_rs_transitive A B (LTC … S) R. +#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1 +elim (TC_idem … (S L1) … T1 T2) +elim (TC_idem … (S L2) … T1 T2) +#_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/ +qed-. + (* relations on unboxed pairs ***********************************************) lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R → -- 2.39.2