From 7a25b8fcba2436a75556db1725c6e1be78a9faca Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 Apr 2014 12:12:05 +0000 Subject: [PATCH] - advances in the theory of cofrees - some notational changes - some refactoring in etc --- .../basic_2/computation/cpxs_lleq.ma | 8 +- .../basic_2/computation/csx_lleq.ma | 4 +- .../lambdadelta/basic_2/computation/fpbc.ma | 4 +- .../basic_2/computation/fpbc_fleq.ma | 8 +- .../basic_2/computation/fpbc_fpbs.ma | 2 +- .../lambdadelta/basic_2/computation/fpbg.ma | 26 +- .../basic_2/computation/fpbg_fleq.ma | 24 +- .../basic_2/computation/fpbg_fpbg.ma | 4 +- .../basic_2/computation/fpbg_lift.ma | 4 +- .../lambdadelta/basic_2/computation/fpbs.ma | 6 +- .../basic_2/computation/fpbs_alt.ma | 6 +- .../basic_2/computation/fpbs_fleq.ma | 2 +- .../lambdadelta/basic_2/computation/fpbu.ma | 4 +- .../basic_2/computation/fpbu_fleq.ma | 8 +- .../basic_2/computation/fpbu_lleq.ma | 4 +- .../basic_2/computation/fsb_aaa.ma | 4 +- .../basic_2/computation/fsb_alt.ma | 6 +- .../basic_2/computation/fsb_csx.ma | 2 +- .../basic_2/computation/lpxs_lleq.ma | 24 +- .../lambdadelta/basic_2/computation/lsx.ma | 4 +- .../basic_2/computation/lsx_alt.ma | 14 +- .../basic_2/computation/lsx_lpx.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 60 ++--- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 6 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lsstas.ma | 8 +- .../basic_2/dynamic/snv_lsstas_lpr.ma | 8 +- .../basic_2/etc/{lsuby => cpy}/cpx_cpys.etc | 0 .../etc/{cpx_cpys.etc => cpy/cpx_cpys2.etc} | 0 .../basic_2/etc/{lsuby => cpy}/cpxs_cpys.etc | 0 .../lambdadelta/basic_2/etc/cpy/cpy.etc | 27 ++ .../lambdadelta/basic_2/etc/cpy/cpys.etc | 14 + .../basic_2/etc/{lsuby => cpy}/lpx_cpys.etc | 0 .../lambdadelta/basic_2/etc/cpy/lsuby.etc | 15 ++ .../etc/{lsuby => lleq_alt}/lazyeqalt_4.etc | 0 .../basic_2/etc/{lsuby => lleq_alt}/lleq.etc | 0 .../etc/{lsuby => lleq_alt}/lleq_alt.etc | 0 .../etc/{lsuby => lleq_alt}/lleq_ext.etc | 0 .../etc/{lsuby => lleq_alt}/lleq_fqus.etc | 0 .../etc/{lsuby => lleq_alt}/lleq_ldrop.etc | 0 .../etc/{lsuby => lleq_alt}/lleq_lleq.etc | 0 .../basic_2/etc/{lpx_sn => }/llor.etc | 71 ++--- .../lambdadelta/basic_2/etc/llpx_sn_alt2.etc | 45 ++++ .../{cofreestar_3.ma => cofreestar_4.ma} | 4 +- .../notation/relations/lazybtpredproper_8.ma | 2 +- .../relations/lazybtpredstarproper_8.ma | 2 +- .../basic_2/notation/relations/lazyeq_4.ma | 2 +- .../basic_2/notation/relations/lazyeq_7.ma | 2 +- .../basic_2/reduction/cpr_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 6 +- .../basic_2/reduction/cpx_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/fpb.ma | 2 +- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 24 +- .../basic_2/relocation/llpx_sn_alt.ma | 250 ------------------ .../lambdadelta/basic_2/static/aaa_lleq.ma | 4 +- .../basic_2/static/ssta_llpx_sn.ma | 2 +- .../basic_2/substitution/cofrees.ma | 68 ++++- .../basic_2/substitution/cpys_lift.ma | 8 + .../lambdadelta/basic_2/substitution/fleq.ma | 6 +- .../basic_2/substitution/fleq_fleq.ma | 4 +- .../lambdadelta/basic_2/substitution/lleq.ma | 68 ++--- .../basic_2/substitution/lleq_alt.ma | 20 +- .../basic_2/substitution/lleq_fqus.ma | 16 +- .../basic_2/substitution/lleq_ldrop.ma | 80 +++--- .../basic_2/substitution/lleq_leq.ma | 18 +- .../basic_2/substitution/lleq_lleq.ma | 8 +- .../{relocation => substitution}/llpx_sn.ma | 0 .../basic_2/substitution/llpx_sn_alt1.ma | 250 ++++++++++++++++++ .../llpx_sn_ldrop.ma | 2 +- .../llpx_sn_leq.ma | 2 +- .../llpx_sn_lpx_sn.ma | 2 +- .../llpx_sn_tc.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 73 files changed, 719 insertions(+), 577 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => cpy}/cpx_cpys.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{cpx_cpys.etc => cpy/cpx_cpys2.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => cpy}/cpxs_cpys.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => cpy}/lpx_cpys.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lazyeqalt_4.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq_alt.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq_ext.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq_fqus.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq_ldrop.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsuby => lleq_alt}/lleq_lleq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lpx_sn => }/llor.etc (61%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{cofreestar_3.ma => cofreestar_4.ma} (89%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/llpx_sn.ma (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/llpx_sn_ldrop.ma (99%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/llpx_sn_leq.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/llpx_sn_lpx_sn.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => substitution}/llpx_sn_tc.ma (96%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma index ce575a47b..2bcff48e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma @@ -20,20 +20,20 @@ include "basic_2/computation/cpxs.ma". (* Properties on lazy equivalence for local environments ********************) lemma lleq_cpxs_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. + ∀L1. L1 ≡[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. #h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /4 width=6 by cpx_lleq_conf_dx, lleq_cpx_trans, cpxs_strap2/ qed-. lemma cpxs_lleq_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L1. L2 ⋕[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. + ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. /3 width=3 by lleq_cpxs_trans, lleq_sym/ qed-. lemma cpxs_lleq_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. + ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2. #h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_lleq_conf_dx/ qed-. lemma cpxs_lleq_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. + ∀L2. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2. /4 width=6 by cpxs_lleq_conf_dx, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma index d56acd9df..765861e3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma @@ -20,11 +20,11 @@ include "basic_2/computation/csx.ma". (* Properties on lazy equivalence for local environments ********************) lemma csx_lleq_conf: ∀h,g,G,L1,T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → - ∀L2. L1 ⋕[T, 0] L2 → ⦃G, L2⦄ ⊢ ⬊*[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. + 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 bf9baaa90..82ea6ec0f 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)" @@ -29,5 +29,5 @@ interpretation (* Baic properties **********************************************************) lemma fpbu_fpbc: ∀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⦄ → ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄. /2 width=5 by ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma index 9056ca4c7..cf2ee2ffc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fleq.ma @@ -20,14 +20,14 @@ include "basic_2/computation/fpbc.ma". (* Properties on lazy equivalence on closures *******************************) -lemma fpbc_fleq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄. +lemma fpbc_fleq_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≡[0] ⦃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 fleq_trans, ex2_3_intro/ qed-. -lemma fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[0] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄. +lemma fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≡[0] ⦃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 (fleq_fpbu_trans … H1 … H0) -G -L -T /3 width=9 by fleq_trans, ex2_3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma index 7d81c812d..2c45646ed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma @@ -20,7 +20,7 @@ include "basic_2/computation/fpbc.ma". (* Forward lemmas on "big tree" parallel computation for closures ***********) -lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → +lemma fpbc_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 * /3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 0755ebf79..5d7ce1cb3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -25,38 +25,38 @@ interpretation "general 'big tree' proper parallel computation (closure)" (* Basic properties *********************************************************) -lemma fpbc_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⦄. +lemma fpbc_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⦄. /2 width=1 by tri_inj/ qed. lemma fpbg_strap1: ∀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⦄. + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_step/ qed. lemma fpbg_strap2: ∀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⦄. + ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed. (* Note: this is used in the closure proof *) -lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄. /4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed. (* Basic eliminators ********************************************************) lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 …. - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. #h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H @(tri_TC_ind … IH1 IH2 G2 L2 T2 H) qed-. lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 …. - (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. + (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻≡[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. #h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma index bb79f4aab..293e666d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma @@ -19,16 +19,16 @@ include "basic_2/computation/fpbg.ma". (* Properties on lazy equivalence for closures ******************************) -lemma fpbg_fleq_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ⋕[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +lemma fpbg_fleq_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃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_fleq_trans/ | /4 width=9 by fpbg_strap1, fpbc_fleq_trans/ ] qed-. -lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⋕[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≡[h, g] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃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, fleq_fpbc_trans/ | /4 width=9 by fpbg_strap2, fleq_fpbc_trans/ @@ -36,8 +36,8 @@ lemma fleq_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2 qed-. lemma fpbs_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≡[0] ⦃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 @@ -52,27 +52,27 @@ 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⦄. + ⦃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_fleq_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⦄. + ⦃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 fleq_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⦄. + ∀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⦄. + ∀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/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index f423aaecd..1f52880ad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -19,7 +19,7 @@ include "basic_2/computation/fpbg_fleq.ma". (* Advanced inversion lemmas ************************************************) -lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → +lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,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⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1 [ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/ @@ -31,7 +31,7 @@ qed-. (* Advanced forward lemmas **************************************************) -lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → +lemma fpbg_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 #H @(fpbg_ind … H) -G2 -L2 -T2 [2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma index 4dd9afb73..c67134ee3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -20,9 +20,9 @@ include "basic_2/computation/fpbg.ma". (* Advanced properties ******************************************************) lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄. + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. /5 width=5 by fpbc_fpbg, fpbu_fpbc, lsstas_fpbu/ qed. lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄. + ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. /4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index d1ce32de1..c9f0875e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -77,7 +77,7 @@ lemma lpxs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1, T /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⦄. +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⦄. @@ -109,7 +109,7 @@ lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G 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⦄. + 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⦄ → @@ -131,7 +131,7 @@ lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃ 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⦄. + 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 → 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 a446b57fa..047fd164a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -26,7 +26,7 @@ definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝ λh,g,G1,L1,T1,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. + ⦃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). @@ -71,7 +71,7 @@ qed-. 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⦄ . + ⦃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 *************************************************) @@ -79,5 +79,5 @@ lemma fpbs_intro_alt: ∀h,g,G1,G2,L1,L0,L,L2,T1,T,T2. 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. + ⦃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_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma index eb0bc4d2b..9f0c8d415 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma @@ -20,6 +20,6 @@ include "basic_2/computation/fpbs.ma". (* Properties on lazy equivalence on closures *******************************) 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⦄. + ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #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/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index f78b30277..1525567aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -20,7 +20,7 @@ include "basic_2/computation/fpbs.ma". 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_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 +| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 . interpretation @@ -33,7 +33,7 @@ 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. -lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[T, 0] L2 → ⊥) → +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. 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 566b83872..c4e1813a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma @@ -20,16 +20,16 @@ include "basic_2/computation/fpbu_lleq.ma". (* Properties on lazy equivalence for closures ******************************) -lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ⋕[0] ⦃F2, K2, T2⦄ → +lemma fleq_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃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⦄ ⋕[0] ⦃G2, L2, U2⦄. + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. #h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 #K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpbu_trans … HK12 … H12) -K2 /3 width=5 by fleq_intro, 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⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨ + ⦃G1, L1, T1⦄ ≡[0] ⦃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 @@ -45,7 +45,7 @@ lemma fpb_fpbu: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, qed-. lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕[0] ⦃G2, L2, T2⦄ ∨ + ⦃G1, L1, T1⦄ ≡[0] ⦃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 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 40791dd84..e39e9d79e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma @@ -22,9 +22,9 @@ include "basic_2/computation/fpbu.ma". (* Properties on lazy equivalence for local environments ********************) -lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ⋕[T, 0] K2 → +lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ≡[T, 0] K2 → ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, g] ⦃G, L2, U⦄ → - ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ⋕[U, 0] L2. + ∃∃L1. ⦃F, K1, T⦄ ≻[h, g] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2. #h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U [ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2 /3 width=3 by fpbu_fqup, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma index 1074ef74d..e8f4d2015 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -52,7 +52,7 @@ lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. @@ -64,7 +64,7 @@ qed-. lemma aaa_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index 992775d70..12df3c22c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -21,7 +21,7 @@ include "basic_2/computation/fsb.ma". (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ | fsba_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2 ) → fsba h g G1 L1 T1. interpretation @@ -32,7 +32,7 @@ interpretation lemma fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 ) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T. @@ -74,7 +74,7 @@ lemma fsb_fpbs_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → lemma fsb_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → R G1 L1 T1. 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 e094ff57f..41ba54fd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -60,7 +60,7 @@ lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. lemma csx_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. 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 8f48afe86..4263c55cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -22,8 +22,8 @@ include "basic_2/computation/lpxs_cpxs.ma". (* Properties on lazy equivalence for local environments ********************) lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → - ∀L1,T,d. L1 ⋕[T, d] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. + ∀L1,T,d. L1 ≡[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ≡[T, d] K2. #h #g #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ #K #K2 #_ #HK2 #IH #L1 #T #d #HT elim (IH … HT) -L2 #L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K @@ -31,8 +31,8 @@ lemma lleq_lpxs_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → qed-. lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct @@ -60,8 +60,8 @@ lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, qed-. lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fquq_inv_gen … H) -H [ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 @@ -71,8 +71,8 @@ elim (fquq_inv_gen … H) -H qed-. lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 [ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 /3 width=4 by fqu_fqup, ex3_intro/ @@ -83,8 +83,8 @@ lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G qed-. lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fqus_inv_gen … H) -H [ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 @@ -96,7 +96,7 @@ qed-. fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ → ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). + (∀T. L0 ≡[T, d] L2 ↔ L1 ≡[T, d] L). #h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e [ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H /3 width=5 by ex3_intro, conj/ @@ -120,5 +120,5 @@ qed-. lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 → ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). + (∀T. L0 ≡[T, d] L2 ↔ L1 ≡[T, d] L). /2 width=1 by leq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 435650bd1..0f47fe056 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -29,7 +29,7 @@ interpretation lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv. (∀L1. G ⊢ ⬊*[h, g, T, d] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⬊*[h, g, T, d] L → R L. @@ -40,7 +40,7 @@ qed-. (* Basic properties *********************************************************) lemma lsx_intro: ∀h,g,G,L1,T,d. - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) → G ⊢ ⬊*[h, g, T, d] L1. /5 width=1 by lleq_sym, SN_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma index cd7c83be9..50b41adb2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_alt.ma @@ -31,7 +31,7 @@ interpretation lemma lsxa_ind: ∀h,g,G,T,d. ∀R:predicate lenv. (∀L1. G ⊢ ⬊⬊*[h, g, T, d] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⬊⬊*[h, g, T, d] L → R L. @@ -42,17 +42,17 @@ qed-. (* Basic properties *********************************************************) lemma lsxa_intro: ∀h,g,G,L1,T,d. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → G ⊢ ⬊⬊*[h, g, T, d] L1. /5 width=1 by lleq_sym, SN_intro/ qed. fact lsxa_intro_aux: ∀h,g,G,L1,T,d. - (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, d] L → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → + (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, g] L2 → L1 ≡[T, d] L → (L1 ≡[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → G ⊢ ⬊⬊*[h, g, T, d] L1. /4 width=3 by lsxa_intro/ qed-. lemma lsxa_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊⬊*[h, g, T, d] L1 → - ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⬊⬊*[h, g, T, d] L2. + ∀L2. L1 ≡[T, d] L2 → G ⊢ ⬊⬊*[h, g, T, d] L2. #h #g #T #G #L1 #d #H @(lsxa_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @lsxa_intro #K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2 @@ -66,7 +66,7 @@ elim (lleq_dec T L1 L2 d) /3 width=4 by lsxa_lleq_trans/ qed-. lemma lsxa_intro_lpx: ∀h,g,G,L1,T,d. - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → G ⊢ ⬊⬊*[h, g, T, d] L2) → G ⊢ ⬊⬊*[h, g, T, d] L1. #h #g #G #L1 #T #d #IH @lsxa_intro_aux #L #L2 #H @(lpxs_ind_dx … H) -L @@ -95,7 +95,7 @@ qed-. (* Advanced properties ******************************************************) lemma lsx_intro_alt: ∀h,g,G,L1,T,d. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) → G ⊢ ⬊*[h, g, T, d] L1. /6 width=1 by lsxa_inv_lsx, lsx_lsxa, lsxa_intro/ qed. @@ -107,7 +107,7 @@ lemma lsx_lpxs_trans: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 → lemma lsx_ind_alt: ∀h,g,G,T,d. ∀R:predicate lenv. (∀L1. G ⊢ ⬊*[h, g, T, d] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ≡[T, d] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⬊*[h, g, T, d] L → R L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma index 37f4edfaf..d191024b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpx.ma @@ -21,7 +21,7 @@ include "basic_2/computation/lsx.ma". (* Advanced properties ******************************************************) lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊*[h, g, T, d] L1 → - ∀L2. L1 ⋕[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2. + ∀L2. L1 ≡[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2. #h #g #T #G #L1 #d #H @(lsx_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @lsx_intro #K2 #HLK2 #HnLK2 elim (lleq_lpx_trans … HLK2 … HL12) -HLK2 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 797f73147..56ed1c2c5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -47,17 +47,17 @@ definition IH_snv_lsstas: ∀h:sh. sd h → relation3 genv lenv term ≝ (* Properties for the preservation results **********************************) fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. #h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H @(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H @@ -65,10 +65,10 @@ fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. qed-. fact da_cpcs_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H @@ -76,8 +76,8 @@ elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/ qed-. fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → @@ -88,10 +88,10 @@ elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) qed-. fact lsstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → @@ -109,12 +109,12 @@ elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 qed-. fact lsstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g, l] U1 → - ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, g, l] U2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 @@ -125,18 +125,18 @@ lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_ qed-. fact snv_ssta_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ∀U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g]. /3 width=8 by lsstas_inv_SO, ssta_lsstas/ qed-. fact lsstas_cpds_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, g, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. @@ -155,9 +155,9 @@ elim (le_or_ge l2 l) #Hl2 qed-. fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma index 5adc067d5..dd56de7a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma @@ -22,9 +22,9 @@ include "basic_2/dynamic/snv_cpcs.ma". (* Properties on degree assignment for terms ********************************) fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 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 367312794..f73c20a5e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -21,10 +21,10 @@ include "basic_2/dynamic/lsubsv_snv.ma". (* Properties on context-free parallel reduction for local environments *****) fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma index 739caf494..a0ef9e99e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/snv_cpcs.ma". (* Properties on nat-iterated stratified static type assignment for terms ***) fact snv_lsstas_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsstas h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #HG0 #HL0 #HT0 #_ #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 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 9213b4d57..1ee5ba08e 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 @@ -22,10 +22,10 @@ include "basic_2/dynamic/lsubsv_lsstas.ma". (* Properties on sn parallel reduction for local environments ***************) fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpx_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpx_cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpx_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpx_cpys2.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpx_cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpx_cpys2.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpxs_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpxs_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpxs_cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpxs_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc new file mode 100644 index 000000000..e941c9653 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc @@ -0,0 +1,27 @@ +include "basic_2/grammar/cl_shift.ma". +include "basic_2/relocation/ldrop_append.ma". + +lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G). +#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e +/2 width=1 by cpy_atom, cpy_bind, cpy_flat/ +#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L +lapply (ldrop_fwd_length_lt2 … HK0) #H +@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *) +@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ +qed-. + +lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#G #L1 @(lenv_ind_dx … L1) -L1 normalize +[ #L #T1 #T #d #e #HT1 + @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #L #T1 #X #d #e + >shift_append_assoc normalize #H + elim (cpy_inv_bind1 … H) -H + #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] (**) (* explicit constructor *) + /2 width=3 by trans_eq/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc new file mode 100644 index 000000000..22f74d0a8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc @@ -0,0 +1,14 @@ +lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G). +#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2 +/3 width=3 by cpys_strap1, cpy_append/ +qed-. + +lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T +[ /2 width=4 by ex2_2_intro/ +| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct + elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct + /2 width=4 by ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lpx_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lpx_cpys.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lpx_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc new file mode 100644 index 000000000..657ad6b6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc @@ -0,0 +1,15 @@ +(* +lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 → + ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2. +#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 // +[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21 + >(yle_inv_O2 … He21) -He21 + /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21 + elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ + * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21 + elim (ynat_cases d2) /3 width=1 by lsuby_pair/ + * #d0 #H destruct @lsuby_succ @IHL12 // + [ destruct + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lazyeqalt_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lazyeqalt_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lazyeqalt_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lazyeqalt_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ext.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_ext.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ext.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_ext.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_fqus.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_fqus.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_fqus.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_lleq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lleq_alt/lleq_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llor.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc index a2f332a69..6a750a0ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llor.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc @@ -15,13 +15,14 @@ include "ground_2/xoa/xoa2.ma". include "basic_2/notation/relations/lazyor_4.ma". include "basic_2/relocation/lpx_sn_alt.ma". +include "basic_2/substitution/cofrees.ma". (* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) -inductive clor (T) (L2) (K1) (V1): predicate term ≝ -| clor_sn: ∀U. |K1| < |L2| → ⇧[|L2|-|K1|-1, 1] U ≡ T → clor T L2 K1 V1 V1 -| clor_dx: ∀I,K2,V2. |K1| < |L2| → (∀U. ⇧[|L2|-|K1|-1, 1] U ≡ T → ⊥) → - ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2 +inductive clor (T) (L2) (I) (K1) (V1): predicate term ≝ +| clor_sn: |K1| < |L2| → |L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → clor T L2 I K1 V1 V1 +| clor_dx: ∀K2,V2. |K1| < |L2| → (|L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → ⊥) → + ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 I K1 V1 V2 . definition llor: relation4 term lenv lenv lenv ≝ @@ -33,46 +34,45 @@ interpretation (* Basic properties *********************************************************) -lemma llor_pair_sn: ∀I,L1,L2,L,V,T,U. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → ⇧[|L2|-|L1|-1, 1] U ≡ T → +lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L → + |L1| < |L2| → |L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ → L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V. /3 width=2 by clor_sn, lpx_sn_pair/ qed. -lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → (∀U. ⇧[|L2|-|L1|-1, 1] U ≡ T → ⊥) → - ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 → +lemma llor_pair_dx: ∀I,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → + |L1| < |L2| → (|L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ → ⊥) → + ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{I}V2 → L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2. /4 width=3 by clor_dx, lpx_sn_pair/ qed. - +(* lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. #T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/ #L1 #I1 #V1 #IHL1 normalize #H elim IHL1 -IHL1 /2 width=3 by transitive_le/ -#L #HT elim (is_lift_dec T (|L2|-|L1|-1) 1) -[ * /3 width=2 by llor_pair_sn, ex_intro/ +#L #HT elim (cofrees_dec L1 T (|L2|-|L1|-1)) +[ /3 width=2 by llor_pair_sn, ex_intro/ | elim (ldrop_O1_lt L2 (|L2|-|L1|-1)) /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/ +| ] qed-. - +*) (* Alternative definition ***************************************************) (* 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. +lemma plus_minus_minus_be: ∀x,y,z:nat. 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. +fact plus_minus_minus_be_aux: ∀i,x,y,z:nat. 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 ~ϵ 𝐅*⦃K1, T⦄ → I1 = I ∧ V1 = V) ∧ + (∀I2,K2,V2. (|L2|-|L1|+i ~ϵ 𝐅*⦃K1, T⦄ → ⊥) → ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K + ∧∧ I1 = I & I2 = I & V2 = V ) ) → L1 ⩖[T] L2 ≡ L. #T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 @@ -82,40 +82,15 @@ lapply (ldrop_fwd_length_le4 … HLK1) normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // #H2i lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1 elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2 -elim (is_lift_dec T (|L2|-|L1|+i) 1) -[ -IH2 * #U #HUT elim (IH1 … HUT) -IH1 - /3 width=2 by clor_sn, and3_intro/ +elim (cofrees_dec K1 T (|L2|-|L1|+i)) +[ -IH2 #HT elim (IH1 … HT) -IH1 + /3 width=2 by clor_sn, conj/ | -IH1 #H elim (ldrop_O1_lt L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/ #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 /5 width=3 by clor_dx, ex_intro, and3_intro/ ] qed. -lemma llor_ind_alt: ∀T,L2. ∀S:relation lenv. ( - ∀L1,L. |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 & S K1 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 & S K1 K - ) - ) → |L1| ≤ |L2| → S L1 L - ) → - ∀L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → S L1 L. -#T #L2 #S #IH1 #L1 #L #H @(lpx_sn_ind_alt … H) -L1 -L -#L1 #L #HL1 #IH2 #HL12 @IH1 // -IH1 -HL1 -#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK -lapply (ldrop_fwd_length_minus4 … HLK1) -lapply (ldrop_fwd_length_le4 … HLK1) -normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // -lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 -elim (IH2 … HLK1 HLK) -IH2 #H * -/5 width=5 by lt_to_le, ex6_3_intro, ex5_intro, or_intror, or_introl/ -qed-. - lemma llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L1| = |L| ∧ (∀I1,I,K1,K,V1,V,i. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc new file mode 100644 index 000000000..bdbc32e88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cofrees_lift.ma". +include "basic_2/substitution/llpx_sn_alt1.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* alternative definition of llpx_sn (not recursive) *) +definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝ + λR,d,T,L1,L2. |L1| = |L2| ∧ + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R I1 K1 V1 V2 + ). + +(* Main properties **********************************************************) + +lemma cpy_inv_nlift2_be: ∀G,L,U1,U2,d. ⦃G, L⦄ ⊢ U1 ▶[d, ∞] U2 → ∀i. d ≤ yinj i → + ∀K,s. ⇩[s, i, 1] L ≡ K → + (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥). +#G #L #U1 #U2 #d #HU12 #i #Hdi #K #s #HLK #HnU2 #T1 #HTU1 +elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=2 by/ +qed-. + +theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2. +#R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H +#HL12 #IH @conj // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1 +#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1 +[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/ +| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i + #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2 + @(cpy_inv_nlift2_be … HU10) /2 width=3 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma index 86fc1f140..e73167c3f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( d ~ ϵ break 𝐅 * ⦃ term 46 L, break term 46 T ⦄ )" +notation "hvbox( L ⊢ break term 46 i ~ ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )" non associative with precedence 45 - for @{ 'CoFreeStar $d $L $T }. + for @{ 'CoFreeStar $L $i $d $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma index a821838f7..6abdbeb59 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma @@ -14,6 +14,6 @@ (* 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 ⦄ )" +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 @{ 'LazyBTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma index 91a275ab8..e56e02e46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma @@ -14,6 +14,6 @@ (* 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 ⦄ )" +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 @{ 'LazyBTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma index 955d59e0d..0d9afe1ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⋕ break [ term 46 T , break term 46 d ] break term 46 L2 )" +notation "hvbox( L1 ≡ break [ term 46 T , break term 46 d ] break term 46 L2 )" non associative with precedence 45 for @{ 'LazyEq $T $d $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma index 3c6f5e75e..4bfa2c754 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 d ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ break [ term 46 d ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'LazyEq $d $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma index 786779565..4db858798 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_ldrop.ma". +include "basic_2/substitution/llpx_sn_ldrop.ma". include "basic_2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index c36dd0fb4..507aaef29 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -20,7 +20,7 @@ include "basic_2/reduction/cpx_llpx_sn.ma". (* Properties on lazy equivalence for local environments ********************) lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. + ∀L1. L1 ≡[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. #h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_st/ [ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 [ #H elim (ylt_yle_false … H) // @@ -44,12 +44,12 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → qed-. lemma cpx_lleq_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L2 ⋕[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. + ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. /3 width=3 by lleq_cpx_trans, lleq_sym/ qed-. lemma cpx_lleq_conf_sn: ∀h,g,G. s_r_confluent1 … (cpx h g G) (lleq 0). /3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-. lemma cpx_lleq_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. + ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2. /4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma index 46a83164a..418106494 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_ldrop.ma". +include "basic_2/substitution/llpx_sn_ldrop.ma". include "basic_2/reduction/cpx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 40e03d59b..71d7a0cb9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -23,7 +23,7 @@ inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 | fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 | fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] 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 +| fpb_lleq: ∀L2. L1 ≡[T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index 182aaae8a..3ff9a954f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -22,12 +22,12 @@ include "basic_2/reduction/lpx_ldrop.ma". (* Properties on lazy equivalence for local environments ********************) axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → - ∀L1,T,d. L1 ⋕[T, d] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ⋕[T, d] K2. + ∀L1,T,d. L1 ≡[T, d] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ≡[T, d] K2. lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct @@ -55,8 +55,8 @@ lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, qed-. lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fquq_inv_gen … H) -H [ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 @@ -66,8 +66,8 @@ elim (fquq_inv_gen … H) -H qed-. lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 [ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 /3 width=4 by fqu_fqup, ex3_intro/ @@ -78,8 +78,8 @@ lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2 qed-. lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ≡[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fqus_inv_gen … H) -H [ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 @@ -91,7 +91,7 @@ qed-. fact leq_lpx_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, g] L2 → ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). + (∀T. L0 ≡[T, d] L2 ↔ L1 ≡[T, d] L). #h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e [ #d #e #_ #L2 #H >(lpx_inv_atom1 … H) -H /3 width=5 by ex3_intro, conj/ @@ -115,5 +115,5 @@ qed-. lemma leq_lpx_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, g] L2 → ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡[h, g] L & - (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). + (∀T. L0 ≡[T, d] L2 ↔ L1 ≡[T, d] L). /2 width=1 by leq_lpx_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma deleted file mode 100644 index d0b9b2049..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma +++ /dev/null @@ -1,250 +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/lift_neg.ma". -include "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/relocation/llpx_sn.ma". - -(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) - -(* alternative definition of llpx_sn *) -inductive llpx_sn_alt (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝ -| llpx_sn_alt_intro: ∀L1,L2,T,d. - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2 - ) → - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt R 0 V1 K1 K2 - ) → |L1| = |L2| → llpx_sn_alt R d T L1 L2 -. - -(* Compact definition of llpx_sn_alt ****************************************) - -lemma llpx_sn_alt_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| → - (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 - ) → llpx_sn_alt R d T L1 L2. -#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_intro // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 -elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/ -qed. - -lemma llpx_sn_alt_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv. - (∀L1,L2,T,d. |L1| = |L2| → ( - ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2 & S 0 V1 K1 K2 - ) → S d T L1 L2) → - ∀L1,L2,T,d. llpx_sn_alt R d T L1 L2 → S d T L1 L2. -#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d -#L1 #L2 #T #d #H1 #H2 #HL12 #IH2 @IH -IH // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 -elim (H1 … HnT HLK1 HLK2) -H1 /4 width=8 by and4_intro/ -qed-. - -lemma llpx_sn_alt_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt R d T L1 L2 → - |L1| = |L2| ∧ - ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt R 0 V1 K1 K2. -#R #L1 #L2 #T #d #H @(llpx_sn_alt_ind_alt … H) -L1 -L2 -T -d -#L1 #L2 #T #d #HL12 #IH @conj // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 -elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma llpx_sn_alt_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓕ{I}V.T) L1 L2 → - llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R d T L1 L2. -#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H -#HL12 #IH @conj @llpx_sn_alt_intro_alt // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 -elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 // -/3 width=8 by nlift_flat_sn, nlift_flat_dx, and3_intro/ -qed-. - -lemma llpx_sn_alt_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt R d (ⓑ{a,I}V.T) L1 L2 → - llpx_sn_alt R d V L1 L2 ∧ llpx_sn_alt R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). -#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt_inv_alt … H) -H -#HL12 #IH @conj @llpx_sn_alt_intro_alt [1,3: normalize // ] -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 -[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 - /3 width=9 by nlift_bind_sn, and3_intro/ -| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi - lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1 - lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2 - elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/ - @nlift_bind_dx (cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄. +#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ → + ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → + ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄. +#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/ +qed. + +lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → + ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄. +#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/ +qed. + +axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄). + +(* Negated inversion lemmas *************************************************) + +lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥). +#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i) +/4 width=9 by cofrees_bind, or_intror, or_introl/ +qed-. + +lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥). +#I #L #W #U #d #H elim (cofrees_dec L W d) +/4 width=8 by cofrees_flat, or_intror, or_introl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma index b6d9e45a1..f4803a17d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -77,6 +77,14 @@ lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/ qed-. +lemma cpys_inv_lref1_Y2: ∀G,L,T2,i,d. ⦃G, L⦄ ⊢ #i ▶*[d, ∞] T2 → + T2 = #i ∨ + ∃∃I,K,V1,V2. d ≤ i & ⇩[i] L ≡ K.ⓑ{I}V1 & + ⦃G, K⦄ ⊢ V1 ▶*[0, ∞] V2 & ⇧[O, i+1] V2 ≡ T2. +#G #L #T2 #i #d #H elim (cpys_inv_lref1 … H) -H /2 width=1 by or_introl/ +* >yminus_Y_inj /3 width=7 by or_intror, ex4_4_intro/ +qed-. + lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[O, i+1] V2 ≡ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma index bb55c859f..3c90f5a9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR CLOSURES ********************************************) inductive fleq (d) (G) (L1) (T): relation3 genv lenv term ≝ -| fleq_intro: ∀L2. L1 ⋕[T, d] L2 → fleq d G L1 T G L2 T +| fleq_intro: ∀L2. L1 ≡[T, d] L2 → fleq d G L1 T G L2 T . interpretation @@ -37,7 +37,7 @@ qed-. (* Basic inversion lemmas ***************************************************) -lemma fleq_inv_gen: ∀G1,G2,L1,L2,T1,T2,d. ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & L1 ⋕[T1, d] L2 & T1 = T2. +lemma fleq_inv_gen: ∀G1,G2,L1,L2,T1,T2,d. ⦃G1, L1, T1⦄ ≡[d] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≡[T1, d] L2 & T1 = T2. #G1 #G2 #L1 #L2 #T1 #T2 #d * -G2 -L2 -T2 /2 width=1 by and3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma index 36885f0e1..e8d5dac02 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fleq_fleq.ma @@ -26,9 +26,9 @@ theorem fleq_trans: ∀d. tri_transitive … (fleq d). qed-. theorem fleq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2,d. - ⦃G, L, T⦄ ⋕[d] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ⋕[d] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄. + ⦃G, L, T⦄ ≡[d] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡[d] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡[d] ⦃G2, L2, T2⦄. /3 width=5 by fleq_trans, fleq_sym/ qed-. theorem fleq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T,d. - ⦃G1, L1, T1⦄ ⋕[d] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ⋕[d] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕[d] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≡[d] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡[d] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡[d] ⦃G2, L2, T2⦄. /3 width=5 by fleq_trans, fleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index d8a174b82..dc138a492 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazyeq_4.ma". -include "basic_2/relocation/llpx_sn.ma". +include "basic_2/substitution/llpx_sn.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) @@ -26,7 +26,7 @@ interpretation 'LazyEq T d L1 L2 = (lleq d T L1 L2). definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝ - λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ⋕[T1, 0] L2 → R I L1 T1 T2. + λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R I L1 T1 T2. (* Basic inversion lemmas ***************************************************) @@ -37,103 +37,103 @@ lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( ) → ( ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2 + K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2 ) → ( ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2 ) → ( ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2 ) → ( ∀a,I,L1,L2,V,T,d. - L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → + L1 ≡[V, d]L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V → R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2 ) → ( ∀I,L1,L2,V,T,d. - L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 → + L1 ≡[V, d]L2 → L1 ≡[T, d] L2 → R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2 ) → - ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2. + ∀d,T,L1,L2. L1 ≡[T, d] L2 → R d T L1 L2. #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim H -L1 -L2 -T -d /2 width=8 by/ qed-. -lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[ⓑ{a,I}V.T, d] L2 → - L1 ⋕[V, d] L2 ∧ L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V. +lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ≡[ⓑ{a,I}V.T, d] L2 → + L1 ≡[V, d] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V. /2 width=2 by llpx_sn_inv_bind/ qed-. -lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[ⓕ{I}V.T, d] L2 → - L1 ⋕[V, d] L2 ∧ L1 ⋕[T, d] L2. +lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ≡[ⓕ{I}V.T, d] L2 → + L1 ≡[V, d] L2 ∧ L1 ≡[T, d] L2. /2 width=2 by llpx_sn_inv_flat/ qed-. (* Basic forward lemmas *****************************************************) -lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|. +lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ≡[T, d] L2 → |L1| = |L2|. /2 width=4 by llpx_sn_fwd_length/ qed-. -lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → +lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → ∨∨ |L1| ≤ i ∧ |L2| ≤ i | yinj i < d | ∃∃I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V & ⇩[i] L2 ≡ K2.ⓑ{I}V & - K1 ⋕[V, yinj 0] K2 & d ≤ yinj i. + K1 ≡[V, yinj 0] K2 & d ≤ yinj i. #L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/ * /3 width=7 by or3_intro2, ex4_4_intro/ qed-. -lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 → +lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 → ∃K2. ⇩[i] L2 ≡ K2. /2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-. -lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 → +lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 → ∃K1. ⇩[i] L1 ≡ K1. /2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-. lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d. - L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2. + L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2. /2 width=4 by llpx_sn_fwd_bind_sn/ qed-. lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d. - L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V. + L1 ≡[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V. /2 width=2 by llpx_sn_fwd_bind_dx/ qed-. lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d. - L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[V, d] L2. + L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[V, d] L2. /2 width=3 by llpx_sn_fwd_flat_sn/ qed-. lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d. - L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[T, d] L2. + L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[T, d] L2. /2 width=3 by llpx_sn_fwd_flat_dx/ qed-. (* Basic properties *********************************************************) -lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2. +lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ≡[⋆k, d] L2. /2 width=1 by llpx_sn_sort/ qed. -lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2. +lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ≡[#i, d] L2. /2 width=1 by llpx_sn_skip/ qed. lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2. + K1 ≡[V, 0] K2 → L1 ≡[#i, d] L2. /2 width=9 by llpx_sn_lref/ qed. -lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ⋕[#i, d] L2. +lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, d] L2. /2 width=1 by llpx_sn_free/ qed. -lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] L2. +lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ≡[§p, d] L2. /2 width=1 by llpx_sn_gref/ qed. lemma lleq_bind: ∀a,I,L1,L2,V,T,d. - L1 ⋕[V, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → - L1 ⋕[ⓑ{a,I}V.T, d] L2. + L1 ≡[V, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V → + L1 ≡[ⓑ{a,I}V.T, d] L2. /2 width=1 by llpx_sn_bind/ qed. lemma lleq_flat: ∀I,L1,L2,V,T,d. - L1 ⋕[V, d] L2 → L1 ⋕[T, d] L2 → L1 ⋕[ⓕ{I}V.T, d] L2. + L1 ≡[V, d] L2 → L1 ≡[T, d] L2 → L1 ≡[ⓕ{I}V.T, d] L2. /2 width=1 by llpx_sn_flat/ qed. lemma lleq_refl: ∀d,T. reflexive … (lleq d T). /2 width=1 by llpx_sn_refl/ qed. -lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ⋕[T, ∞] L2. +lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ≡[T, ∞] L2. /2 width=1 by llpx_sn_Y/ qed. lemma lleq_sym: ∀d,T. symmetric … (lleq d T). @@ -141,20 +141,20 @@ lemma lleq_sym: ∀d,T. symmetric … (lleq d T). /2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ qed-. -lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → +lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U → - dt ≤ d + e → L1 ⋕[U, d] L2. + dt ≤ d + e → L1 ≡[U, d] L2. /2 width=6 by llpx_sn_ge_up/ qed-. -lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. +lemma lleq_ge: ∀L1,L2,T,d1. L1 ≡[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ≡[T, d2] L2. /2 width=3 by llpx_sn_ge/ qed-. -lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → - L1 ⋕[ⓑ{a,I}V.T, 0] L2. +lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → + L1 ≡[ⓑ{a,I}V.T, 0] L2. /2 width=1 by llpx_sn_bind_O/ qed-. (* Advancded properties on lazy pointwise exyensions ************************) lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) → - ∀L1,L2,T,d. L1 ⋕[T, d] L2 → llpx_sn R d T L1 L2. + ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2. /2 width=3 by llpx_sn_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma index dd97ea641..a209206af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_alt.ma". +include "basic_2/substitution/llpx_sn_alt1.ma". include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) @@ -22,9 +22,9 @@ include "basic_2/substitution/lleq.ma". theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| → (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 - ) → L1 ⋕[T, d] L2. -#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt // -HL12 + ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2 + ) → L1 ≡[T, d] L2. +#L1 #L2 #T #d #HL12 #IH @llpx_sn_intro_alt1 // -HL12 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ qed. @@ -33,21 +33,21 @@ theorem lleq_ind_alt: ∀S:relation4 ynat term lenv lenv. (∀L1,L2,T,d. |L1| = |L2| → ( ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2 & S 0 V1 K1 K2 + ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2 & S 0 V1 K1 K2 ) → S d T L1 L2) → - ∀L1,L2,T,d. L1 ⋕[T, d] L2 → S d T L1 L2. -#S #IH1 #L1 #L2 #T #d #H @(llpx_sn_ind_alt … H) -L1 -L2 -T -d + ∀L1,L2,T,d. L1 ≡[T, d] L2 → S d T L1 L2. +#S #IH1 #L1 #L2 #T #d #H @(llpx_sn_ind_alt1 … H) -L1 -L2 -T -d #L1 #L2 #T #d #HL12 #IH2 @IH1 -IH1 // -HL12 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 elim (IH2 … HnT HLK1 HLK2) -IH2 -HnT -HLK1 -HLK2 /2 width=1 by and4_intro/ qed-. -theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → +theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ≡[T, d] L2 → |L1| = |L2| ∧ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & V1 = V2 & K1 ⋕[V1, 0] K2. -#L1 #L2 #T #d #H elim (llpx_sn_inv_alt … H) -H + ∧∧ I1 = I2 & V1 = V2 & K1 ≡[V1, 0] K2. +#L1 #L2 #T #d #H elim (llpx_sn_inv_alt1 … H) -H #HL12 #IH @conj // #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma index 3a510eb28..ac1329b45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma @@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma". (* Properties on supclosure *************************************************) lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. + ∀L1. L1 ≡[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U [ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 @@ -45,8 +45,8 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ qed-. lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. + ∀L1. L1 ≡[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H [ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ | * #HG #HL #HT destruct /2 width=3 by ex2_intro/ @@ -54,8 +54,8 @@ lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U qed-. lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. + ∀L1. L1 ≡[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U [ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 /3 width=3 by fqu_fqup, ex2_intro/ @@ -66,8 +66,8 @@ lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ qed-. lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐* ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[T, 0] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. + ∀L1. L1 ≡[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U⦄ & K1 ≡[U, 0] K2. #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H [ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ | * #HG #HL #HT destruct /2 width=3 by ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma index 27b16110d..cc527074c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma @@ -12,22 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_ldrop.ma". +include "basic_2/substitution/llpx_sn_ldrop.ma". include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) (* Advanced properties ******************************************************) -lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → - ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W. +lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → + ∀J,W. L1 ≡[W, 0] L2 → L1.ⓑ{J}W ≡[T, 0] L2.ⓑ{J}W. /2 width=7 by llpx_sn_bind_repl_O/ qed-. -lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2). +lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ≡[T, d] L2). /3 width=1 by llpx_sn_dec, eq_term_dec/ qed-. lemma lleq_llpx_sn_trans: ∀R. lleq_transitive R → - ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L1,L2,T,d. L1 ≡[T, d] L2 → ∀L. llpx_sn R d T L2 L → llpx_sn R d T L1 L. #R #HR #L1 #L2 #T #d #H @(lleq_ind … H) -L1 -L2 -T -d [1,2,5: /4 width=6 by llpx_sn_fwd_length, llpx_sn_gref, llpx_sn_skip, llpx_sn_sort, trans_eq/ @@ -42,109 +42,109 @@ lemma lleq_llpx_sn_trans: ∀R. lleq_transitive R → qed-. lemma lleq_llpx_sn_conf: ∀R. lleq_transitive R → - ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L1,L2,T,d. L1 ≡[T, d] L2 → ∀L. llpx_sn R d T L1 L → llpx_sn R d T L2 L. /3 width=3 by lleq_llpx_sn_trans, lleq_sym/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → +lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → d ≤ i → ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V → - ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2. + ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ≡[V, 0] K2. #L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (llpx_sn_inv_lref_ge_dx … H … HLK2) -L2 /2 width=3 by ex2_intro/ qed-. -lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → +lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → d ≤ i → ∀I,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → - ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[V, 0] K2. + ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ≡[V, 0] K2. #L1 #L2 #d #i #H #Hdi #I1 #K1 #V #HLK1 elim (llpx_sn_inv_lref_ge_sn … H … HLK1) -L1 /2 width=3 by ex2_intro/ qed-. -lemma lleq_inv_lref_ge_bi: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → +lemma lleq_inv_lref_ge_bi: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → d ≤ i → ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & K1 ⋕[V1, 0] K2 & V1 = V2. + ∧∧ I1 = I2 & K1 ≡[V1, 0] K2 & V1 = V2. /2 width=8 by llpx_sn_inv_lref_ge_bi/ qed-. -lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → +lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → d ≤ i → ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, 0] K2. + K1 ≡[V, 0] K2. #L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2 elim (lleq_inv_lref_ge_bi … HL12 … HLK1 HLK2) // qed-. -lemma lleq_inv_S: ∀L1,L2,T,d. L1 ⋕[T, d+1] L2 → +lemma lleq_inv_S: ∀L1,L2,T,d. L1 ≡[T, d+1] L2 → ∀I,K1,K2,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. + K1 ≡[V, 0] K2 → L1 ≡[T, d] L2. /2 width=9 by llpx_sn_inv_S/ qed-. -lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → - L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 → + L1 ≡[V, 0] L2 ∧ L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V. /2 width=2 by llpx_sn_inv_bind_O/ qed-. (* Advanced forward lemmas **************************************************) -lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → +lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V → i < d ∨ - ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2 & d ≤ i. + ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ≡[V, 0] K2 & d ≤ i. #L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2 [ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/ qed-. -lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → +lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → ∀I,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → i < d ∨ - ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[V, 0] K2 & d ≤ i. + ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ≡[V, 0] K2 & d ≤ i. #L1 #L2 #d #i #H #I #K1 #V #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1 [ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/ qed-. -lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → - L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 → + L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V. /2 width=2 by llpx_sn_fwd_bind_O_dx/ qed-. (* Properties on relocation *************************************************) -lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → +lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ≡[T, dt] K2 → ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → - ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ⋕[U, dt] L2. + ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ≡[U, dt] L2. /3 width=10 by llpx_sn_lift_le, lift_mono/ qed-. -lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → +lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ≡[T, dt] K2 → ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → - ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ⋕[U, dt+e] L2. + ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ≡[U, dt+e] L2. /2 width=9 by llpx_sn_lift_ge/ qed-. (* Inversion lemmas on relocation *******************************************) -lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → +lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 → ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ⋕[T, dt] K2. + ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ≡[T, dt] K2. /3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-. -lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → +lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 → ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → K1 ⋕[T, d] K2. + ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → K1 ≡[T, d] K2. /2 width=11 by llpx_sn_inv_lift_be/ qed-. -lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → +lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 → ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ dt → K1 ⋕[T, dt-e] K2. + ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ dt → K1 ≡[T, dt-e] K2. /2 width=9 by llpx_sn_inv_lift_ge/ qed-. (* Inversion lemmas on negated lazy quivalence for local environments *******) -lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ⋕[ⓑ{a,I}V.T, d] L2 → ⊥) → - (L1 ⋕[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → ⊥). +lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ≡[ⓑ{a,I}V.T, d] L2 → ⊥) → + (L1 ≡[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V → ⊥). /3 width=2 by nllpx_sn_inv_bind, eq_term_dec/ qed-. -lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ⋕[ⓕ{I}V.T, d] L2 → ⊥) → - (L1 ⋕[V, d] L2 → ⊥) ∨ (L1 ⋕[T, d] L2 → ⊥). +lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ≡[ⓕ{I}V.T, d] L2 → ⊥) → + (L1 ≡[V, d] L2 → ⊥) ∨ (L1 ≡[T, d] L2 → ⊥). /3 width=2 by nllpx_sn_inv_flat, eq_term_dec/ qed-. -lemma nlleq_inv_bind_O: ∀a,I,L1,L2,V,T. (L1 ⋕[ⓑ{a,I}V.T, 0] L2 → ⊥) → - (L1 ⋕[V, 0] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → ⊥). +lemma nlleq_inv_bind_O: ∀a,I,L1,L2,V,T. (L1 ≡[ⓑ{a,I}V.T, 0] L2 → ⊥) → + (L1 ≡[V, 0] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → ⊥). /3 width=2 by nllpx_sn_inv_bind_O, eq_term_dec/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma index 01bde31ec..bef6eeb7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma @@ -12,25 +12,25 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_leq.ma". +include "basic_2/substitution/llpx_sn_leq.ma". include "basic_2/substitution/lleq.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) (* Properties on equivalence for local environments *************************) -lemma leq_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L → - ∀L1. L1 ≃[d, ∞] L2 → L1 ⋕[T, d] L. +lemma leq_lleq_trans: ∀L2,L,T,d. L2 ≡[T, d] L → + ∀L1. L1 ≃[d, ∞] L2 → L1 ≡[T, d] L. /2 width=3 by leq_llpx_sn_trans/ qed-. -lemma lleq_leq_trans: ∀L,L1,T,d. L ⋕[T, d] L1 → - ∀L2. L1 ≃[d, ∞] L2 → L ⋕[T, d] L2. +lemma lleq_leq_trans: ∀L,L1,T,d. L ≡[T, d] L1 → + ∀L2. L1 ≃[d, ∞] L2 → L ≡[T, d] L2. /2 width=3 by llpx_sn_leq_trans/ qed-. -lemma lleq_leq_repl: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 → - ∀K2. L2 ≃[d, ∞] K2 → K1 ⋕[T, d] K2. +lemma lleq_leq_repl: ∀L1,L2,T,d. L1 ≡[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 → + ∀K2. L2 ≃[d, ∞] K2 → K1 ≡[T, d] K2. /2 width=5 by llpx_sn_leq_repl/ qed-. -lemma lleq_bind_repl_SO: ∀I1,I2,L1,L2,V1,V2,T. L1.ⓑ{I1}V1 ⋕[T, 0] L2.ⓑ{I2}V2 → - ∀J1,J2,W1,W2. L1.ⓑ{J1}W1 ⋕[T, 1] L2.ⓑ{J2}W2. +lemma lleq_bind_repl_SO: ∀I1,I2,L1,L2,V1,V2,T. L1.ⓑ{I1}V1 ≡[T, 0] L2.ⓑ{I2}V2 → + ∀J1,J2,W1,W2. L1.ⓑ{J1}W1 ≡[T, 1] L2.ⓑ{J2}W2. /2 width=5 by llpx_sn_bind_repl_SO/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma index a3a276ff3..abee448a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -19,14 +19,14 @@ include "basic_2/substitution/lleq_ldrop.ma". theorem lleq_trans: ∀d,T. Transitive … (lleq d T). /2 width=3 by lleq_llpx_sn_trans/ qed-. -theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2. +theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ≡[d, T] L1→ L ≡[d, T] L2 → L1 ≡[d, T] L2. /3 width=3 by lleq_trans, lleq_sym/ qed-. -theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2. +theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ≡[d, T] L → L2 ≡[d, T] L → L1 ≡[d, T] L2. /3 width=3 by lleq_trans, lleq_sym/ qed-. -(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1⋕[T, d] L → - ∀L2. (L ⋕[T, d] L2 → ⊥) → (L1 ⋕[T, d] L2 → ⊥). +(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1≡[T, d] L → + ∀L2. (L ≡[T, d] L2 → ⊥) → (L1 ≡[T, d] L2 → ⊥). /3 width=3 by lleq_canc_sn/ qed-. works with /4 width=8/ so lleq_canc_sn is more convenient *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma new file mode 100644 index 000000000..7e071f24d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma @@ -0,0 +1,250 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lift_neg.ma". +include "basic_2/relocation/ldrop_ldrop.ma". +include "basic_2/substitution/llpx_sn.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* alternative definition of llpx_sn (recursive) *) +inductive llpx_sn_alt1 (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝ +| llpx_sn_alt1_intro: ∀L1,L2,T,d. + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2 + ) → + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt1 R 0 V1 K1 K2 + ) → |L1| = |L2| → llpx_sn_alt1 R d T L1 L2 +. + +(* Compact definition of llpx_sn_alt1 ****************************************) + +lemma llpx_sn_alt1_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| → + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt1 R 0 V1 K1 K2 + ) → llpx_sn_alt1 R d T L1 L2. +#R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt1_intro // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 +elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by conj/ +qed. + +lemma llpx_sn_alt1_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv. + (∀L1,L2,T,d. |L1| = |L2| → ( + ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt1 R 0 V1 K1 K2 & S 0 V1 K1 K2 + ) → S d T L1 L2) → + ∀L1,L2,T,d. llpx_sn_alt1 R d T L1 L2 → S d T L1 L2. +#R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d +#L1 #L2 #T #d #H1 #H2 #HL12 #IH2 @IH -IH // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 +elim (H1 … HnT HLK1 HLK2) -H1 /4 width=8 by and4_intro/ +qed-. + +lemma llpx_sn_alt1_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt1 R d T L1 L2 → + |L1| = |L2| ∧ + ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt1 R 0 V1 K1 K2. +#R #L1 #L2 #T #d #H @(llpx_sn_alt1_ind_alt … H) -L1 -L2 -T -d +#L1 #L2 #T #d #HL12 #IH @conj // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 +elim (IH … HnT HLK1 HLK2) -IH -HnT -HLK1 -HLK2 /2 width=1 by and3_intro/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma llpx_sn_alt1_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn_alt1 R d (ⓕ{I}V.T) L1 L2 → + llpx_sn_alt1 R d V L1 L2 ∧ llpx_sn_alt1 R d T L1 L2. +#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt1_inv_alt … H) -H +#HL12 #IH @conj @llpx_sn_alt1_intro_alt // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 +elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 // +/3 width=8 by nlift_flat_sn, nlift_flat_dx, and3_intro/ +qed-. + +lemma llpx_sn_alt1_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn_alt1 R d (ⓑ{a,I}V.T) L1 L2 → + llpx_sn_alt1 R d V L1 L2 ∧ llpx_sn_alt1 R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_alt1_inv_alt … H) -H +#HL12 #IH @conj @llpx_sn_alt1_intro_alt [1,3: normalize // ] -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 +[ elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 + /3 width=9 by nlift_bind_sn, and3_intro/ +| lapply (yle_inv_succ1 … Hdi) -Hdi * #Hdi #Hi + lapply (ldrop_inv_drop1_lt … HLK1 ?) -HLK1 /2 width=1 by ylt_O/ #HLK1 + lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/ #HLK2 + elim (IH … HLK1 HLK2) -IH -HLK1 -HLK2 /2 width=1 by and3_intro/ + @nlift_bind_dx