From 890a19d326338d96879dedce1eadc7c91a3beac2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 10 Apr 2014 20:50:46 +0000 Subject: [PATCH] - 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 --- .../basic_2/computation/cpxs_cpxs.ma | 36 ++---- .../basic_2/computation/cpxs_lift.ma | 5 +- .../basic_2/computation/csx_fpbs.ma | 1 + .../basic_2/computation/csx_llpx.ma | 119 +----------------- .../csx_lpx.etc => computation/csx_lpx.ma} | 0 .../csx_lpxs.etc => computation/csx_lpxs.ma} | 0 .../basic_2/computation/csx_tstc_vector.ma | 2 +- .../basic_2/computation/fpbs_alt.ma | 2 +- .../basic_2/computation/fpbs_lift.ma | 4 +- .../basic_2/computation/llpxs_cpxs.ma | 16 +-- .../basic_2/computation/llsx_csx.ma | 1 + .../lpx_sn/lpxs.etc => computation/lpxs.ma} | 10 +- .../lpxs_aaa.etc => computation/lpxs_aaa.ma} | 4 +- .../lpxs_alt.etc => computation/lpxs_alt.ma} | 0 .../lpxs_cpxs.ma} | 11 +- .../lpxs_ldrop.ma} | 0 .../lpxs_lleq.ma} | 2 +- .../lpxs_lpxs.ma} | 2 +- .../relations/lazycosn_5.ma} | 0 .../relations/predsn_5.ma} | 0 .../relations/predsnstar_5.ma} | 0 .../relations/predsnstaralt_5.ma} | 0 .../{etc/lpx_sn/lpx.etc => reduction/lpx.ma} | 0 .../lpx_aaa.etc => reduction/lpx_aaa.ma} | 0 .../lpx_ldrop.etc => reduction/lpx_ldrop.ma} | 2 +- .../lpx_lleq.etc => reduction/lpx_lleq.ma} | 25 +--- .../lambdadelta/basic_2/relocation/llor.ma | 92 ++++++++++---- .../basic_2/relocation/llpx_sn_alt.ma | 102 +++++++++------ .../basic_2/relocation/lpx_sn_alt.ma | 85 ++++++++----- .../basic_2/substitution/lleq_alt.ma | 17 ++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 +- 31 files changed, 254 insertions(+), 292 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/csx_lpx.etc => computation/csx_lpx.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/csx_lpxs.etc => computation/csx_lpxs.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs.etc => computation/lpxs.ma} (95%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_aaa.etc => computation/lpxs_aaa.ma} (95%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_alt.etc => computation/lpxs_alt.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_cpxs.etc => computation/lpxs_cpxs.ma} (94%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_ldrop.etc => computation/lpxs_ldrop.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_lleq.etc => computation/lpxs_lleq.ma} (99%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpxs_lpxs.etc => computation/lpxs_lpxs.ma} (97%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lazycosn_5.etc => notation/relations/lazycosn_5.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsn_5.etc => notation/relations/predsn_5.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsnstar_5.etc => notation/relations/predsnstar_5.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsnstaralt_5.etc => notation/relations/predsnstaralt_5.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx.etc => reduction/lpx.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_aaa.etc => reduction/lpx_aaa.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_ldrop.etc => reduction/lpx_ldrop.ma} (98%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_lleq.etc => reduction/lpx_lleq.ma} (82%) 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/etc/lpx_sn/csx_lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpx.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/csx_lpxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpxs.ma 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/etc/lpx_sn/lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma index 35a8cb482..ee557e438 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma @@ -43,19 +43,19 @@ qed-. (* Basic properties *********************************************************) lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. -/3 width=3/ qed. +/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/ qed. +/2 width=1 by inj/ qed. lemma lpxs_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡*[h, g] L. -/2 width=1/ qed. +/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/ qed. +/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/ qed. +/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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma index 80c43c731..89122eb55 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_aaa.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma @@ -27,6 +27,4 @@ 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-. +/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma index 2f21a8d70..1dfb297e7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -36,11 +36,14 @@ lemma lpxs_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, g] K2.ⓑ{I}V (* 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_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-. -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-. +(* 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_ldrop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index e21c79912..2f9b322db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lleq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_leq.ma". +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". diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma index 998f89e14..1d287d368 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_lpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lpxs.ma @@ -19,4 +19,4 @@ include "basic_2/computation/lpxs.ma". (* Main properties **********************************************************) theorem lpxs_trans: ∀h,g,G. Transitive … (lpxs h g G). -/2 width=3/ qed-. +/2 width=3 by trans_TC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lazycosn_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazycosn_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma index 188e8d11b..e24b05283 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/ldrop_lpx_sn.ma". +include "basic_2/relocation/lpx_sn_ldrop.ma". include "basic_2/reduction/cpx_lift.ma". include "basic_2/reduction/lpx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma similarity index 82% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index 353f810c3..d3f594317 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,37 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_ldrop.ma". +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 ********************) -(* -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 → 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