From ff7754f834f937bfe2384c7703cf63f552885395 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 14 Jun 2014 20:15:10 +0000 Subject: [PATCH] reorganization of the "static" component: from now on we use the non-stratified version of the static type assignment, as in basic_1 --- .../lambdadelta/basic_2/computation/cpds.ma | 21 +- .../basic_2/computation/cpds_aaa.ma | 6 +- .../basic_2/computation/cpds_cpds.ma | 24 +- .../basic_2/computation/cpds_lift.ma | 7 +- .../basic_2/computation/cpxs_aaa.ma | 8 +- .../basic_2/computation/cpxs_lift.ma | 32 +-- .../basic_2/computation/csx_aaa.ma | 4 +- .../basic_2/computation/fpbg_lift.ma | 12 +- .../basic_2/computation/fpbs_aaa.ma | 4 +- .../basic_2/computation/fpbs_lift.ma | 24 +- .../basic_2/computation/fpbu_lift.ma | 16 +- .../basic_2/computation/fsb_aaa.ma | 4 +- .../basic_2/computation/lpxs_aaa.ma | 8 +- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 46 ++++ .../basic_2/dynamic/lsubsv_cpds.ma | 6 +- .../basic_2/dynamic/lsubsv_ldrop.ma | 65 ----- .../basic_2/dynamic/lsubsv_lstas.ma | 90 ++++++ .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 4 +- .../lambdadelta/basic_2/dynamic/snv.ma | 14 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 34 +-- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 126 ++++----- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 30 +- .../lambdadelta/basic_2/dynamic/snv_lstas.ma | 63 +++++ .../basic_2/dynamic/snv_lstas_lpr.ma | 151 +++++++++++ .../basic_2/dynamic/snv_preserve.ma | 90 +++--- .../basic_2/equivalence/cpcs_aaa.ma | 6 +- .../lambdadelta/basic_2/equivalence/cpes.ma | 21 +- .../lambdadelta/basic_2/etc/da/da.etc | 28 -- .../lambdadelta/basic_2/etc/da/da_da.etc | 8 - .../lambdadelta/basic_2/etc/da/da_lift.etc | 23 -- .../etc/{lsubss => lsubss2}/lsubss.etc | 0 .../etc/{lsubss => lsubss2}/lsubss_cpcs.etc | 0 .../etc/{lsubss => lsubss2}/lsubss_etc.etc | 0 .../etc/{lsubss => lsubss2}/lsubss_ldrop.etc | 0 .../etc/{lsubss => lsubss2}/lsubss_ssta.etc | 0 .../aaa_ssta.ma => etc/ssta1/aaa_ssta.etc} | 0 .../lambdadelta/basic_2/etc/ssta1/cpds.etc | 46 ++++ .../basic_2/etc/ssta1/cpds_aaa.etc | 25 ++ .../basic_2/etc/ssta1/cpds_cpds.etc | 75 +++++ .../basic_2/etc/ssta1/cpds_lift.etc | 35 +++ .../lambdadelta/basic_2/etc/ssta1/cpes.etc | 46 ++++ .../basic_2/etc/ssta1/cpx_lift.etc | 256 ++++++++++++++++++ .../basic_2/etc/ssta1/cpxs_lift.etc | 118 ++++++++ .../basic_2/etc/ssta1/fpb_lift.etc | 25 ++ .../basic_2/etc/ssta1/fpbg_lift.etc | 28 ++ .../basic_2/etc/ssta1/fpbs_lift.etc | 37 +++ .../basic_2/etc/ssta1/fpbu_lift.etc | 32 +++ .../lsstas.ma => etc/ssta1/lsstas.etc} | 0 .../ssta1/lsstas_aaa.etc} | 0 .../ssta1/lsstas_alt.etc} | 0 .../ssta1/lsstas_lift.etc} | 0 .../ssta1/lsstas_lsstas.etc} | 0 .../basic_2/etc/ssta1/lsubsv_cpds.etc | 31 +++ .../ssta1/lsubsv_lsstas.etc} | 0 .../basic_2/etc/ssta1/lsubsv_snv.etc | 52 ++++ .../lambdadelta/basic_2/etc/ssta1/snv.etc | 119 ++++++++ .../lambdadelta/basic_2/etc/ssta1/snv_aaa.etc | 66 +++++ .../basic_2/etc/ssta1/snv_cpcs.etc | 169 ++++++++++++ .../basic_2/etc/ssta1/snv_da_lpr.etc | 94 +++++++ .../basic_2/etc/ssta1/snv_lift.etc | 104 +++++++ .../lambdadelta/basic_2/etc/ssta1/snv_lpr.etc | 132 +++++++++ .../ssta1/snv_lsstas.etc} | 0 .../ssta1/snv_lsstas_lpr.etc} | 0 .../basic_2/etc/ssta1/snv_preserve.etc | 146 ++++++++++ .../{static/ssta.ma => etc/ssta1/ssta.etc} | 0 .../ssta_lift.ma => etc/ssta1/ssta_lift.etc} | 0 .../ssta1/ssta_llpx_sn.etc} | 0 .../ssta_ssta.ma => etc/ssta1/ssta_ssta.etc} | 0 .../ssta1/statictype_6.etc} | 0 .../ssta1/statictypestar_7.etc} | 0 .../ssta1/statictypestaralt_7.etc} | 0 .../basic_2/etc/{ssta => ssta2}/ssta.etc | 0 .../basic_2/etc/{ssta => ssta2}/ssta_aaa.etc | 0 .../basic_2/etc/{ssta => ssta2}/ssta_lift.etc | 0 .../basic_2/etc/{ssta => ssta2}/ssta_ssta.etc | 0 .../etc/{ssta => ssta2}/statictype_7.etc | 0 .../basic_2/etc/{sstas => sstas2}/sstas.etc | 0 .../etc/{sstas => sstas2}/sstas_aaa.etc | 0 .../etc/{sstas => sstas2}/sstas_lift.etc | 0 .../etc/{sstas => sstas2}/sstas_sstas.etc | 0 .../lambdadelta/basic_2/etc/sta/sta_aaa.etc | 13 - .../relations/statictype_5.ma} | 0 .../notation/relations/statictypestar_6.ma | 19 ++ .../notation/relations/statictypestaralt_6.ma | 19 ++ .../lambdadelta/basic_2/reduction/cpx_lift.ma | 33 +-- .../lambdadelta/basic_2/reduction/fpb_aaa.ma | 4 +- .../lambdadelta/basic_2/reduction/fpb_lift.ma | 6 +- .../lambdadelta/basic_2/reduction/lpx_aaa.ma | 18 +- .../basic_2/static/{aaa_da.ma => da_aaa.ma} | 19 +- .../lambdadelta/basic_2/static/da_sta.ma | 74 +++++ .../lambdadelta/basic_2/static/lsuba.ma | 56 +++- .../lambdadelta/basic_2/static/lsuba_aaa.ma | 26 +- .../lambdadelta/basic_2/static/lsuba_ldrop.ma | 63 ----- .../{etc/sta/sta.etc => static/sta.ma} | 59 +--- .../lambdadelta/basic_2/static/sta_aaa.ma | 52 ++++ .../sta/sta_lift.etc => static/sta_lift.ma} | 90 +++--- .../lambdadelta/basic_2/static/sta_llpx_sn.ma | 43 +++ .../sta/sta_sta.etc => static/sta_sta.ma} | 8 +- .../lambdadelta/basic_2/unfold/lstas.ma | 133 +++++++++ .../lambdadelta/basic_2/unfold/lstas_aaa.ma | 23 ++ .../lambdadelta/basic_2/unfold/lstas_alt.ma | 102 +++++++ .../lambdadelta/basic_2/unfold/lstas_da.ma | 27 ++ .../lambdadelta/basic_2/unfold/lstas_lift.ma | 81 ++++++ .../lambdadelta/basic_2/unfold/lstas_lstas.ma | 51 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 28 +- 107 files changed, 3047 insertions(+), 627 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/da/da.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/da/da_da.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/da/da_lift.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsubss => lsubss2}/lsubss.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsubss => lsubss2}/lsubss_cpcs.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsubss => lsubss2}/lsubss_etc.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsubss => lsubss2}/lsubss_ldrop.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lsubss => lsubss2}/lsubss_ssta.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/aaa_ssta.ma => etc/ssta1/aaa_ssta.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_aaa.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_cpds.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpds_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpes.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpx_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/cpxs_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lsstas.ma => etc/ssta1/lsstas.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lsstas_aaa.ma => etc/ssta1/lsstas_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lsstas_alt.ma => etc/ssta1/lsstas_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lsstas_lift.ma => etc/ssta1/lsstas_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{unfold/lsstas_lsstas.ma => etc/ssta1/lsstas_lsstas.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/lsubsv_lsstas.ma => etc/ssta1/lsubsv_lsstas.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/snv_lsstas.ma => etc/ssta1/snv_lsstas.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/snv_lsstas_lpr.ma => etc/ssta1/snv_lsstas_lpr.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_preserve.etc rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta.ma => etc/ssta1/ssta.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta_lift.ma => etc/ssta1/ssta_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta_llpx_sn.ma => etc/ssta1/ssta_llpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{static/ssta_ssta.ma => etc/ssta1/ssta_ssta.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/statictype_6.ma => etc/ssta1/statictype_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/statictypestar_7.ma => etc/ssta1/statictypestar_7.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/statictypestaralt_7.ma => etc/ssta1/statictypestaralt_7.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ssta => ssta2}/ssta.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ssta => ssta2}/ssta_aaa.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ssta => ssta2}/ssta_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ssta => ssta2}/ssta_ssta.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{ssta => ssta2}/statictype_7.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{sstas => sstas2}/sstas.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{sstas => sstas2}/sstas_aaa.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{sstas => sstas2}/sstas_lift.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{sstas => sstas2}/sstas_sstas.etc (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc/sta/statictype_5.etc => notation/relations/statictype_5.ma} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestaralt_6.ma rename matita/matita/contribs/lambdadelta/basic_2/static/{aaa_da.ma => da_aaa.ma} (63%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/da_sta.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/sta/sta.etc => static/sta.ma} (73%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/sta_aaa.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/sta/sta_lift.etc => static/sta_lift.ma} (53%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/sta_llpx_sn.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/sta/sta_sta.etc => static/sta_sta.ma} (94%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lstas.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma index 692f1fb0a..bf329f737 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma @@ -13,34 +13,35 @@ (**************************************************************************) include "basic_2/notation/relations/dpredstar_6.ma". -include "basic_2/unfold/lsstas.ma". +include "basic_2/static/da.ma". +include "basic_2/unfold/lstas.ma". include "basic_2/computation/cprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) definition cpds: ∀h. sd h → relation4 genv lenv term term ≝ λh,g,G,L,T1,T2. - ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. + ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. interpretation "decomposed extended parallel computation (term)" 'DPRedStar h g G L T1 T2 = (cpds h g G L T1 T2). (* Basic properties *********************************************************) -lemma ssta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h, g] T → - ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/3 width=7/ qed. +lemma sta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → + ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. +/3 width=7 by sta_lstas, ex4_3_intro/ qed. -lemma lsstas_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7/ qed. +lemma lstas_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. +/2 width=7 by ex4_3_intro/ qed. lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7/ qed. +/2 width=7 by lstar_O, ex4_3_intro/ qed. lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g] T. -/2 width=2/ qed. +/2 width=2 by cprs_cpds/ qed. lemma cpds_strap1: ∀h,g,G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -#h #g #G #L #T1 #T #T2 * /3 width=9/ +#h #g #G #L #T1 #T #T2 * /3 width=9 by cprs_strap1, ex4_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma index 039e82abf..1c45e715b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lsstas_aaa.ma". +include "basic_2/unfold/lstas_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". include "basic_2/computation/cpds.ma". @@ -20,6 +20,6 @@ include "basic_2/computation/cpds.ma". (* Properties on atomic arity assignment for terms **************************) -lemma aaa_cpds_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L). -#h #g #G #L #A #T #HT #U * /3 width=6 by aaa_lsstas_conf, aaa_cprs_conf/ +lemma cpds_aaa_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L). +#h #g #G #L #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma index ef1e56d90..9bd6b2d87 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lsstas_lsstas.ma". +include "basic_2/unfold/lstas_lstas.ma". include "basic_2/computation/lprs_cprs.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/cpds.ma". @@ -22,12 +22,12 @@ include "basic_2/computation/cpds.ma". (* Advanced properties ******************************************************) lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. + ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. #h #g #G #L #T1 #T #T2 #l #Hl #HT1 * #T0 #l0 #l1 #Hl10 #HT #HT0 #HT02 -lapply (ssta_da_conf … HT1 … Hl) (plus_minus_m_m (l2-l1) 1 ?) -[ /4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/ +[ /4 width=5 by cpxs_strap1, sta_cpx, lt_to_le/ | /2 width=1 by monotonic_le_minus_r/ ] qed. @@ -88,11 +88,11 @@ lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] ] qed-. -lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-. +lemma fquq_lstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +/3 width=5 by fquq_cpxs_trans, lstas_cpxs/ qed-. lemma fqup_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → ∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → @@ -111,8 +111,8 @@ lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] ] qed-. -lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-. +lemma fqus_lstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +/3 width=6 by fqus_cpxs_trans, lstas_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index f1b70f0c7..0a42fb1f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -32,7 +32,7 @@ fact aaa_ind_csx_aux: ∀h,g,G,L,A. ∀R:predicate term. (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #g #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by aaa_cpx_conf/ +#h #g #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ qed-. lemma aaa_ind_csx: ∀h,g,G,L,A. ∀R:predicate term. @@ -47,7 +47,7 @@ fact aaa_ind_csx_alt_aux: ∀h,g,G,L,A. ∀R:predicate term. (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #g #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by aaa_cpxs_conf/ +#h #g #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by cpxs_aaa_conf/ qed-. lemma aaa_ind_csx_alt: ∀h,g,G,L,A. ∀R:predicate term. 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 c67134ee3..6b5b5719b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -19,10 +19,10 @@ 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⦄. -/5 width=5 by fpbc_fpbg, fpbu_fpbc, lsstas_fpbu/ qed. +lemma lstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = 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, lstas_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⦄. -/4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ qed. +lemma sta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •[h] T2 → ⦃G, L, T1⦄ >≡[h, g] ⦃G, L, T2⦄. +/4 width=2 by fpbc_fpbg, fpbu_fpbc, sta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma index 7cef76336..ad075940e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma @@ -19,9 +19,9 @@ include "basic_2/computation/fpbs.ma". (* Properties on atomic arity assignment for terms **************************) -lemma aaa_fpbs_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → +lemma fpbs_aaa_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=2 by ex_intro/ #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A -/2 width=8 by aaa_fpb_conf/ +/2 width=8 by fpb_aaa_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index ab8f6608d..93f6bf7c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -20,18 +20,18 @@ include "basic_2/computation/fpbs.ma". (* Advanced properties ******************************************************) -lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. +lemma lstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +/3 width=5 by cpxs_fpbs, lstas_cpxs/ qed. -lemma ssta_fpbs: ∀h,g,G,L,T,U,l. - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → - ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/4 width=2 by fpb_fpbs, ssta_fpb/ qed. +lemma sta_fpbs: ∀h,g,G,L,T,U,l. + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h] U → + ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. +/4 width=2 by fpb_fpbs, sta_fpb/ qed. (* Note: this is used in the closure proof *) -lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. - ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → - ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. -/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, ssta_cpx, fpb_cpx/ qed. +lemma cpr_lpr_sta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h] U2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, sta_cpx, fpb_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma index d7b48650e..a76af75e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/ssta_ssta.ma". +include "basic_2/static/sta_sta.ma". include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbu.ma". @@ -20,13 +20,13 @@ include "basic_2/computation/fpbu.ma". (* Advanced properties ******************************************************) -lemma lsstas_fpbu: ∀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⦄. -/4 width=5 by fpbu_cpxs, lsstas_cpxs/ qed. +lemma lstas_fpbu: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → (T1 = T2 → ⊥) → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. +/4 width=5 by fpbu_cpxs, lstas_cpxs/ qed. -lemma ssta_fpbu: ∀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⦄. +lemma sta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •[h] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. #h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=5 by ssta_lsstas, lsstas_fpbu/ #H destruct -elim (ssta_inv_refl_pos … HT1 … HT12) +/3 width=5 by sta_lstas, lstas_fpbu/ #H destruct +elim (sta_inv_refl_pos … HT1 … HT12) qed. 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 e8f4d2015..271839873 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -38,7 +38,7 @@ fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term. ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. #h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // -#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1 +#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpbu_fwd_fpbs/ qed-. @@ -58,7 +58,7 @@ fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term. ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. #h #g #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // -#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1 +#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpbg_fwd_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma index 89122eb55..d335f57da 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_aaa.ma @@ -19,12 +19,12 @@ include "basic_2/computation/lpxs.ma". (* Properties about atomic arity assignment on terms ************************) -lemma aaa_lpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → +lemma lpxs_aaa_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. #h #g #G #L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/ +@(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by lpx_aaa_conf/ qed-. -lemma aaa_lprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → +lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A. -/3 width=5 by lprs_lpxs, aaa_lpxs_conf/ qed-. +/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index ec0832ad4..7d1faa892 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -118,3 +118,49 @@ lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2. /3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/ qed-. + +(* Note: the constant 0 cannot be generalized *) +lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → + ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → + ∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. +#h #g #G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H + elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ + ] +| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #s #e #H + elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ + ] +] +qed-. + +(* Note: the constant 0 cannot be generalized *) +lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → + ∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 → + ∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. +#h #g #G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H + elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ + ] +| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #s #e #H + elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H + <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ + | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma index a4d4cff8d..2604db925 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/lsubsv_lsstas.ma". +include "basic_2/dynamic/lsubsv_lstas.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) @@ -23,9 +23,9 @@ lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T. #h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12 lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2 -elim (lsubsv_lsstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0 +elim (lsubsv_lstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0 lapply (lsubsv_fwd_lsubd … HL12) -HL12 #HL12 lapply (lsubd_da_trans … Hl1 … HL12) -L2 #Hl1 lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02 -elim (cpcs_inv_cprs … HT02) -HT02 /3 width=7/ +elim (cpcs_inv_cprs … HT02) -HT02 /3 width=7 by ex2_intro, ex4_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma deleted file mode 100644 index 3897a75fa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma +++ /dev/null @@ -1,65 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/dynamic/lsubsv.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) - -(* Properties concerning basic local environment slicing ********************) - -(* Note: the constant 0 cannot be generalized *) -lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → - ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. -#h #g #G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ - ] -| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #s #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 - [ destruct - elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ - | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/ - ] -] -qed-. - -(* Note: the constant 0 cannot be generalized *) -lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → - ∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. -#h #g #G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ - ] -| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #s #e #H - elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 - [ destruct - elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H - <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/ - | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma new file mode 100644 index 000000000..fe3432732 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/da_sta.ma". +include "basic_2/static/lsubd_da.ma". +include "basic_2/unfold/lstas_alt.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/dynamic/lsubsv_lsubd.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties on nat-iterated static type assignment ************************) + +lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, l1] U2 → + ∀l2. l1 ≤ l2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l2 → + ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. +#h #g #G #L2 #T #U #l1 #H @(lstas_ind_alt … H) -G -L2 -T -U -l1 +[1,2: /2 width=3 by ex2_intro/ +| #G #L2 #K2 #X #Y #U #i #l1 #HLK2 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 + elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 + lapply (ldrop_mono … HK0 … HLK2) -HK0 #H destruct + elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ] + [ #HK12 #H destruct + elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY + lapply (ldrop_fwd_drop2 … HLK1) #H + elim (lift_total T 0 (i+1)) + /3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/ + | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct + ] +| #G #L2 #K2 #X #Y #Y0 #U #i #l1 #HLK2 #HXY0 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 + elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ] + lapply (ldrop_mono … HK0 … HLK2) -HK0 #H2 destruct + lapply (le_plus_to_le_r … Hl12) -Hl12 #Hl12 + elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubsv_inv_pair2 … H) -H * #K1 + [ #HK12 #H destruct + lapply (lsubsv_fwd_lsubd … HK12) #H + lapply (lsubd_da_trans … HV0 … H) -H #H + elim (da_inv_sta … H) -H + elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y1 + lapply (ldrop_fwd_drop2 … HLK1) + elim (lift_total Y1 0 (i+1)) + /3 width=12 by lstas_ldec, cpcs_lift, ex2_intro/ + | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct + lapply (da_mono … HX … HV0) -HX #H destruct + elim (IHXY … Hl12 HV0 … HK12) -K2 #Y0 #HXY0 #HY0 + elim (da_inv_sta … HV) -HV #W #HVW + elim (lstas_total … HVW (l1+1)) -W #W #HVW + lapply (HVX … Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0 + lapply (cpcs_trans … HWY0 … HY0) -Y0 + lapply (ldrop_fwd_drop2 … HLK1) + elim (lift_total W 0 (i+1)) + /4 width=12 by lstas_ldef, lstas_cast, cpcs_lift, ex2_intro/ + ] +| #a #I #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 + lapply (da_inv_bind … Hl2) -Hl2 #Hl2 + elim (IHTU2 … Hl2 (L1.ⓑ{I}V2) …) + /3 width=3 by lsubsv_pair, lstas_bind, cpcs_bind_dx, ex2_intro/ +| #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 + lapply (da_inv_flat … Hl2) -Hl2 #Hl2 + elim (IHTU2 … Hl2 … HL12) -L2 + /3 width=5 by lstas_appl, cpcs_flat, ex2_intro/ +| #G #L2 #W2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12 + lapply (da_inv_flat … Hl2) -Hl2 #Hl2 + elim (IHTU2 … Hl2 … HL12) -L2 + /3 width=3 by lstas_cast, ex2_intro/ +] +qed-. + +lemma lsubsv_sta_trans: ∀h,g,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •[h] U2 → + ∀l. ⦃G, L2⦄ ⊢ T ▪[h, g] l+1 → + ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∃∃U1. ⦃G, L1⦄ ⊢ T •[h] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. +#h #g #G #L2 #T #U2 #H #l #HTl #L1 #HL12 +elim (lsubsv_lstas_trans … U2 1 … HTl … HL12) +/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index e4596e7d4..887107b80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -35,7 +35,7 @@ lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → /4 width=1 by snv_bind, lsubsv_pair/ | #a #G #L2 #V #W #W0 #T #U #l #_ #_ #HVl #HVW #HW0 #HTU #IHV #IHT #L1 #HL12 lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 - elim (lsubsv_ssta_trans … HVW … HVl … HL12) -HVW #W1 #HVW1 #HW1 + elim (lsubsv_sta_trans … HVW … HVl … HL12) -HVW #W1 #HVW1 #HW1 lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10 lapply (lsubd_da_trans … HVl L1 ?) -HVl /2 width=1 by lsubsv_fwd_lsubd/ #HVl elim (lsubsv_cpds_trans … HTU … HL12) -HTU #X #HTU #H @@ -45,7 +45,7 @@ lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → /4 width=11 by snv_appl, cpds_cprs_trans, cprs_bind/ | #G #L2 #W #T #U #l #_ #_ #HTl #HTU #HUW #IHW #IHT #L1 #HL12 lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW - elim (lsubsv_ssta_trans … HTU … HTl … HL12) -HTU #U0 #HTU0 #HU0 + elim (lsubsv_sta_trans … HTU … HTl … HL12) -HTU #U0 #HTU0 #HU0 lapply (lsubd_da_trans … HTl L1 ?) -HTl /4 width=5 by lsubsv_fwd_lsubd, snv_cast, cpcs_trans/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 7bdef30fa..11e8bea80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -20,7 +20,7 @@ include "basic_2/equivalence/cpcs.ma". definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝ λh,g,l,G,L,V,W. ∀V0,W0,l0. - l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, g, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, g, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0. + l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0. (* activate genv *) inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ @@ -28,10 +28,10 @@ inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ | snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) | snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T) | snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T → - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h, g] W → ⦃G, L⦄ ⊢ W ➡* W0 → + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h] W → ⦃G, L⦄ ⊢ W ➡* W0 → ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T) | snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T → - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T) + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T) . interpretation "stratified native validity (term)" @@ -84,7 +84,7 @@ lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h] W & ⦃G, L⦄ ⊢ W ➡* W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. #h #g #G #L #X * -L -X [ #G #L #k #V #T #H destruct @@ -97,13 +97,13 @@ qed-. lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h] W & ⦃G, L⦄ ⊢ W ➡* W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. /2 width=3 by snv_inv_appl_aux/ qed-. fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h] U & ⦃G, L⦄ ⊢ U ⬌* W. #h #g #G #L #X * -G -L -X [ #G #L #k #W #T #H destruct | #I #G #L #K #V #i #_ #_ #W #T #H destruct @@ -115,5 +115,5 @@ qed-. lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] → ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h] U & ⦃G, L⦄ ⊢ U ⬌* W. /2 width=3 by snv_inv_cast_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index 20d72ef3e..cf5e7fcb1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/static/da_aaa.ma". +include "basic_2/unfold/lstas_lift.ma". include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/cpds_aaa.ma". include "basic_2/equivalence/cpcs_aaa.ma". @@ -23,38 +25,38 @@ include "basic_2/dynamic/snv.ma". lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. #h #g #G #L #T #H elim H -G -L -T -[ /2 width=2/ -| #I #G #L #K #V #i #HLK #_ * /3 width=6/ -| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ +[ /2 width=2 by aaa_sort, ex_intro/ +| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/ +| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/ | #a #G #L #V #W #W0 #T #U #l #_ #_ #Hl #HVW #HW0 #HTU * #B #HV * #X #HT - lapply (aaa_cpds_conf h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) - lapply (aaa_cpds_conf … HT … HTU) -HTU #H + lapply (cpds_aaa_conf h g … HV W0 ?) [ -HTU /3 width=4 by cpds_strap1, sta_cprs_cpds/ ] -W #HW0 (**) (* auto fail without -HTU *) + lapply (cpds_aaa_conf … HT … HTU) -HTU #H elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct - lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ + lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/ | #G #L #W #T #U #l #_ #_ #_ #HTU #HUW * #B #HW * #A #HT - lapply (aaa_ssta_conf … HT … HTU) -HTU #H - lapply (aaa_cpcs_mono … HUW … H … HW) -HUW -H #H destruct /3 width=3/ + lapply (sta_aaa_conf … HT … HTU) -HTU #H + lapply (cpcs_aaa_mono … HUW … H … HW) -HUW -H #H destruct /3 width=3 by aaa_cast, ex_intro/ ] qed-. lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_csx/ qed-. (* Advanced forward lemmas **************************************************) lemma snv_fwd_da: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_da/ +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_da/ qed-. -lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃U. ⦃G, L⦄ ⊢ T •[h, g] U. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_ssta/ +lemma snv_fwd_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃U. ⦃G, L⦄ ⊢ T •[h] U. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_sta/ qed-. -lemma snv_lsstas_fwd_correct: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g, l] T2 → - ∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2. +lemma snv_lstas_fwd_correct: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, l] T2 → + ∃U2. ⦃G, L⦄ ⊢ T2 •[h] U2. #h #g #G #L #T1 #T2 #l #HT1 #HT12 -elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by lsstas_fwd_correct/ +elim (snv_fwd_sta … HT1) -HT1 /2 width=5 by lstas_fwd_correct/ qed-. (* Advanced properties ******************************************************) @@ -62,5 +64,5 @@ qed-. lemma snv_scast: ∀h,g,G,L,V,W,l. ⦃G, L⦄ ⊢ V ¡[h, g] → ⦃G, L⦄ ⊢ W ¡[h, g] → scast h g l G L V W → ⦃G, L⦄ ⊢V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ ⓝW.V ¡[h, g]. #h #g #G #L #V #W #l #HV #HW #H #Hl -elim (snv_fwd_ssta … HV) /4 width=6 by snv_cast, ssta_lsstas/ +elim (snv_fwd_sta … HV) /4 width=6 by snv_cast, sta_lstas/ qed-. 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 e73f809fc..2aeeea06d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lsstas_lsstas.ma". +include "basic_2/unfold/lstas_lstas.ma". include "basic_2/computation/fpbs_lift.ma". include "basic_2/computation/fpbg_fleq.ma". include "basic_2/equivalence/cpes_cpds.ma". @@ -32,17 +32,17 @@ definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. -definition IH_lsstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λ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 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λ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, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -definition IH_snv_lsstas: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → - ∀U. ⦃G, L⦄ ⊢ T •*[h, g, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g]. +definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → + ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g]. (* Properties for the preservation results **********************************) @@ -75,27 +75,27 @@ fact da_cpcs_aux: ∀h,g,G0,L0,T0. 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] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → - ∀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. +fact sta_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_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] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. #h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12 -/3 width=3 by lsstas_inv_SO, ssta_lsstas, ex2_intro/ +/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ 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] → - ∀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 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +fact lstas_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_lstas_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, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H @(cprs_ind … H) -T2 [ /2 width=10 by/ ] #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 @@ -108,54 +108,54 @@ elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 /4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ 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] → - ∀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] → - ∀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. +fact lstas_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_lstas_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, l] U1 → + ∀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, 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 elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 -elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 -lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ +elim (lstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 +elim (lstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 +lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ 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] → - ∀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] → - ∀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. +fact snv_sta_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas 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] U → ⦃G, L⦄ ⊢ U ¡[h, g]. +/3 width=8 by lstas_inv_SO, sta_lstas/ qed-. + +fact lstas_cpds_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas 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_lstas_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, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → + ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 lapply (da_mono … H … Hl1) -H #H destruct -lapply (lsstas_da_conf … HTU1 … Hl1) #Hl12 +lapply (lstas_da_conf … HTU1 … Hl1) #Hl12 elim (le_or_ge l2 l) #Hl2 -[ lapply (lsstas_conf_le … HTU1 … HT1T) -HT1T +[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ -| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l - lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 - elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2 - /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l, ex3_2_intro/ +| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l + lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 + elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2 + /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l, ex3_2_intro/ ] 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) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_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 → 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 dd56de7a2..d7f639251 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,7 +22,7 @@ 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_lstas 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. @@ -69,11 +69,11 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (da_inv_bind … Hl) -Hl #Hl elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3 lapply (cprs_div … HW3 … HW10) -W3 #HWW1 - lapply (ssta_da_conf … HVW1 … Hl0) ≡[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_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_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. @@ -56,7 +56,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0 - elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 + elim (sta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10 @@ -69,28 +69,28 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 lapply (cprs_div … HW10 … HW230) -W30 #HW120 - lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10 - lapply (ssta_da_conf … HVW1 … Hl0) ≡[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_lstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas 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 + >(lstas_inv_sort1 … H2) -X // +| #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 + [ lapply (lstas_inv_O … H2) -H2 #H destruct // ] + elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0 + elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l ] #HLK1 [ #Hl1 | #Hl #H ] + lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H0 destruct + elim (lstas_inv_lref1 … H2) -H2 * #K0 #Y0 #X0 [2,4: #Y1 ] #HLK0 [1,2: #HY01 ] #HYX0 #HX0 + lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct + [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] + lapply (fqup_lref … G1 … HLK1) #H + lapply (ldrop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/ +| #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #HV1 #HT1 + lapply (da_inv_bind … Hl1) -Hl1 #Hl1 + elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/ +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct + elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 + lapply (da_inv_flat … Hl1) -Hl1 #Hl1 + elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct + lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1 + elim (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2 + elim (lstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l + elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02 + elim (cprs_inv_abst … HU02) -HU02 #HW02 #_ + /3 width=7 by snv_appl, cprs_trans/ +| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 + [ lapply (lstas_inv_O … H2) -H2 #H destruct // ] + elim (snv_inv_cast … H1) -H1 + lapply (da_inv_flat … Hl1) -Hl1 + lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma new file mode 100644 index 000000000..616becd30 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma @@ -0,0 +1,151 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cpds_cpds.ma". +include "basic_2/dynamic/snv_aaa.ma". +include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/lsubsv_lstas.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on sn parallel reduction for local environments ***************) + +fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas 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_lstas_cpr_lpr h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_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 + >(lstas_inv_sort1 … H2) -X2 + >(cpr_inv_sort1 … H3) -X3 /2 width=3 by ex2_intro/ +| #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 + [ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ] + elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0 + elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l0 ] #HLK1 [ #HVl1 | #HWl1 #H destruct ] + lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct + elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #W0 [2,4: #X0 ] #HK0 [1,2: #_ -X0 ] #HVW0 #HX2 + lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct + [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] + lapply (fqup_lref … G1 … HLK1) #HKV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct + lapply (ldrop_fwd_drop2 … HLK2) #H2 + elim (cpr_inv_lref1 … H3) -H3 + [1,3: #H destruct -HLK1 + |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0 + lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct + ] + [ lapply (IH2 … HWl1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H + elim (da_inv_sta … H) -H + elim (IH1 … HWl1 … HVW0 … HW12 … HK12) -IH1 -HVW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 + elim (lift_total V2 0 (i+1)) + /3 width=12 by cpcs_lift, lstas_ldec, ex2_intro/ + | elim (IH1 … HVl1 … HVW0 … HV12 … HK12) -IH1 -HVl1 -HVW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02 + elim (lift_total W2 0 (i+1)) + /4 width=12 by cpcs_lift, lstas_ldef, ex2_intro/ + | elim (IH1 … HVl1 … HVW0 … HVX0 … HK12) -IH1 -HVl1 -HVW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02 + elim (lift_total W2 0 (i+1)) + /3 width=12 by cpcs_lift, lstas_lift, ex2_intro/ + ] +| #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #_ #HT1 + lapply (da_inv_bind … Hl1) -Hl1 #Hl1 + elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct + elim (cpr_inv_bind1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct + elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 + /4 width=5 by cpcs_bind2, lpr_cpr_conf, lstas_bind, ex2_intro/ + | #T3 #HT13 #HXT3 #H1 #H2 destruct + elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 + elim (lstas_inv_lift1 … HTU3 L2 … HXT3) -T3 + /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10 + lapply (da_inv_flat … Hl1) -Hl1 #Hl1 + elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct + elim (cpr_inv_appl1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2 + elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 + /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/ + | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 + lapply (da_inv_bind … Hl1) -Hl1 #Hl1 + elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct + elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct + lapply (cprs_div … HW10 … HW20) -W0 #HW12 + lapply (da_sta_conf … HVW1 … Hl0) (lift_mono … H1 … H2) -H1 -H2 // +| #G #K #k #l #Hkl #L #s #d #e #_ #U1 #H1 #U2 #H2 + >(lift_inv_sort1 … H1) -U1 + >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/ +| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, ldrop_inv_gen/ + ] +| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpx_bind, ldrop_skip/ +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpx_flat/ +| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct + elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpx_zeta, ldrop_skip/ +| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_eps/ +| #G #K #V1 #V2 #T #_ #IHV12 #L #s #d #e #HLK #U1 #H #U2 #HVU2 + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ct/ +| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct + elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpx_beta, ldrop_skip/ +| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct + elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpx_theta, ldrop_skip/ +] +qed. + +lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G). +#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2 +[ * #i #G #L #K #s #d #e #_ #T1 #H + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/ + ] +| #G #L #k #l #Hkl #K #s #d #e #_ #T1 #H + lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_st, lift_sort, ex2_intro/ +| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV + elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 + elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus plus_minus // (plus_minus_m_m (l2-l1) 1 ?) +[ /4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/ +| /2 width=1 by monotonic_le_minus_r/ +] +qed. + +lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i. + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 → + ∀W2. ⇧[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2. +#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 +[ /3 width=9 by cpx_cpxs, cpx_delta/ +| #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK + elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 → + T2 = #i ∨ + ∃∃I,K,V1,T1. ⇩[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 & + ⇧[0, i+1] T1 ≡ T2. +#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ +| * #I #K #V1 #T1 #HLK #HVT1 #HT1 + lapply (ldrop_fwd_drop2 … HLK) #H0LK + elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ +] +qed-. + +(* Relocation properties ****************************************************) + +lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G). +/3 width=10 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed. + +lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G). +/3 width=6 by l_deliftable_sn_LTC, cpx_inv_lift1/ +qed-. + +(* Properties on supclosure *************************************************) + +lemma fqu_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T +#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + +lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-. + +lemma fqup_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T +#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + +lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H +[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc new file mode 100644 index 000000000..8011dd753 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpb_lift.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cpx_lift.ma". +include "basic_2/reduction/fpb.ma". + +(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) + +(* Advanced properties ******************************************************) + +lemma ssta_fpb: ∀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⦄. +/3 width=5 by fpb_cpx, ssta_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc new file mode 100644 index 000000000..c67134ee3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbg_lift.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fpbu_lift.ma". +include "basic_2/computation/fpbg.ma". + +(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) + +(* 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⦄. +/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⦄. +/4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc new file mode 100644 index 000000000..ab8f6608d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbs_lift.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/fpb_lift.ma". +include "basic_2/computation/cpxs_lift.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Advanced properties ******************************************************) + +lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. + +lemma ssta_fpbs: ∀h,g,G,L,T,U,l. + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → + ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. +/4 width=2 by fpb_fpbs, ssta_fpb/ qed. + +(* Note: this is used in the closure proof *) +lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, ssta_cpx, fpb_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc new file mode 100644 index 000000000..d7b48650e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/fpbu_lift.etc @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/ssta_ssta.ma". +include "basic_2/computation/cpxs_lift.ma". +include "basic_2/computation/fpbu.ma". + +(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) + +(* Advanced properties ******************************************************) + +lemma lsstas_fpbu: ∀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⦄. +/4 width=5 by fpbu_cpxs, lsstas_cpxs/ qed. + +lemma ssta_fpbu: ∀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⦄. +#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) +/3 width=5 by ssta_lsstas, lsstas_fpbu/ #H destruct +elim (ssta_inv_refl_pos … HT1 … HT12) +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lsstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lsstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsstas_lsstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc new file mode 100644 index 000000000..a4d4cff8d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_cpds.etc @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/lsubsv_lsstas.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties on decomposed extended parallel computation on terms **********) + +lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 → + ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T. +#h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12 +lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2 +elim (lsubsv_lsstas_trans … HT1 … Hl1 … HL12) // #T0 #HT10 #HT0 +lapply (lsubsv_fwd_lsubd … HL12) -HL12 #HL12 +lapply (lsubd_da_trans … Hl1 … HL12) -L2 #Hl1 +lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02 +elim (cpcs_inv_cprs … HT02) -HT02 /3 width=7/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_lsstas.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_lsstas.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc new file mode 100644 index 000000000..e4596e7d4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/lsubsv_snv.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cpds_cpds.ma". +include "basic_2/dynamic/snv_aaa.ma". +include "basic_2/dynamic/lsubsv_cpds.ma". +include "basic_2/dynamic/lsubsv_cpcs.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties concerning stratified native validity *************************) + +lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → + ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g]. +#h #g #G #L2 #T #H elim H -G -L2 -T // +[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12 + elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubsv_inv_pair2 … H) -H * #K1 + [ #HK12 #H destruct /3 width=5 by snv_lref/ + | #W #l #H1V #H1W #HWV #_ #HWl #_ #_ #H1 #H2 destruct -IHV + /3 width=10 by snv_scast, snv_lref/ + ] +| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct + /4 width=1 by snv_bind, lsubsv_pair/ +| #a #G #L2 #V #W #W0 #T #U #l #_ #_ #HVl #HVW #HW0 #HTU #IHV #IHT #L1 #HL12 + lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 + elim (lsubsv_ssta_trans … HVW … HVl … HL12) -HVW #W1 #HVW1 #HW1 + lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10 + lapply (lsubd_da_trans … HVl L1 ?) -HVl /2 width=1 by lsubsv_fwd_lsubd/ #HVl + elim (lsubsv_cpds_trans … HTU … HL12) -HTU #X #HTU #H + elim (cprs_inv_abst1 … H) -H #W #U2 #HW0 #_ #H destruct + lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H + elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 + /4 width=11 by snv_appl, cpds_cprs_trans, cprs_bind/ +| #G #L2 #W #T #U #l #_ #_ #HTl #HTU #HUW #IHW #IHT #L1 #HL12 + lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW + elim (lsubsv_ssta_trans … HTU … HTl … HL12) -HTU #U0 #HTU0 #HU0 + lapply (lsubd_da_trans … HTl L1 ?) -HTl + /4 width=5 by lsubsv_fwd_lsubd, snv_cast, cpcs_trans/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc new file mode 100644 index 000000000..7bdef30fa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv.etc @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/nativevalid_5.ma". +include "basic_2/computation/cpds.ma". +include "basic_2/equivalence/cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +definition scast: ∀h. sd h → nat → relation4 genv lenv term term ≝ + λh,g,l,G,L,V,W. ∀V0,W0,l0. + l0 ≤ l → ⦃G, L⦄ ⊢ V •*[h, g, l0+1] V0 → ⦃G, L⦄ ⊢ W •*[h, g, l0] W0 → ⦃G, L⦄ ⊢ V0 ⬌* W0. + +(* activate genv *) +inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ +| snv_sort: ∀G,L,k. snv h g G L (⋆k) +| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) +| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T) +| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T → + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h, g] W → ⦃G, L⦄ ⊢ W ➡* W0 → + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T) +| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T → + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T) +. + +interpretation "stratified native validity (term)" + 'NativeValid h g G L T = (snv h g G L T). + +(* Basic inversion lemmas ***************************************************) + +fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i → + ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. +#h #g #G #L #X * -G -L -X +[ #G #L #k #i #H destruct +| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/ +| #a #I #G #L #V #T #_ #_ #i #H destruct +| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #i #H destruct +| #G #L #W #T #U #l #_ #_ #_ #_ #_ #i #H destruct +] +qed-. + +lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] → + ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. +/2 width=3 by snv_inv_lref_aux/ qed-. + +fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥. +#h #g #G #L #X * -G -L -X +[ #G #L #k #p #H destruct +| #I #G #L #K #V #i #_ #_ #p #H destruct +| #a #I #G #L #V #T #_ #_ #p #H destruct +| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #p #H destruct +| #G #L #W #T #U #l #_ #_ #_ #_ #_ #p #H destruct +] +qed-. + +lemma snv_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥. +/2 width=8 by snv_inv_gref_aux/ qed-. + +fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → + ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. +#h #g #G #L #X * -G -L -X +[ #G #L #k #a #I #V #T #H destruct +| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct +| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/ +| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct +| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct +] +qed-. + +lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → + ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. +/2 width=4 by snv_inv_bind_aux/ qed-. + +fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → + ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. +#h #g #G #L #X * -L -X +[ #G #L #k #V #T #H destruct +| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct +| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct +| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8 by ex6_5_intro/ +| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #V #T #H destruct +] +qed-. + +lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → + ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. +/2 width=3 by snv_inv_appl_aux/ qed-. + +fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → + ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. +#h #g #G #L #X * -G -L -X +[ #G #L #k #W #T #H destruct +| #I #G #L #K #V #i #_ #_ #W #T #H destruct +| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct +| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #_ #W #T #H destruct +| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4 by ex5_2_intro/ +] +qed-. + +lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] → + ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & + ⦃G, L⦄ ⊢ T ▪[h, g] l+1 & ⦃G, L⦄ ⊢ T •[h, g] U & ⦃G, L⦄ ⊢ U ⬌* W. +/2 width=3 by snv_inv_cast_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc new file mode 100644 index 000000000..20d72ef3e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_aaa.etc @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/csx_aaa.ma". +include "basic_2/computation/cpds_aaa.ma". +include "basic_2/equivalence/cpcs_aaa.ma". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Forward lemmas on atomic arity assignment for terms **********************) + +lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. +#h #g #G #L #T #H elim H -G -L -T +[ /2 width=2/ +| #I #G #L #K #V #i #HLK #_ * /3 width=6/ +| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ +| #a #G #L #V #W #W0 #T #U #l #_ #_ #Hl #HVW #HW0 #HTU * #B #HV * #X #HT + lapply (aaa_cpds_conf h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) + lapply (aaa_cpds_conf … HT … HTU) -HTU #H + elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct + lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ +| #G #L #W #T #U #l #_ #_ #_ #HTU #HUW * #B #HW * #A #HT + lapply (aaa_ssta_conf … HT … HTU) -HTU #H + lapply (aaa_cpcs_mono … HUW … H … HW) -HUW -H #H destruct /3 width=3/ +] +qed-. + +lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma snv_fwd_da: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_da/ +qed-. + +lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃U. ⦃G, L⦄ ⊢ T •[h, g] U. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fwd_ssta/ +qed-. + +lemma snv_lsstas_fwd_correct: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g, l] T2 → + ∃U2. ⦃G, L⦄ ⊢ T2 •[h, g] U2. +#h #g #G #L #T1 #T2 #l #HT1 #HT12 +elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by lsstas_fwd_correct/ +qed-. + +(* Advanced properties ******************************************************) + +lemma snv_scast: ∀h,g,G,L,V,W,l. ⦃G, L⦄ ⊢ V ¡[h, g] → ⦃G, L⦄ ⊢ W ¡[h, g] → + scast h g l G L V W → ⦃G, L⦄ ⊢V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ ⓝW.V ¡[h, g]. +#h #g #G #L #V #W #l #HV #HW #H #Hl +elim (snv_fwd_ssta … HV) /4 width=6 by snv_cast, ssta_lsstas/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc new file mode 100644 index 000000000..e73f809fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_cpcs.etc @@ -0,0 +1,169 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/lsstas_lsstas.ma". +include "basic_2/computation/fpbs_lift.ma". +include "basic_2/computation/fpbg_fleq.ma". +include "basic_2/equivalence/cpes_cpds.ma". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Inductive premises for the preservation results **************************) + +definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. + +definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λ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. + +definition IH_lsstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λ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 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. + +definition IH_snv_lsstas: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → + ∀U. ⦃G, L⦄ ⊢ T •*[h, g, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g]. + +(* 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] → + ∀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] → + ∀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 +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ +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] → + ∀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 +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] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → + ∀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. +#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 +elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12 +/3 width=3 by lsstas_inv_SO, ssta_lsstas, ex2_intro/ +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] → + ∀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 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=10 by/ ] +#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 +elim (IHT1 L1) // -IHT1 #U #HTU #HU1 +elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 +[2: /3 width=12 by da_cprs_lpr_aux/ +|3: /3 width=10 by snv_cprs_lpr_aux/ +|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ +] -G0 -L0 -T0 -T1 -T -l1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +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] → + ∀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] → + ∀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 +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 +elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 +lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ +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] → + ∀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] → + ∀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. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 +lapply (da_mono … H … Hl1) -H #H destruct +lapply (lsstas_da_conf … HTU1 … Hl1) #Hl12 +elim (le_or_ge l2 l) #Hl2 +[ lapply (lsstas_conf_le … HTU1 … HT1T) -HT1T + /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ +| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l + lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 + elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2 + /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l, ex3_2_intro/ +] +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] → + ∀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. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 +lapply (IH2 … H01 … Hl1 … HT12 … HL12) -L0 -T0 // -T1 +lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc new file mode 100644 index 000000000..dd56de7a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_da_lpr.etc @@ -0,0 +1,94 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lsubd_da.ma". +include "basic_2/computation/cpds_cpds.ma". +include "basic_2/dynamic/snv_aaa.ma". +include "basic_2/dynamic/snv_cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* 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 = 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 + lapply (da_inv_sort … H2) -H2 + lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/ +| #i #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0 + elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #l1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (cpr_inv_lref1 … H3) -H3 + [1,3: #H destruct + lapply (fqup_lref … G1 … HLK1) + elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + /4 width=10 by da_ldef, da_ldec, fqup_fpbg/ + |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0 + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (fqup_lref … G1 … HLK1) + elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct + lapply (ldrop_fwd_drop2 … HLK2) -V2 + /4 width=8 by da_lift, fqup_fpbg/ + ] +| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH2 + elim (snv_inv_bind … H1) -H1 #_ #HT1 + lapply (da_inv_bind … H2) -H2 + elim (cpr_inv_bind1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct + /4 width=9 by da_bind, fqup_fpbg, lpr_pair/ + | #T2 #HT12 #HT2 #H1 #H2 destruct + /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 + lapply (da_inv_flat … H2) -H2 #Hl + elim (cpr_inv_appl1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/ + | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW #HU1 + lapply (da_inv_bind … Hl) -Hl #Hl + elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3 + lapply (cprs_div … HW3 … HW10) -W3 #HWW1 + lapply (ssta_da_conf … HVW1 … Hl0) (lift_inv_sort1 … H) -X -K -d -e // +| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #d #e #HLK #X #H + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #L0 #W #HLK0 #HVW #H destruct + /3 width=9 by snv_lref/ + | lapply (ldrop_trans_ge … HLK … HK0 ?) -K + /3 width=9 by snv_lref, ldrop_inv_gen/ + ] +| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H + elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct + /4 width=5 by snv_bind, ldrop_skip/ +| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct + elim (lift_total V0 d e) #W0 #HVW0 + elim (lift_total V1 d e) #W1 #HVW1 + elim (lift_total T1 (d+1) e) #U1 #HTU1 + @(snv_appl … a … W0 … W1 … U1 l) + [1,2,3,4,5: /2 width=10 by cprs_lift, ssta_lift, da_lift/ ] + @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *) +| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct + elim (lift_total V d e) + /3 width=12 by snv_cast, cpcs_lift, ssta_lift, da_lift/ +] +qed. + +lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g]. +#h #g #G #L #U #H elim H -G -L -U +[ #G #L #k #K #s #d #e #_ #X #H + >(lift_inv_sort2 … H) -X -L -d -e // +| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #d #e #HLK #X #H + elim (lift_inv_lref2 … H) * #Hid #H destruct + [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H + elim (ldrop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K0 #V #HLK0 #HVW #H destruct + /3 width=12 by snv_lref/ + | lapply (ldrop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ + ] +| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H + elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct + /4 width=5 by snv_bind, ldrop_skip/ +| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct + lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl + elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0 + elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01 + elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU + elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct + lapply (lift_inj … HY … HVW1) -HY #H destruct + /3 width=8 by snv_appl/ +| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct + lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl + elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV + lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W + /3 width=8 by snv_cast/ +] +qed-. + +(* Advanced properties ******************************************************) + +lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I1 #G1 #L1 #V1 #H + elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 + lapply (ldrop_inv_O2 … H) -H #H destruct // +|2: * +|5,6: /3 width=8 by snv_inv_lift/ +] +[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // +|2,4: * #G1 #L1 #V1 #T1 #H + [1,3: elim (snv_inv_appl … H) -H // + |2,4: elim (snv_inv_cast … H) -H // + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc new file mode 100644 index 000000000..f73c20a5e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ssta1/snv_lpr.etc @@ -0,0 +1,132 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/snv_lift.ma". +include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/lsubsv_snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* 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 = 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 + >(cpr_inv_sort1 … H2) -X // +| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (fqup_lref … G1 … HLK1) #HKL + elim (cpr_inv_lref1 … H2) -H2 + [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/ + | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 + lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct + lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/ + ] +| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #HV1 #HT1 + elim (cpr_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/ + | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 + /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_drop/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1 + elim (cpr_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 + lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 + lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0 + elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 + elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H + elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct + lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10 + lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 + lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 + elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 + lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) + /2 width=7 by snv_appl, cprs_bind/ + | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 + elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 + lapply (cprs_div … HW10 … HW230) -W30 #HW120 + lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10 + lapply (ssta_da_conf … HVW1 … Hl0) (lift_inv_sort1 … H1) -X1 >(lift_inv_sort1 … H2) -X2 // -| #G #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 +| #G #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #s #d #e #HL21 #X #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (lift_trans_ge … HW1 … HWU2) -W // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=8/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=9 by sta_ldef/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W /2 width=1 by le_S/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=9 by sta_ldef, ldrop_inv_gen/ ] -| #G #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 +| #G #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #s #d #e #HL21 #X #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (lift_trans_ge … HW1 … HWU2) -W // (lift_inv_sort2 … H) -X /2 width=3/ -| #G #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H +[ #G #L2 #k #L1 #s #d #e #_ #X #H + >(lift_inv_sort2 … H) -X /2 width=3 by sta_sort, lift_sort, ex2_intro/ +| #G #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #s #d #e #HL21 #X #H elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HW12 #HVW1 - elim (lift_trans_le … HW12 … HW2) -W2 // >minus_plus minus_plus minus_minus_m_m /2 width=1/ /3 width=8/ - | minus_minus_m_m /3 width=8 by sta_ldef, le_S, ex2_intro/ ] -| #G #L2 #K2 #W2 #V2 #W #i #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H +| #G #L2 #K2 #W2 #V2 #W #i #HLK2 #HWV2 #HW2 #IHWV2 #L1 #s #d #e #HL21 #X #H elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ] [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 // #K1 #W1 #HLK1 #HK21 #HW12 elim (IHWV2 … HK21 … HW12) -K2 #V1 #_ #HWV1 - elim (lift_trans_le … HW12 … HW2) -W2 // >minus_plus minus_plus minus_minus_m_m /2 width=1/ /3 width=8/ - | minus_minus_m_m /3 width=8 by sta_ldec, le_S, ex2_intro/ ] -| #a #I #G #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H +| #a #I #G #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #s #d #e #HL21 #X #H elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/ -| #G #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H + elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /3 width=5 by sta_bind, ldrop_skip, lift_bind, ex2_intro/ +| #G #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #s #d #e #HL21 #X #H elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct - elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/ -| #G #L2 #W2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H + elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5 by sta_appl, lift_flat, ex2_intro/ +| #G #L2 #W2 #T2 #U2 #_ #IHTU2 #L1 #s #d #e #HL21 #X #H elim (lift_inv_flat2 … H) -H #W1 #T1 #_ #HT12 #H destruct - elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/ + elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3 by sta_cast, ex2_intro/ ] qed-. @@ -105,13 +101,13 @@ lemma sta_fwd_correct: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ∃T0. ⦃G, #h #G #L #T #U #H elim H -G -L -T -U [ /2 width=2/ | #G #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0 - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK - elim (lift_total V0 0 (i+1)) /3 width=10/ + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK + elim (lift_total V0 0 (i+1)) /3 width=11 by ex_intro, sta_lift/ | #G #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_ - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK - elim (lift_total V 0 (i+1)) /3 width=10/ -| #a #I #G #L #V #T #U #_ * /3 width=2/ -| #G #L #V #T #U #_ * #T0 #HUT0 /3 width=2/ -| #G #L #W #T #U #_ * /2 width=2/ + lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK + elim (lift_total V 0 (i+1)) /3 width=11 by ex_intro, sta_lift/ +| #a #I #G #L #V #T #U #_ * /3 width=2 by sta_bind, ex_intro/ +| #G #L #V #T #U #_ * #T0 #HUT0 /3 width=2 by sta_appl, ex_intro/ +| #G #L #W #T #U #_ * /2 width=2 by ex_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sta_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sta_llpx_sn.ma new file mode 100644 index 000000000..af4cfb8c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sta_llpx_sn.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/multiple/llpx_sn_ldrop.ma". +include "basic_2/static/sta.ma". + +(* STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ******************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma sta_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → + ∀h,G. s_r_confluent1 … (sta h G) (llpx_sn R 0). +#R #H1R #H2R #h #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ +| #G #Ls #Ks #V1s #W2s #V2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #G #Ls #Ks #V1s #W1s #V2s #i #HLKs #_ #HV12s #IHVW1s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HV12s) -HLKs -HLKd -HV12s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/static/sta_sta.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc rename to matita/matita/contribs/lambdadelta/basic_2/static/sta_sta.ma index 03d4c8d73..6f737b59f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sta_sta.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/ldrop_ldrop.ma". +include "basic_2/substitution/ldrop_ldrop.ma". include "basic_2/static/sta.ma". (* STATIC TYPE ASSIGNMENT ON TERMS ******************************************) @@ -34,10 +34,10 @@ theorem sta_mono: ∀h,G,L. singlevalued … (sta h G L). lapply (IHWV … HWV0) -IHWV -HWV0 #H destruct >(lift_mono … HWU1 … HV0U2) -W -U1 // | #a #I #G #L #V #T #U1 #_ #IHTU1 #X #H - elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ + elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1 by eq_f/ | #G #L #V #T #U1 #_ #IHTU1 #X #H - elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ + elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1 by eq_f/ | #G #L #W #T #U1 #_ #IHTU1 #U2 #H - lapply (sta_inv_cast1 … H) -H /2 width=1/ + lapply (sta_inv_cast1 … H) -H /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma new file mode 100644 index 000000000..feed03e3f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas.ma @@ -0,0 +1,133 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/statictypestar_6.ma". +include "basic_2/static/sta.ma". + +(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************) + +definition lstas: ∀h. genv → lenv → nat → relation term ≝ + λh,G,L. lstar … (sta h G L). + +interpretation "nat-iterated static type assignment (term)" + 'StaticTypeStar h G L l T U = (lstas h G L l T U). + +(* Basic eliminators ********************************************************) + +lemma lstas_ind_sn: ∀h,G,L,U2. ∀R:relation2 nat term. + R 0 U2 → ( + ∀l,T,U1. ⦃G, L⦄ ⊢ T •[h] U1 → ⦃G, L⦄ ⊢ U1 •* [h, l] U2 → + R l U1 → R (l+1) T + ) → + ∀l,T. ⦃G, L⦄ ⊢ T •*[h, l] U2 → R l T. +/3 width=5 by lstar_ind_l/ qed-. + +lemma lstas_ind_dx: ∀h,G,L,T. ∀R:relation2 nat term. + R 0 T → ( + ∀l,U1,U2. ⦃G, L⦄ ⊢ T •* [h, l] U1 → ⦃G, L⦄ ⊢ U1 •[h] U2 → + R l U1 → R (l+1) U2 + ) → + ∀l,U. ⦃G, L⦄ ⊢ T •*[h, l] U → R l U. +/3 width=5 by lstar_ind_r/ qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lstas_inv_O: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, 0] U → T = U. +/2 width=4 by lstar_inv_O/ qed-. + +lemma lstas_inv_SO: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, 1] U → ⦃G, L⦄ ⊢ T •[h] U. +/2 width=1 by lstar_inv_step/ qed-. + +lemma lstas_inv_step_sn: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l+1] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 •[h] T & ⦃G, L⦄ ⊢ T •*[h, l] T2. +/2 width=3 by lstar_inv_S/ qed-. + +lemma lstas_inv_step_dx: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l+1] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, l] T & ⦃G, L⦄ ⊢ T •[h] T2. +/2 width=3 by lstar_inv_S_dx/ qed-. + +lemma lstas_inv_sort1: ∀h,G,L,X,k,l. ⦃G, L⦄ ⊢ ⋆k •*[h, l] X → X = ⋆((next h)^l k). +#h #G #L #X #k #l #H @(lstas_ind_dx … H) -X -l // +#l #X #X0 #_ #H #IHX destruct +lapply (sta_inv_sort1 … H) -H #H destruct +>iter_SO // +qed-. + +lemma lstas_inv_gref1: ∀h,G,L,X,p,l. ⦃G, L⦄ ⊢ §p •*[h, l+1] X → ⊥. +#h #G #L #X #p #l #H elim (lstas_inv_step_sn … H) -H +#U #H #HUX elim (sta_inv_gref1 … H) +qed-. + +lemma lstas_inv_bind1: ∀h,a,I,G,L,V,T,X,l. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T •*[h, l] X → + ∃∃U. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, l] U & X = ⓑ{a,I}V.U. +#h #a #I #G #L #V #T #X #l #H @(lstas_ind_dx … H) -X -l /2 width=3 by ex2_intro/ +#l #X #X0 #_ #HX0 * #U #HTU #H destruct +elim (sta_inv_bind1 … HX0) -HX0 #U0 #HU0 #H destruct /3 width=3 by lstar_dx, ex2_intro/ +qed-. + +lemma lstas_inv_appl1: ∀h,G,L,V,T,X,l. ⦃G, L⦄ ⊢ ⓐV.T •*[h, l] X → + ∃∃U. ⦃G, L⦄ ⊢ T •*[h, l] U & X = ⓐV.U. +#h #G #L #V #T #X #l #H @(lstas_ind_dx … H) -X -l /2 width=3 by ex2_intro/ +#l #X #X0 #_ #HX0 * #U #HTU #H destruct +elim (sta_inv_appl1 … HX0) -HX0 #U0 #HU0 #H destruct /3 width=3 by lstar_dx, ex2_intro/ +qed-. + +lemma lstas_inv_cast1: ∀h,G,L,W,T,U,l. ⦃G, L⦄ ⊢ ⓝW.T •*[h, l+1] U → ⦃G, L⦄ ⊢ T •*[h, l+1] U. +#h #G #L #W #T #X #l #H elim (lstas_inv_step_sn … H) -H +#U #H #HUX lapply (sta_inv_cast1 … H) -H /2 width=3 by lstar_S/ +qed-. + +(* Basic properties *********************************************************) + +lemma lstas_refl: ∀h,G,L. reflexive … (lstas h G L 0). +// qed. + +lemma sta_lstas: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ T •*[h, 1] U. +/2 width=1 by lstar_step/ qed. + +lemma lstas_step_sn: ∀h,G,L,T1,U1,U2,l. ⦃G, L⦄ ⊢ T1 •[h] U1 → ⦃G, L⦄ ⊢ U1 •*[h, l] U2 → + ⦃G, L⦄ ⊢ T1 •*[h, l+1] U2. +/2 width=3 by lstar_S/ qed. + +lemma lstas_step_dx: ∀h,G,L,T1,T2,U2,l. ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T2 •[h] U2 → + ⦃G, L⦄ ⊢ T1 •*[h, l+1] U2. +/2 width=3 by lstar_dx/ qed. + +lemma lstas_split: ∀h,G,L. inv_ltransitive … (lstas h G L). +/2 width=1 by lstar_inv_ltransitive/ qed-. + +lemma lstas_sort: ∀h,G,L,l,k. ⦃G, L⦄ ⊢ ⋆k •*[h, l] ⋆((next h)^l k). +#h #G #L #l @(nat_ind_plus … l) -l // +#l #IHl #k >iter_SO /2 width=3 by sta_sort, lstas_step_dx/ +qed. + +lemma lstas_bind: ∀h,I,G,L,V,T,U,l. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, l] U → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T •*[h, l] ⓑ{a,I}V.U. +#h #I #G #L #V #T #U #l #H @(lstas_ind_dx … H) -U -l /3 width=3 by sta_bind, lstar_O, lstas_step_dx/ +qed. + +lemma lstas_appl: ∀h,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, l] U → + ∀V.⦃G, L⦄ ⊢ ⓐV.T •*[h, l] ⓐV.U. +#h #G #L #T #U #l #H @(lstas_ind_dx … H) -U -l /3 width=3 by sta_appl, lstar_O, lstas_step_dx/ +qed. + +lemma lstas_cast: ∀h,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, l+1] U → + ∀W. ⦃G, L⦄ ⊢ ⓝW.T •*[h, l+1] U. +#h #G #L #T #U #l #H elim (lstas_inv_step_sn … H) -H /3 width=3 by sta_cast, lstas_step_sn/ +qed. + +(* Basic_1: removed theorems 7: + sty1_abbr sty1_appl sty1_bind sty1_cast2 + sty1_correct sty1_lift sty1_trans +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma new file mode 100644 index 000000000..7497f44b6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_aaa.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/sta_aaa.ma". +include "basic_2/unfold/lstas.ma". + +(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************) + +(* Properties on atomic arity assignment for terms **************************) + +lemma lstas_aaa_conf: ∀h,G,L,l. Conf3 … (aaa G L) (lstas h G L l). +/3 width=6 by sta_aaa_conf, lstar_Conf3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma new file mode 100644 index 000000000..17e048a63 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/statictypestaralt_6.ma". +include "basic_2/unfold/lstas_lift.ma". + +(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************) + +(* alternative definition of lstas *) +inductive lstasa (h): genv → relation4 lenv nat term term ≝ +| lstasa_O : ∀G,L,T. lstasa h G L 0 T T +| lstasa_sort: ∀G,L,l,k. lstasa h G L l (⋆k) (⋆((next h)^l k)) +| lstasa_ldef: ∀G,L,K,V,W,U,i,l. ⇩[i] L ≡ K.ⓓV → lstasa h G K (l+1) V W → + ⇧[0, i+1] W ≡ U → lstasa h G L (l+1) (#i) U +| lstasa_ldec: ∀G,L,K,W,V,V0,U,i,l. ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W •[h] V0 → + lstasa h G K l W V → ⇧[0, i+1] V ≡ U → lstasa h G L (l+1) (#i) U +| lstasa_bind: ∀a,I,G,L,V,T,U,l. lstasa h G (L.ⓑ{I}V) l T U → + lstasa h G L l (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) +| lstasa_appl: ∀G,L,V,T,U,l. lstasa h G L l T U → lstasa h G L l (ⓐV.T) (ⓐV.U) +| lstasa_cast: ∀G,L,W,T,U,l. lstasa h G L (l+1) T U → lstasa h G L (l+1) (ⓝW.T) U +. + +interpretation "nat-iterated static type assignment (term) alternative" + 'StaticTypeStarAlt h G L l T U = (lstasa h G L l T U). + +(* Base properties **********************************************************) + +lemma sta_lstasa: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ T ••*[h, 1] U. +#h #G #L #T #U #H elim H -G -L -T -U +/2 width=8 by lstasa_O, lstasa_sort, lstasa_ldef, lstasa_ldec, lstasa_bind, lstasa_appl, lstasa_cast/ +qed. + +lemma lstasa_step_dx: ∀h,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, l] T → + ∀T2. ⦃G, L⦄ ⊢ T •[h] T2 → ⦃G, L⦄ ⊢ T1 ••*[h, l+1] T2. +#h #G #L #T1 #T #l #H elim H -G -L -T1 -T -l +[ /2 width=1 by sta_lstasa/ +| #G #L #l #k #X #H >(sta_inv_sort1 … H) -X >commutative_plus // +| #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2 + lapply (ldrop_fwd_drop2 … HLK) #H + elim (sta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6 by lstasa_ldef/ +| #G #L #K #W #V #V0 #U #i #l #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2 + lapply (ldrop_fwd_drop2 … HLK) #H + elim (sta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lstasa_ldec/ +| #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H + elim (sta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lstasa_bind/ +| #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H + elim (sta_inv_appl1 … H) -H #U #HU1 #H destruct /3 width=1 by lstasa_appl/ +| /3 width=1 by lstasa_cast/ +] +qed. + +(* Main properties **********************************************************) + +theorem lstas_lstasa: ∀h,G,L,T,U,l. ⦃G, L⦄ ⊢ T •*[h, l] U → ⦃G, L⦄ ⊢ T ••*[h, l] U. +#h #G #L #T #U #l #H @(lstas_ind_dx … H) -U -l /2 width=3 by lstasa_step_dx, lstasa_O/ +qed. + +(* Main inversion lemmas ****************************************************) + +theorem lstasa_inv_lstas: ∀h,G,L,T,U,l. ⦃G, L⦄ ⊢ T ••*[h, l] U → ⦃G, L⦄ ⊢ T •*[h, l] U. +#h #G #L #T #U #l #H elim H -G -L -T -U -l +/2 width=8 by lstas_inv_SO, lstas_ldec, lstas_ldef, lstas_cast, lstas_appl, lstas_bind/ +qed-. + +(* Advanced eliminators *****************************************************) + +lemma lstas_ind_alt: ∀h. ∀R:genv→relation4 lenv nat term term. + (∀G,L,T. R G L O T T) → + (∀G,L,l,k. R G L l (⋆k) (⋆((next h)^l k))) → ( + ∀G,L,K,V,W,U,i,l. + ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V •*[h, l+1] W → ⇧[O, i+1] W ≡ U → + R G K (l+1) V W → R G L (l+1) (#i) U + ) → ( + ∀G,L,K,W,V,V0,U,i,l. + ⇩[i] L ≡ K.ⓛW → ⦃G, K⦄ ⊢ W •[h] V0 → + ⦃G, K⦄ ⊢ W •*[h, l]V → ⇧[O, i+1] V ≡ U → + R G K l W V → R G L (l+1) (#i) U + ) → ( + ∀a,I,G,L,V,T,U,l. ⦃G, L.ⓑ{I}V⦄ ⊢ T •*[h, l] U → + R G (L.ⓑ{I}V) l T U → R G L l (ⓑ{a,I}V.T) (ⓑ{a,I}V.U) + ) → ( + ∀G,L,V,T,U,l. ⦃G, L⦄ ⊢ T •*[h, l] U → + R G L l T U → R G L l (ⓐV.T) (ⓐV.U) + ) → ( + ∀G,L,W,T,U,l. ⦃G, L⦄⊢ T •*[h, l+1] U → + R G L (l+1) T U → R G L (l+1) (ⓝW.T) U + ) → + ∀G,L,l,T,U. ⦃G, L⦄ ⊢ T •*[h, l] U → R G L l T U. +#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #G #L #l #T #U #H +elim (lstas_lstasa … H) /3 width=10 by lstasa_inv_lstas/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma new file mode 100644 index 000000000..c1726ff5d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/lstas.ma". +include "basic_2/static/da_sta.ma". + +(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************) + +(* Properties on degree assignment for terms ********************************) + +lemma lstas_da_conf: ∀h,g,G,L,T,U,l1. ⦃G, L⦄ ⊢ T •*[h, l1] U → + ∀l2. ⦃G, L⦄ ⊢ T ▪[h, g] l2 → ⦃G, L⦄ ⊢ U ▪[h, g] l2-l1. +#h #g #G #L #T #U #l1 #H @(lstas_ind_dx … H) -U -l1 // +#l1 #U #U0 #_ #HU0 #IHTU #l2 #HT +(plus_minus_m_m … Hl12) in ⊢ (%→?); -Hl12 >commutative_plus #H +elim (lstas_split … H) -H #U #HTU +>(lstas_mono … HTU … HTU1) -T // +qed-. + +(* Advanced properties ******************************************************) + +lemma lstas_sta_conf_pos: ∀h,G,L,T,U1. ⦃G, L⦄ ⊢ T •[h] U1 → + ∀U2,l. ⦃G, L⦄ ⊢ T •*[h, l+1] U2 → ⦃G, L⦄ ⊢ U1 •*[h, l] U2. +#h #G #L #T #U1 #HTU1 #U2 #l #HTU2 +lapply (lstas_conf_le … T U1 1 … HTU2) -HTU2 /2 width=1 by sta_lstas/ +qed-. + +lemma lstas_strip_pos: ∀h,G,L,T1,U1. ⦃G, L⦄ ⊢ T1 •[h] U1 → + ∀T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l+1] T2 → + ∃∃U2. ⦃G, L⦄ ⊢ T2 •[h] U2 & ⦃G, L⦄ ⊢ U1 •*[h, l+1] U2. +#h #G #L #T1 #U1 #HTU1 #T2 #l #HT12 +elim (lstas_fwd_correct … HTU1 … HT12) +lapply (lstas_sta_conf_pos … HTU1 … HT12) -T1 /3 width=5 by lstas_step_dx, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index db46ed578..4778311f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -40,11 +40,11 @@ table { ] *) [ { "local env. ref. for stratified native validity" * } { - [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_ldrop" + "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lsstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] + [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] } ] [ { "stratified native validity" * } { - [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_da_lpr" + "snv_aaa" + "snv_lsstas" + "snv_lsstas_lpr" + "snv_lpr" + "snv_cpcs" + "snv_preserve" * ] + [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpcs" + "snv_preserve" * ] } ] } @@ -170,35 +170,35 @@ table { } ] [ { "iterated static type assignment" * } { - [ "lsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )" "lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )" "lsstas_lift" + "lsstas_aaa" + "lsstas_lsstas" * ] + [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )" "lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )" "lstas_lift" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ] } ] } ] class "grass" [ { "static typing" * } { - [ { "local env. ref. for atomic arity assignment" * } { - [ "lsuba ( ? ⊢ ? ⁝⫃ ? )" "lsuba_ldrop" + "lsuba_aaa" + "lsuba_lsuba" * ] + [ { "local env. ref. for degree assignment" * } { + [ "lsubd ( ? ⊢ ? ▪⫃ ? )" "lsubd_da" + "lsubd_lsubd" * ] } ] - [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ] + [ { "degree assignment" * } { + [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_sta" + "da_da" * ] } ] [ { "stratified static type assignment" * } { - [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_lpx_sn" + "ssta_ssta" * ] + [ "sta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "sta_lift" + "sta_lpx_sn" + "sta_aaa" + "sta_sta" * ] } ] - [ { "local env. ref. for degree assignment" * } { - [ "lsubd ( ? ⊢ ? ▪⫃ ? )" "lsubd_da" + "lsubd_lsubd" * ] + [ { "parameters" * } { + [ "sh" "sd" * ] } ] - [ { "degree assignment" * } { - [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_da" * ] + [ { "local env. ref. for atomic arity assignment" * } { + [ "lsuba ( ? ⊢ ? ⁝⫃ ? )" "lsuba_aaa" + "lsuba_lsuba" * ] } ] - [ { "parameters" * } { - [ "sh" "sd" * ] + [ { "atomic arity assignment" * } { + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_aaa" * ] } ] [ { "restricted local env. ref." * } { -- 2.39.2