From 07d915d411ffabeb0c7cd678f00cbeca53ae8276 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 15 Apr 2014 18:06:55 +0000 Subject: [PATCH] - lazy extended reduction parked - fpns finally removed - "big tree" computation based again on "full" extended reduction but improved with lazy equivalence for local environments - llor parked for now (something to fix there) --- .../basic_2/computation/cpxs_aaa.ma | 2 +- .../basic_2/computation/cpxs_tstc.ma | 2 +- .../basic_2/computation/csx_fpbs.ma | 6 +- .../fpns_fpns.etc => computation/csx_lleq.ma} | 21 +-- .../lambdadelta/basic_2/computation/fpbc.ma | 2 +- .../basic_2/computation/fpbg_fpbg.ma | 1 - .../lambdadelta/basic_2/computation/fpbs.ma | 79 ++++++----- .../basic_2/computation/fpbs_alt.ma | 52 +++++--- .../basic_2/computation/fpbs_ext.ma | 14 +- .../basic_2/computation/fpbs_fleq.ma | 3 +- .../basic_2/computation/fpbs_fpbs.ma | 2 +- .../basic_2/computation/fpbs_lift.ma | 7 + .../lambdadelta/basic_2/computation/fpbu.ma | 19 ++- .../basic_2/computation/fpbu_fleq.ma | 18 +-- .../basic_2/computation/fpbu_lleq.ma | 6 +- .../basic_2/computation/fsb_csx.ma | 12 +- .../basic_2/computation/lpxs_lleq.ma | 1 - .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 1 + .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 1 - .../basic_2/dynamic/snv_lsstas_lpr.ma | 1 - .../cpxs_llpx.ma => etc/llpx/cpxs_llpx.etc} | 0 .../csx_llpx.ma => etc/llpx/csx_llpx.etc} | 0 .../csx_llpxs.ma => etc/llpx/csx_llpxs.etc} | 0 .../fpbs_lpr.ma => etc/llpx/fpbs_lpr.etc} | 0 .../llpx/lazypredsn_7.etc} | 0 .../llpx/lazypredsnstar_7.etc} | 0 .../lazysn_6.ma => etc/llpx/lazysn_6.etc} | 0 .../llpx/lazysnalt_6.etc} | 0 .../{reduction/llpx.ma => etc/llpx/llpx.etc} | 0 .../llpx_aaa.ma => etc/llpx/llpx_aaa.etc} | 0 .../llpx_ldrop.ma => etc/llpx/llpx_ldrop.etc} | 0 .../llpx_lleq.ma => etc/llpx/llpx_lleq.etc} | 0 .../llpx_lpr.ma => etc/llpx/llpx_lpr.etc} | 0 .../llpxs.ma => etc/llpx/llpxs.etc} | 0 .../llpxs_aaa.ma => etc/llpx/llpxs_aaa.etc} | 0 .../llpxs_cpxs.ma => etc/llpx/llpxs_cpxs.etc} | 0 .../llpxs_lleq.ma => etc/llpx/llpxs_lleq.etc} | 0 .../llpx/llpxs_llpxs.etc} | 0 .../llpxs_lprs.ma => etc/llpx/llpxs_lprs.etc} | 0 .../llsx.ma => etc/llpx/llsx.etc} | 0 .../llsx_alt.ma => etc/llpx/llsx_alt.etc} | 0 .../llsx_csx.ma => etc/llpx/llsx_csx.etc} | 2 +- .../llsx_ldrop.ma => etc/llpx/llsx_ldrop.etc} | 0 .../llsx_llpx.ma => etc/llpx/llsx_llpx.etc} | 0 .../llsx_llpxs.ma => etc/llpx/llsx_llpxs.etc} | 0 .../basic_2/etc/lpx_sn/btpredsnstar_8.etc | 19 --- .../basic_2/etc/lpx_sn/fpbc_fpns.etc | 34 ----- .../basic_2/etc/lpx_sn/fpbg_fpns.etc | 78 ----------- .../basic_2/etc/lpx_sn/fpbu_fpns.etc | 77 ----------- .../lambdadelta/basic_2/etc/lpx_sn/fpns.etc | 39 ------ .../lpx_sn/{fpbs_fpns.etc => lleq_llor.etc} | 26 ++-- .../llor.ma => etc/lpx_sn/llor.etc} | 0 .../basic_2/etc/lpx_sn/lpxs_llor.etc | 125 ++++++++++++++++++ .../lambdadelta/basic_2/reduction/fpb.ma | 13 +- .../lambdadelta/basic_2/reduction/fpb_aaa.ma | 5 +- .../lambdadelta/basic_2/static/aaa_lleq.ma | 42 ++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 11 +- 57 files changed, 348 insertions(+), 373 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/fpns_fpns.etc => computation/csx_lleq.ma} (61%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/cpxs_llpx.ma => etc/llpx/cpxs_llpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/csx_llpx.ma => etc/llpx/csx_llpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/csx_llpxs.ma => etc/llpx/csx_llpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/fpbs_lpr.ma => etc/llpx/fpbs_lpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazypredsn_7.ma => etc/llpx/lazypredsn_7.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazypredsnstar_7.ma => etc/llpx/lazypredsnstar_7.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazysn_6.ma => etc/llpx/lazysn_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazysnalt_6.ma => etc/llpx/lazysnalt_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpx.ma => etc/llpx/llpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpx_aaa.ma => etc/llpx/llpx_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpx_ldrop.ma => etc/llpx/llpx_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpx_lleq.ma => etc/llpx/llpx_lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpx_lpr.ma => etc/llpx/llpx_lpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs.ma => etc/llpx/llpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs_aaa.ma => etc/llpx/llpxs_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs_cpxs.ma => etc/llpx/llpxs_cpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs_lleq.ma => etc/llpx/llpxs_lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs_llpxs.ma => etc/llpx/llpxs_llpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llpxs_lprs.ma => etc/llpx/llpxs_lprs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx.ma => etc/llpx/llsx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx_alt.ma => etc/llpx/llsx_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx_csx.ma => etc/llpx/llsx_csx.etc} (98%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx_ldrop.ma => etc/llpx/llsx_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx_llpx.ma => etc/llpx/llsx_llpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llsx_llpxs.ma => etc/llpx/llsx_llpxs.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/{fpbs_fpns.etc => lleq_llor.etc} (56%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llor.ma => etc/lpx_sn/llor.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_llor.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma index 540d80d7e..4f054eac6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/llpx_aaa.ma". +include "basic_2/reduction/lpx_aaa.ma". include "basic_2/computation/cpxs.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma index 76b8cc8ad..eed76daea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/tstc.ma". -include "basic_2/computation/llpxs_cpxs.ma". +include "basic_2/computation/lpxs_cpxs.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) 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 53fe83271..6b7fcd333 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/computation/fpbs.ma". -include "basic_2/computation/csx_lift.ma". (* added *) -include "basic_2/computation/csx_llpx.ma". +include "basic_2/computation/csx_lleq.ma". +include "basic_2/computation/csx_lpx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) @@ -23,7 +23,7 @@ include "basic_2/computation/csx_llpx.ma". lemma csx_fpb_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2. #h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_llpx_conf/ +/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_lleq_conf/ qed-. lemma csx_fpbs_conf: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma index deaa7a967..d56acd9df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma @@ -12,16 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_lleq.ma". -include "basic_2/computation/lpxs_lpxs.ma". -include "basic_2/computation/fpns.ma". +include "basic_2/reduction/cpx_lleq.ma". +include "basic_2/computation/csx.ma". -(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) +(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -(* Main properties **********************************************************) +(* Properties on lazy equivalence for local environments ********************) -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/ +lemma csx_lleq_conf: ∀h,g,G,L1,T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → + ∀L2. L1 ⋕[T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L1 #T #H @(csx_ind … H) -T +/4 width=6 by csx_intro, cpx_lleq_conf_dx, lleq_cpx_trans/ qed-. + +lemma csx_lleq_trans: ∀h,g,G,L1,L2,T. + L1 ⋕[T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T → ⦃G, L1⦄ ⊢ ⬊*[h, g] T. +/3 width=3 by csx_lleq_conf, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma index 4656f8431..bf9baaa90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma @@ -20,7 +20,7 @@ include "basic_2/computation/fpbu.ma". definition fpbc: ∀h. sd h → tri_relation genv lenv term ≝ λh,g,G1,L1,T1,G2,L2,T2. - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ . + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄. interpretation "single-step 'big tree' proper parallel reduction (closure)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index 9cf029f09..f423aaecd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -49,4 +49,3 @@ lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). /2 width=5 by tri_TC_transitive/ qed-. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 87d1d71d8..193638ce2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/btpredstar_8.ma". include "basic_2/substitution/fqus.ma". include "basic_2/reduction/fpb.ma". include "basic_2/computation/cpxs.ma". -include "basic_2/computation/llpxs.ma". +include "basic_2/computation/lpxs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) @@ -72,17 +72,20 @@ lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, /3 width=5 by fpb_cpx, fpbs_strap1/ qed. -lemma llpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g, T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -#h #g #G #L1 #L2 #T #H @(llpxs_ind … H) -L2 -/3 width=5 by fpb_llpx, fpbs_strap1/ +lemma lpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +#h #g #G #L1 #L2 #T #H @(lpxs_ind … H) -L2 +/3 width=5 by fpb_lpx, fpbs_strap1/ qed. +lemma lleq_fpbs: ∀h,g,G,L1,L2,T. L1 ⋕[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpb_fpbs, fpb_lleq/ qed. + lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. /3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. -(* -lamma llprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -/3 width=1 by llprs_llpxs, llpxs_fpbs/ qed. -*) + +lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +/3 width=1 by lprs_lpxs, lpxs_fpbs/ qed. + lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2 @@ -99,27 +102,15 @@ lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G /3 width=5 by fpbs_strap1, fpb_cpx/ qed-. -lemma fpbs_llpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → - ⦃G, L⦄ ⊢ ➡*[h, g, T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. -#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(llpxs_ind … H) -L2 -/3 width=5 by fpbs_strap1, fpb_llpx/ +lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. +#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2 +/3 width=5 by fpbs_strap1, fpb_lpx/ qed-. -lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → - ⦃G1, L1, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. - -lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → - ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed-. - -lemma fqus_llpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T2⦄ → - ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/3 width=3 by fpbs_llpxs_trans, fqus_fpbs/ qed. - -lemma cpxs_fqus_llpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → - ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by cpxs_fqus_fpbs, fpbs_llpxs_trans/ qed. +lemma fpbs_lleq_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + L ⋕[T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. +/3 width=5 by fpbs_strap1, fpb_lleq/ qed-. lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. @@ -133,8 +124,34 @@ lemma cpxs_fpbs_trans: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, g] ⦃ /3 width=5 by fpbs_strap2, fpb_cpx/ qed-. -lemma llpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ➡*[h, g, T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(llpxs_ind_dx … H) -L1 -/3 width=5 by fpbs_strap2, fpb_llpx/ +lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ➡*[h, g] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1 +/3 width=5 by fpbs_strap2, fpb_lpx/ qed-. + +lemma lleq_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + L1 ⋕[T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_strap2, fpb_lleq/ qed-. + +lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → + ⦃G1, L1, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed. + +lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → + ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed. + +lemma fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T2⦄ → + ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=3 by fpbs_lpxs_trans, fqus_fpbs/ qed. + +lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → + ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed. + +(* Note: this is used in the closure proof *) +lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. +/4 width=5 by fpbs_strap1, fpb_fpbs, lpr_fpb, cpr_fpb/ +qed. 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 cf39bffcc..f74199390 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -13,17 +13,20 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstaralt_8.ma". -include "basic_2/computation/llpxs_cpxs.ma". -include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/substitution/lleq_fqus.ma". +include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/computation/cpxs_lleq.ma". +include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/computation/fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) (* Note: alternative definition of fpbs *) definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ λh,g,G1,L1,T1,G2,L2,T2. - ∃∃L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T & - ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ & - ⦃G2, L⦄ ⊢ ➡*[h, g, T2, 0] L2. + ∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T & + ⦃G1, L1, T⦄ ⊃* ⦃G2, L0, T2⦄ & + ⦃G2, L0⦄ ⊢ ➡*[h, g] L & L ⋕[T2, 0] L2. interpretation "'big tree' parallel computation (closure) alternative" 'BTPRedStarAlt h g G1 L1 T1 G2 L2 T2 = (fpbsa h g G1 L1 T1 G2 L2 T2). @@ -32,15 +35,19 @@ interpretation "'big tree' parallel computation (closure) alternative" lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ] -#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02 +#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 | #L #HL1 ] +#G2 #L2 #T2 * #L00 #L0 #T0 #HT0 #HG2 #HL00 #HL02 [ 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 (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/ + /3 width=7 by fqus_strap2, ex4_3_intro/ +| /3 width=7 by cpxs_strap2, ex4_3_intro/ +| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 #HT10 + elim (lpx_fqus_trans … HG2 … HL1) -L + /3 width=7 by lpxs_strap2, cpxs_trans, ex4_3_intro/ +| lapply (lleq_cpxs_trans … HT0 … HL1) -HT0 #HT0 + lapply (cpxs_lleq_conf_sn … HT0 … HL1) -HL1 #HL1 + elim (lleq_fqus_trans … HG2 … HL1) -L #K00 #HG12 #HKL00 + elim (lleq_lpxs_trans … HL00 … HKL00) -L00 + /3 width=9 by lleq_trans, ex4_3_intro/ ] qed-. @@ -49,7 +56,7 @@ qed-. theorem fpbs_fpbsa: ∀h,g,G1,G2,L1,L2,T1,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 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 -/2 width=5 by fpb_fpbsa_trans, ex3_2_intro/ +/2 width=7 by fpb_fpbsa_trans, ex4_3_intro/ qed. (* Main inversion lemmas ****************************************************) @@ -57,5 +64,20 @@ qed. theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,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 * -/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, llpxs_fpbs/ +/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpb_lleq/ qed-. + +(* Advanced properties ******************************************************) + +lemma fpbs_intro_alt: ∀h,g,G1,G2,L1,L0,L,L2,T1,T,T2. + ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃* ⦃G2, L0, T2⦄ → + ⦃G2, L0⦄ ⊢ ➡*[h, g] L → L ⋕[T2, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ . +/3 width=7 by fpbsa_inv_fpbs, ex4_3_intro/ qed. + +(* Advanced inversion lemmas *************************************************) + +lemma fpbs_inv_alt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T & + ⦃G1, L1, T⦄ ⊃* ⦃G2, L0, T2⦄ & + ⦃G2, L0⦄ ⊢ ➡*[h, g] L & L ⋕[T2, 0] L2. +/2 width=1 by fpbs_fpbsa/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma index 8ae11770f..8aedee009 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma @@ -21,11 +21,11 @@ include "basic_2/computation/fpbs_alt.ma". lemma fpbs_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_fpbsa … H) -H -#L0 #T0 #HT10 #H10 #HL02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU2 ] -[ #H destruct lapply (llpxs_cpxs_trans … HTU2 … HL02) - #H elim (fqus_cpxs_trans_neq … H10 … H HnTU2) -H10 -H -HnTU2 - /4 width=8 by fqus_llpxs_fpbs, llpxs_cpxs_conf_dx, ex3_intro/ -| /4 width=6 by fpbs_cpxs_trans, fqus_llpxs_fpbs, ex3_intro/ -] +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_inv_alt … H) -H +#L00 #L0 #T0 #HT10 #H10 #HL00 #HL02 lapply (lleq_cpxs_trans … HTU2 … HL02) -HTU2 +#HTU2 lapply (cpxs_lleq_conf_sn … HTU2 … HL02) -HL02 +#HL02 lapply (lpxs_cpxs_trans … HTU2 … HL00) -HTU2 +#HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -H10 -HTU2 -HnTU2 +#U0 #HTU0 #HnTU0 #HU02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU0 ] +[ #H destruct ] /3 width=10 by fpbs_intro_alt, ex3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma index 3823dfbd0..eb0bc4d2b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/substitution/fleq.ma". -include "basic_2/computation/llpxs_lleq.ma". include "basic_2/computation/fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) @@ -22,5 +21,5 @@ include "basic_2/computation/fpbs.ma". lemma fleq_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=1 by llpxs_fpbs, llpxs_lrefl/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by lleq_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma index 0a9f3af8c..e821fe561 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_lift.ma". +include "basic_2/computation/fpbs_alt.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) 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 4895dccf5..ab8f6608d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -28,3 +28,10 @@ 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⦄. /4 width=2 by fpb_fpbs, ssta_fpb/ qed. + +(* Note: this is used in the closure proof *) +lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, ssta_cpx, fpb_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index 4373c210e..f966dff5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -13,15 +13,14 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/substitution/lleq.ma". include "basic_2/computation/fpbs.ma". (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbu_fqup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 -| fpbu_cpxs : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 -| fpbu_llpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g, T1, 0] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 +| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 +| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 +| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 . interpretation @@ -33,15 +32,15 @@ interpretation lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpbu_cpxs, cprs_cpxs/ qed. -(* -lamma llprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → (L1 ⋕[T, 0] L2 → ⊥) → - ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpbu_llpxs, llprs_llpxs/ qed. -*) + +lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[T, 0] L2 → ⊥) → + ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed. + (* Basic forward lemmas *****************************************************) lemma fpbu_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,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 -/3 width=1 by llpxs_fpbs, cpxs_fpbs, fqup_fpbs/ +/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma index 3beb43760..566b83872 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma @@ -39,7 +39,8 @@ lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, | #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_llpxs, fleq_intro, llpx_llpxs, or_intror, or_introl/ + /4 width=3 by fpbu_lpxs, fleq_intro, lpx_lpxs, or_intror, or_introl/ +| /3 width=1 by fleq_intro, or_introl/ ] qed-. @@ -53,17 +54,16 @@ lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, 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 +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_inv_alt … H) -H +#L0 #L #T #HT1 #HT2 #HL0 #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 fleq_intro, or_introl/ - | /5 width=5 by fpbu_llpxs, ex2_3_intro, or_intror/ + [ /4 width=11 by fpbs_intro_alt, fpbu_fqup, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L0 L 0) #H + [ /4 width=3 by fleq_intro, lleq_trans, or_introl/ + | /5 width=5 by fpbu_lpxs, lleq_fpbs, 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/ + /5 width=11 by fpbs_intro_alt, fpbu_cpxs, cpx_cpxs, ex2_3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma index d1b1c9c94..40791dd84 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma @@ -14,7 +14,8 @@ include "basic_2/substitution/lleq_fqus.ma". include "basic_2/substitution/lleq_lleq.ma". -include "basic_2/computation/llpxs_lleq.ma". +include "basic_2/computation/cpxs_lleq.ma". +include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/fpbu.ma". (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) @@ -28,6 +29,7 @@ lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ⋕[T, 0] K2 → [ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2 /3 width=3 by fpbu_fqup, ex2_intro/ | /4 width=10 by fpbu_cpxs, cpxs_lleq_conf_sn, lleq_cpxs_trans, ex2_intro/ -| /5 width=3 by fpbu_llpxs, lleq_llpxs_trans, lleq_canc_sn, ex2_intro/ +| #L2 #HKL2 #HnKL2 elim (lleq_lpxs_trans … HKL2 … HT) -HKL2 + /6 width=3 by fpbu_lpxs, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index 453383dc4..e094ff57f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -14,7 +14,7 @@ include "basic_2/computation/fpbs_ext.ma". include "basic_2/computation/csx_fpbs.ma". -include "basic_2/computation/llsx_csx.ma". +include "basic_2/computation/lsx_csx.ma". include "basic_2/computation/fsb_alt.ma". (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) @@ -27,19 +27,19 @@ lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2 #G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1 #HT0 generalize in match IHu; -IHu generalize in match H10; -H10 -@(llsx_ind_alt … (csx_llsx … HT0 0)) -L0 +@(lsx_ind_alt … (csx_lsx … HT0 0)) -L0 #L0 #_ #IHl #H10 #IHu @fsb_intro #G2 #L2 #T2 * -G2 -L2 -T2 [ -IHl -IHc | -IHu -IHl | ] [ /3 width=5 by fpbs_fqup_trans/ | #T2 #HT02 #HnT02 elim (fpbs_cpxs_trans_neq … H10 … HT02 HnT02) -T0 /3 width=4 by/ | #L2 #HL02 #HnL02 @(IHl … HL02 HnL02) -IHl -HnL02 [ -IHu -IHc | ] - [ /2 width=3 by fpbs_llpxs_trans/ - | #G3 #L3 #T3 #H03 #_ elim (llpxs_fqup_trans … H03 … HL02) -L2 + [ /2 width=3 by fpbs_lpxs_trans/ + | #G3 #L3 #T3 #H03 #_ elim (lpxs_fqup_trans … H03 … HL02) -L2 #L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ] - [ #H destruct /4 width=5 by fsb_fpbs_trans, llpxs_fpbs, fpbs_fqup_trans/ + [ #H destruct /4 width=5 by fsb_fpbs_trans, lpxs_fpbs, fpbs_fqup_trans/ | #HnT04 #HT04 #H04 elim (fpbs_cpxs_trans_neq … H10 … HT04 HnT04) -T0 - /4 width=8 by fpbs_fqup_trans, fpbs_llpxs_trans/ + /4 width=8 by fpbs_fqup_trans, fpbs_lpxs_trans/ ] ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 2f9b322db..536288f01 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -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/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index d40cc3224..797f73147 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". +include "basic_2/computation/fpbs_lift.ma". include "basic_2/computation/fpbg_fleq.ma". include "basic_2/equivalence/cpes_cpds.ma". include "basic_2/dynamic/snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 3634321be..367312794 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbs_lpr.ma". include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index 4e6d1b33c..9213b4d57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/computation/cpds_cpds.ma". -include "basic_2/computation/fpbs_lpr.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lsstas.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/cpxs_llpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_llpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/cpxs_llpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/fpbs_lpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/fpbs_lpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsn_7.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsn_7.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsnstar_7.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsnstar_7.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysn_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysn_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysnalt_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysnalt_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_cpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_cpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_llpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_llpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lprs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lprs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_csx.etc similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_csx.etc index 33767f56c..9c284732c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_csx.etc @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/csx_lift.ma". (* added *) +include "basic_2/computation/csx_lift.ma". include "basic_2/computation/csx_llpxs.ma". include "basic_2/computation/llsx_ldrop.ma". include "basic_2/computation/llsx_llpx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc deleted file mode 100644 index 629d79828..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊢ ⋕ ➡ * break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc deleted file mode 100644 index dd15570ef..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc +++ /dev/null @@ -1,34 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpns_fpns.ma". -include "basic_2/computation/fpbu_fpns.ma". -include "basic_2/computation/fpbc.ma". - -(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) - -(* Properties on parallel computation for "big tree" normal forms ***********) - -lemma fpbc_fpns_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * -/3 width=9 by fpns_trans, ex2_3_intro/ -qed-. - -lemma fpns_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 * -#G0 #L0 #T0 #H0 #H02 elim (fpns_fpbu_trans … H1 … H0) -G -L -T -/3 width=9 by fpns_trans, ex2_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc deleted file mode 100644 index bf1e62fde..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpbc_fpns.ma". -include "basic_2/computation/fpbg.ma". - -(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) - -(* Properties on parallel computation for "big tree" normal forms ***********) - -lemma fpbg_fpns_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T #H @(fpbg_ind … H) -G -L -T -[ /3 width=5 by fpbc_fpbg, fpbc_fpns_trans/ -| /4 width=9 by fpbg_strap1, fpbc_fpns_trans/ -] -qed-. - -lemma fpns_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T -[ /3 width=5 by fpbc_fpbg, fpns_fpbc_trans/ -| /4 width=9 by fpbg_strap2, fpns_fpbc_trans/ -] -qed-. - -lemma fpbs_fpbg: ∀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 #H @(fpbs_ind … H) -G2 -L2 -T2 -[ /2 width=1 by or_introl/ -| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2 - [ /3 width=5 by fpns_trans, or_introl/ - | /5 width=5 by fpbc_fpbg, fpns_fpbc_trans, fpbu_fpbc, or_intror/ - | /3 width=5 by fpbg_fpns_trans, or_intror/ - | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/ - ] -] -qed-. - -(* Advanced properties ******************************************************) - -lemma fpbg_fpb_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim (fpb_fpbu … H2) -H2 -/3 width=5 by fpbg_fpns_trans, fpbg_strap1, fpbu_fpbc/ -qed-. - - -lemma fpb_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 elim (fpb_fpbu … H1) -H1 -/3 width=5 by fpns_fpbg_trans, fpbg_strap2, fpbu_fpbc/ -qed-. - -lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/ -qed-. - -(* Note: this is used in the closure proof *) -lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. -#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/ -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 deleted file mode 100644 index 863b08196..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc +++ /dev/null @@ -1,77 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/lleq_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 deleted file mode 100644 index dce46b065..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc +++ /dev/null @@ -1,39 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/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/etc/lpx_sn/fpbs_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc similarity index 56% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc index fff178ef8..a180d1124 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc @@ -12,14 +12,24 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpns.ma". -include "basic_2/computation/fpbs.ma". +include "basic_2/relocation/llor.ma". +include "basic_2/substitution/lleq_alt.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -(* Properties on parallel computation for "big tree" normal forms ***********) +(* Properties on poinwise union for local environments **********************) -lemma fpns_fpbs: ∀h,g,G1,G2,L1,L2,T1,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 * /2 width=1 by llpxs_fpbs/ -qed. +lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L. +#T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct +#HL1 #IHT @lleq_intro_alt // +#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) +#Hi elim (ldrop_O1_lt L1 i) // +#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 (llor_fwd_sort … H) // +| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) // +| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s + elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s + elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct + elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s + lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d + lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d + + + + +[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d + elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H + elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct + elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct + lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d + lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d + lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s + elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H + lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY + lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H + lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY + >(leq_inv_O_Y … HL2sY) -HL2sY // + + + + + +lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s → + ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s. +#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d // +[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d + elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H + elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct + elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct + lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d + lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d + lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s + elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H + lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY + lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H + lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY + >(leq_inv_O_Y … HL2sY) -HL2sY // +(* +| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d + elim (lleq_inv_bind … H) -H #HV #HT +*) +| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d + elim (lleq_inv_flat … H) -H #HV #HT + lapply (IHV … HV HL12d) -HV #H1 + lapply (IHT … HT HL12d) #H2 + + + + @(lpxs_trans … LV) /2 width=3 by/ -IHV + lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H + + @(IH … HL12d) -IHT -IHV + + /4 width=5 by lpxs_trans/ + + +lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 → + ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2. +#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d +[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 4cf9d4bb0..2ea22a769 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -14,14 +14,16 @@ include "basic_2/notation/relations/btpred_8.ma". include "basic_2/relocation/fquq.ma". -include "basic_2/reduction/llpx.ma". +include "basic_2/substitution/lleq.ma". +include "basic_2/reduction/lpx.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) 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_llpx: ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_lleq: ∀L2. L1 ⋕[T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation @@ -35,7 +37,6 @@ 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. -(* -lamma 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. -*) + +lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpb_lpx, lpr_lpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma index 158b6b1d6..ddbb9743c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/static/aaa_fqus.ma". -include "basic_2/reduction/llpx_aaa.ma". +include "basic_2/static/aaa_lleq.ma". +include "basic_2/reduction/lpx_aaa.ma". include "basic_2/reduction/fpb.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -23,5 +24,5 @@ include "basic_2/reduction/fpb.ma". lemma aaa_fpb_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=6 by aaa_llpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ +/3 width=6 by aaa_lleq_conf, aaa_lpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma new file mode 100644 index 000000000..1edda42ad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L1 ⋕[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. +#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ +[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 + [ #H elim (ylt_yle_false … H) // + | * /3 width=5 by aaa_lref/ + ] +| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=2 by aaa_abbr/ +| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=1 by aaa_abst/ +| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H + /3 width=3 by aaa_appl/ +| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by aaa_cast/ +] +qed-. + +lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L2 ⋕[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. +/3 width=3 by lleq_aaa_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 0fc5b655c..b4ee8c1fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -85,17 +85,16 @@ table { ] [ { "strongly normalizing extended computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] - [ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ] [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_llpx" + "csx_lpxs" + "csx_llpxs" + "csx_fpbs" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] [ { "\"big tree\" parallel computation" * } { [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_lpr" + "fpbs_fpbs" + "fpbs_ext" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ] } ] [ { "decomposed extended computation" * } { @@ -103,9 +102,8 @@ table { } ] [ { "context-sensitive extended computation" * } { - [ "llpxs ( ⦃?,?⦄ ⊢ ➡*[?,?,?,?] ? )" "llpxs_lleq" + "llpxs_aaa" + "llpxs_lprs" "llpxs_cpxs" + "llpxs_llpxs" * ] [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_llpx" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -134,7 +132,6 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "llpx ( ⦃?,?⦄ ⊢ ➡[?,?,?,?] ? )" "llpx_ldrop" + "llpx_lleq" + "llpx_aaa" + "llpx_lpr" * ] [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ] } @@ -185,7 +182,7 @@ table { } ] [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ] + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ] } ] [ { "stratified static type assignment" * } { -- 2.39.2