From: Ferruccio Guidi Date: Fri, 21 Sep 2018 10:37:30 +0000 (+0200) Subject: milestone in basic_2, λδ-2A reconstructed X-Git-Tag: make_still_working~278 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9b09b14538f770b9e65083c24e3e9cf487df648;p=helm.git milestone in basic_2, λδ-2A reconstructed + confluence of rt-computation (not proved in λδ-2A) + preservation of validity for rt-computation --- diff --git a/.gitignore b/.gitignore index 928986366..59fdc3df1 100644 --- a/.gitignore +++ b/.gitignore @@ -72,6 +72,6 @@ helm/www/lambdadelta/xslt/xhtbl.xsl matita/matita/contribs/lambdadelta/.depend matita/matita/contribs/lambdadelta/nodes matita/matita/contribs/lambdadelta/token -matita/matita/contribs/lambdadelta/2A1 +matita/matita/contribs/lambdadelta/2A matita/matita/contribs/lambdadelta/*/*_probe.txt matita/matita/contribs/lambdadelta/*/web/*_sum.tbl diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index bde05a33c..92b22a46a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -151,7 +151,6 @@ lemma cnv_fwd_flat (a) (h) (I) (G) (L): ] -H /2 width=1 by conj/ qed-. -(* Basic_2A1: removed theorems 6: - snv_fwd_da snv_fwd_lstas snv_cast_scpes +(* Basic_2A1: removed theorems 3: shnv_cast shnv_inv_cast snv_shnv_cast *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma index 729159536..fcb2cb319 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma @@ -12,74 +12,29 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/cnv_cpm_tdeq_conf.ma". -include "basic_2/dynamic/cnv_cpms_tdeq.ma". -(* -include "basic_2/dynamic/cnv_cpm_trans.ma". include "basic_2/dynamic/cnv_cpm_conf.ma". -*) +include "basic_2/dynamic/cnv_cpms_tdeq_conf.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Sub confluence propery with t-bound rt-computation for terms *************) -fact cnv_cpms_tdeq_strip_lpr_aux (a) (h) (o) (G0) (L0) (T0): +fact cnv_cpms_conf_lpr_tdeq_tdeq_aux (a) (h) (o) (G0) (L0) (T0): (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 → - ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 → - ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T. -#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 -@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 -[ #H0T1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 - arith_l3 - /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/ -] -qed-. - -fact cnv_cpms_tdeq_conf_lpr_aux (a) (h) (o) (G0) (L0) (T0): - (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → - (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → - ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 → + ⦃G0,L0⦄ ⊢ T0 ![a,h] → + ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛[h,o] T1 → ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T. -#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 -generalize in match IH1; generalize in match IH2; -@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 -[ #H0T1 #IH2 #IH1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 - arith_l3 - /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/ -] + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T. +#a #h #o #G #L0 #T0 #IH2 #IH1 #HT0 +#n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02 +#L1 #HL01 #L2 #HL02 +elim (cnv_cpms_tdeq_conf_lpr_aux … IH2 IH1 … H1T01 … H1T02 … HL01 … HL02) -IH2 -IH1 -H1T01 -H1T02 -HL01 -HL02 +/2 width=3 by ex2_intro/ qed-. -(* -fact cnv_cpms_conf_lpr_refl_refl_aux (h) (G0) (L1) (L2) (T0:term): - ∃∃T. ⦃G0,L1⦄ ⊢ T0 ➡*[h] T & ⦃G0,L2⦄ ⊢ T0 ➡*[h] T. -/2 width=3 by ex2_intro/ qed-. - -fact cnv_cpms_conf_lpr_refl_step_aux (a) (h) (o) (G0) (L0) (T0) (m21) (m22): +fact cnv_cpms_conf_lpr_refl_tdneq_sub (a) (h) (o) (G0) (L0) (T0) (m21) (m22): (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → ⦃G0,L0⦄ ⊢ T0 ![a,h] → @@ -101,14 +56,79 @@ lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y /2 width=3 by ex2_intro/ qed-. -fact cnv_cpms_conf_lpr_step_step_aux (a) (h) (o) (G0) (L0) (T0) (m11) (m12) (m21) (m22): +fact cnv_cpms_conf_lpr_step_tdneq_sub (a) (h) (o) (G0) (L0) (T0) (m11) (m12) (m21) (m22): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ⦃G0,L0⦄ ⊢ T0 ![a,h] → + ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → T0 ≛[h,o] X1 → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 → X1 ≛[h,o] T1 → + ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛[h,o] X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ((∀G,L,T. ⦃G0,L0,X1⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,X1⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ∀m21,m22. + ∀X2. ⦃G0,L0⦄ ⊢ X1 ➡[m21,h] X2 → (X1 ≛[h,o] X2 → ⊥) → + ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-m12,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m12-(m21+m22),h]T + ) → + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. +#a #h #o #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #HT0 +#X1 #H1X01 #H2X01 #T1 #H1XT1 #H2XT1 #X2 #H1X02 #H2X02 #T2 #HXT2 +#L1 #HL01 #L2 #HL02 #IH +lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1 +lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X02 … L0 ?) // #HX2 +elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … H1X01 … H1X02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 +cut (⦃G0,L0,T0⦄ >[h,o] ⦃G0,L0,X2⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) +lapply (fpbg_fpbs_trans ??? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg +lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0 +elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 +elim (tdeq_dec h o X1 Z0) #H2XZ +[ -IH + elim (cnv_cpms_conf_lpr_tdeq_tdeq_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] +| -H1XT1 -H2XT1 + elim (cpms_tdneq_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] + -HXZ10 -H2XZ #n1 #n2 #X0 #H1X10 #H2X10 #HXZ0 #Hn + elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] + >Hn -n1 -n2 -X0 -IH +] +#Z1 #HTZ1 #HZ01 +elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02 +lapply (cpms_trans … HTZ1 … HZ01) -Z1 [h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ⦃G0,L0⦄ ⊢ T0 ![a,h] → + ∀T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → T0 ≛[h,o] T1 → + ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛[h,o] X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-n1,h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-(m21+m22),h] T. +#a #h #o #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0 +#T1 #H1T01 #H2T01 +generalize in match m22; generalize in match m21; -m21 -m22 +generalize in match IH1; generalize in match IH2; +@(cpms_tdeq_ind_sn … H1T01 HT0 H2T01 IH1 IH2) -n1 -T0 +[ #HT1 #IH2 #IH1 #m21 #m22 + #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 + [h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → ⦃G0,L0⦄ ⊢ T0 ![a,h] → ∀X1. ⦃G0,L0⦄ ⊢ T0 ➡[m11,h] X1 → (T0 ≛[h,o] X1 → ⊥) → ∀T1. ⦃G0,L0⦄ ⊢ X1 ➡*[m12,h] T1 → ∀X2. ⦃G0,L0⦄ ⊢ T0 ➡[m21,h] X2 → (T0 ≛[h,o] X2 → ⊥) → ∀T2. ⦃G0,L0⦄ ⊢ X2 ➡*[m22,h] T2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ⦃G0,L2⦄ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. #a #h #o #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0 #X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 @@ -126,27 +146,24 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 [h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_conf_lpr a h G1 L1 T1. -#a #h #o #G #L #T #H0 #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT +fact cnv_cpms_conf_lpr_aux (a) (h) (o) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr a h G L T. +#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct -elim (cpms_fwd_tdpos_sn … HT0 H0 … HT01) * -elim (cpms_fwd_tdpos_sn … HT0 H0 … HT02) * --H0 -HT01 -HT02 -[ #H21 #H22 #H11 #H12 destruct -a -o -L0 - [h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → ∃∃n1,n2,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T0 & T1 ≛[h,o] T0 → ⊥ & ⦃G, L⦄ ⊢ T0 ➡*[n2,h] T2 & n1+n2 = n. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma new file mode 100644 index 000000000..56b7c440d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq_conf.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cnv_cpm_tdeq_conf.ma". +include "basic_2/dynamic/cnv_cpms_tdeq.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Sub confluence propery with restricted rt-transition for terms ***********) + +fact cnv_cpms_tdeq_strip_lpr_aux (a) (h) (o) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T. +#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 +@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 +[ #H0T1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 + arith_l3 + /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/ +] +qed-. + +fact cnv_cpms_tdeq_conf_lpr_aux (a) (h) (o) (G0) (L0) (T0): + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + (∀G,L,T. ⦃G0,L0,T0⦄ >[h,o] ⦃G,L,T⦄ → IH_cnv_cpms_conf_lpr a h G L T) → + ∀n1,T1. ⦃G0,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ⦃G0,L0⦄ ⊢ T0 ![a,h] → T0 ≛[h,o] T1 → + ∀n2,T2. ⦃G0,L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 → + ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G0,L2⦄ ⊢ T2 ➡*[n1-n2,h] T & T2 ≛[h,o] T. +#a #h #o #G #L0 #T0 #IH2 #IH1 #n1 #T1 #H1T01 #H0T0 #H2T01 +generalize in match IH1; generalize in match IH2; +@(cpms_tdeq_ind_sn … H1T01 H0T0 H2T01 IH1 IH2) -n1 -T0 +[ #H0T1 #IH2 #IH1 #n2 #T2 #H1T12 #H2T12 #L1 #HL01 #L2 #HL02 + arith_l3 + /3 width=7 by cpms_step_sn, tdeq_trans, ex4_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma index 9e372bb3e..4ea01e534 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -17,88 +17,33 @@ include "basic_2/dynamic/cnv_cpms_conf.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Main preservation properties *********************************************) -(* + (* Basic_2A1: uses: snv_preserve *) lemma cnv_preserve (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ∧∧ IH_cnv_cpms_conf_lpr a h G L T & IH_cnv_cpm_trans_lpr a h G L T. #a #h #G #L #T #HT -elim (tdpos_total h … T) #o +letin o ≝ (sd_O h) lapply (cnv_fwd_fsb … o … HT) -HT #H -@(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH #Ho +@(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH @conj [ letin aux ≝ cnv_cpms_conf_lpr_aux | letin aux ≝ cnv_cpm_trans_lpr_aux ] @(aux … o … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H // - - -lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → - ∧∧ IH_da_cpr_lpr h o G L T - & IH_snv_cpr_lpr h o G L T - & IH_snv_lstas h o G L T - & IH_lstas_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT -#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A -#G #L #T #A #_ #IH -A @and4_intro -[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux -| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux -] -@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H // -qed-. - -theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/ -qed-. - -theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/ qed-. -theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/ +theorem cnv_cpms_conf_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_conf_lpr a h G L T. +#a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=1 by/ qed-. -theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/ +(* Basic_2A1: uses: snv_cpr_lpr *) +theorem cnv_cpm_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpm_trans_lpr a h G L T. +#a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=2 by/ qed-. (* Advanced preservation properties *****************************************) -lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G #L1 #T1 #HT1 #T2 #H -@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ -qed-. - -lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. -#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H -@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ -qed-. - -lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2 -[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] → - ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 -elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 -lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/ +(* Basic_2A1: uses: snv_cprs_lpr *) +lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T. +#a #h #G #L1 #T1 #HT1 #n #T2 #H +@(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/ qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_aaa.etc new file mode 100644 index 000000000..32f99168e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_aaa.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/static/da_aaa.ma". +include "basic_2/computation/scpds_aaa.ma". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Advanced forward lemmas **************************************************) + +lemma snv_fwd_da: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃d. ⦃G, L⦄ ⊢ T ▪[h, o] d. +#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_da/ +qed-. + +lemma snv_fwd_lstas: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → + ∀d. ∃U. ⦃G, L⦄ ⊢ T •*[h, d] U. +#h #o #G #L #T #H #d elim (snv_fwd_aaa … H) -H +#A #HT elim (aaa_lstas h … HT d) -HT /2 width=2 by ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_da_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_da_lpr.etc new file mode 100644 index 000000000..acaf6f038 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_da_lpr.etc @@ -0,0 +1,92 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/snv_aaa.ma". +include "basic_2/dynamic/snv_scpes.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on degree assignment for terms ********************************) + +fact da_cpr_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1. +#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] +[ #s #_ #_ #_ #_ #d #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 #d #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 #d1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct + lapply (drop_mono … H … HLK1) -H #H destruct + elim (cpr_inv_lref1 … H3) -H3 + [1,3: #H destruct + lapply (fqup_lref … G1 … HLK1) + elim (lpr_drop_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 (drop_mono … H … HLK1) -H #H destruct + lapply (fqup_lref … G1 … HLK1) + elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct + lapply (drop_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 #d #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, drop_drop/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #b1 #W1 #U1 #d1 #HV1 #HT1 #HVW1 #HTU1 + lapply (da_inv_flat … H2) -H2 #Hd + 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 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW #HU + lapply (da_inv_bind … Hd) -Hd #Hd + elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -d1 + elim (snv_fwd_da … HV1) #d1 #Hd1 + elim (snv_fwd_da … HW) #d0 #Hd0 + lapply (cprs_scpds_div … HW3 … Hd0 … 1 HVW1) -W3 #H + elim (da_scpes_aux … IH3 IH2 IH1 … Hd0 … Hd1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1 + (plus_minus_k_k d1 1) in Hd1; // -H1 #Hd1 + lapply (IH1 … HV1 … Hd1 … HV12 … HL12) -HV1 -Hd1 -HV12 [ /2 by fqup_fpbg/ ] + lapply (IH1 … Hd0 … HW2 … HL12) -Hd0 /2 width=1 by fqup_fpbg/ -HW + lapply (IH1 … HU … Hd … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hd -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2 + /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/ + | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -d1 -HV1 + elim (snv_inv_bind … HT1) -HT1 #_ + lapply (da_inv_bind … Hd) -Hd + /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/ + ] +| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 + elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1 + lapply (da_inv_flat … H2) -H2 #Hd + elim (cpr_inv_cast1 … H3) -H3 + [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/ + | /3 width=7 by fqup_fpbg/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve.etc new file mode 100644 index 000000000..8a7b78ef2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve.etc @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fsb_aaa.ma". +include "basic_2/dynamic/snv_da_lpr.ma". +include "basic_2/dynamic/snv_lstas.ma". +include "basic_2/dynamic/snv_lstas_lpr.ma". +include "basic_2/dynamic/snv_lpr.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Main preservation properties *********************************************) + +theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T. +#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/ +qed-. + +theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T. +#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/ +qed-. + +theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T. +#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/ +qed-. + +(* Advanced preservation properties *****************************************) + +lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. +#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H +@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ +qed-. + +lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] +#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 +elim (IHT1 L1) // -IHT1 #U #HTU #HU1 +elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2 +[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +qed-. + +lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] → + ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 → + ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12 +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 +elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 +lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_scpes.etc new file mode 100644 index 000000000..61d7fbdea --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_scpes.etc @@ -0,0 +1,198 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbg_fpbs.ma". +include "basic_2/equivalence/scpes_cpcs.ma". +include "basic_2/equivalence/scpes_scpes.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,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. + +definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. + +definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. + +definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → + ∀d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → + ∀U. ⦃G, L⦄ ⊢ T •*[h, d2] U → ⦃G, L⦄ ⊢ U ¡[h, o]. + +(* Properties for the preservation results **********************************) + +fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. +#h #o #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,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. +#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ +qed-. + +fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → + ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2. +#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d1 #Hd1 #T2 #d2 * #T #d0 #Hd20 #H #HT1 #HT2 #L2 #HL12 +lapply (da_mono … H … Hd1) -H #H destruct +lapply (lstas_da_conf … HT1 … Hd1) #Hd12 +lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12 +/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/ +qed-. + +fact da_scpes_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → + ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → + ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → + ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22. +#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #d11 #Hd11 #d12 #Hd12 #d21 #d22 * #T #HT1 #HT2 +elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd11 … HT1 … L) -Hd11 -HT1 // +elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 // +/3 width=7 by da_mono, and3_intro/ +qed-. + +fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #d1 #d2 #Hd21 #Hd1 #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 … Hd21 … 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 -d1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +qed-. + +fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. +#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #d2 * #W1 #d1 #Hd21 #HTd1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 +lapply (IH2 … H01 … HTd1 … 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=6 by ex4_2_intro, ex2_intro/ +qed-. + +fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] → + ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2. +#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #d1 #d2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12 +elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 +elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 +elim (cprs_conf … H1 … H2) -T0 +/3 width=5 by scpds_div, scpds_cprs_trans/ +qed-. + +fact lstas_scpds_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] → + ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 → + ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2. +#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2 +lapply (da_mono … H … HTd) -H #H destruct +lapply (lstas_da_conf … HT1 … HTd) #HTd1 +lapply (lstas_da_conf … HTX … HTd) #HXd +lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?) +[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2 +elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12) +[ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd + /5 width=6 by lstas_scpds, scpds_div, cprs_strap1, lstas_cpr, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro/ +| elim (da_lstas … HTd1 0) #X1 #HTX1 #_ + lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1 + elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXd … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXd -HXT1 -HXT2 + /4 width=8 by cpcs_scpes, cpcs_cpr_conf, fpbg_fpbs_trans, lstas_fpbs, lstas_cpr, monotonic_le_minus_l/ +] +qed-. + +fact scpes_le_aux: ∀h,o,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → + ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → + ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2. +#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20 +elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_ +elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_ +lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10 +[1,2,3: // | >eq_minus_O [2: // ] eq_minus_O [2: // ] ≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1. -#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #s #_ #_ #_ #_ #d #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 #d #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 #d1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct - lapply (drop_mono … H … HLK1) -H #H destruct - elim (cpr_inv_lref1 … H3) -H3 - [1,3: #H destruct - lapply (fqup_lref … G1 … HLK1) - elim (lpr_drop_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 (drop_mono … H … HLK1) -H #H destruct - lapply (fqup_lref … G1 … HLK1) - elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct - lapply (drop_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 #d #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, drop_drop/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #b1 #W1 #U1 #d1 #HV1 #HT1 #HVW1 #HTU1 - lapply (da_inv_flat … H2) -H2 #Hd - 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 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW #HU - lapply (da_inv_bind … Hd) -Hd #Hd - elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -d1 - elim (snv_fwd_da … HV1) #d1 #Hd1 - elim (snv_fwd_da … HW) #d0 #Hd0 - lapply (cprs_scpds_div … HW3 … Hd0 … 1 HVW1) -W3 #H - elim (da_scpes_aux … IH3 IH2 IH1 … Hd0 … Hd1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1 - (plus_minus_k_k d1 1) in Hd1; // -H1 #Hd1 - lapply (IH1 … HV1 … Hd1 … HV12 … HL12) -HV1 -Hd1 -HV12 [ /2 by fqup_fpbg/ ] - lapply (IH1 … Hd0 … HW2 … HL12) -Hd0 /2 width=1 by fqup_fpbg/ -HW - lapply (IH1 … HU … Hd … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hd -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2 - /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/ - | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -d1 -HV1 - elim (snv_inv_bind … HT1) -HT1 #_ - lapply (da_inv_bind … Hd) -Hd - /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/ - ] -| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 - elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1 - lapply (da_inv_flat … H2) -H2 #Hd - elim (cpr_inv_cast1 … H3) -H3 - [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/ - | /3 width=7 by fqup_fpbg/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_fsb.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_fsb.etc deleted file mode 100644 index ddffd5e9d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_fsb.etc +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fsb_aaa.ma". -include "basic_2/dynamic/snv_aaa.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* forward lemmas on "qrst" strongly normalizing closures *********************) - -lemma snv_fwd_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ⦥[h, o] ⦃G, L, T⦄. -#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lift.etc deleted file mode 100644 index 702ca5ab9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lift.etc +++ /dev/null @@ -1,117 +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/multiple/fqus_alt.ma". -include "basic_2/computation/scpds_lift.ma". -include "basic_2/dynamic/snv.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Relocation properties ****************************************************) - -lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≘ K → - ∀U. ⬆[l, k] T ≘ U → ⦃G, L⦄ ⊢ U ¡[h, o]. -#h #o #G #K #T #H elim H -G -K -T -[ #G #K #s #L #b #l #k #_ #X #H - >(lift_inv_sort1 … H) -X -K -l -k // -| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #b #l #k #HLK #X #H - elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by ylt_fwd_le/ #X #HL0 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #L0 #W #HLK0 #HVW #H destruct - /3 width=9 by snv_lref/ - | lapply (drop_trans_ge … HLK … HK0 ?) -K - /3 width=9 by snv_lref, drop_inv_gen/ - ] -| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct - /4 width=5 by snv_bind, drop_skip/ -| #a #G #K #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total W0 l k) - elim (lift_total U0 (l+1) k) - /4 width=17 by snv_appl, scpds_lift, lift_bind/ -| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total U0 l k) - /3 width=12 by snv_cast, scpds_lift/ -] -qed. - -lemma snv_inv_lift: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T. ⬆[l, k] T ≘ U → ⦃G, K⦄ ⊢ T ¡[h, o]. -#h #o #G #L #U #H elim H -G -L -U -[ #G #L #s #K #b #l #k #_ #X #H - >(lift_inv_sort2 … H) -X -L -l -k // -| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #b #l #k #HLK #X #H - elim (lift_inv_lref2 … H) * #Hil #H destruct - [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H - elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct - /3 width=12 by snv_lref/ - | lapply (drop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ - ] -| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct - /4 width=5 by snv_bind, drop_skip/ -| #a #G #L #W #W1 #U #U1 #d #_ #_ #HW1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0 - elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0 - elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct - lapply (lift_inj … HY … HW01) -HY #H destruct - /3 width=6 by snv_appl/ -| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - elim (scpds_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0 - elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 - lapply (lift_inj … HX … HU01) -HX #H destruct - /3 width=5 by snv_cast/ -] -qed-. - -(* Properties on subclosure *************************************************) - -lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #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 (drop_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-. - -lemma snv_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*] -/2 width=5 by snv_fqu_conf/ -qed-. - -lemma snv_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/3 width=5 by fqup_strap1, snv_fqu_conf/ -qed-. - -lemma snv_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*] -/2 width=5 by snv_fqup_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpr.etc deleted file mode 100644 index 101a50306..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpr.etc +++ /dev/null @@ -1,119 +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/snv_lift.ma". -include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_scpes.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,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h o G1 L1 T1. -#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #s #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_drop_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 (drop_mono … H … HLK1) -HLK1 -H #H destruct - lapply (drop_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, drop_drop/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #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 - elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV - elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H - elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1 - elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW - lapply (scpds_cprs_trans … HVW2 … HXV) -XV - lapply (scpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?) - /2 width=7 by snv_appl, cprs_bind/ - | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10 - elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -d0 - elim (snv_fwd_da … HV1) #d #HV1d - elim (snv_fwd_da … HW10) #d0 #HW10d - lapply (cprs_scpds_div … HW130 … HW10d … 1 HVW1) -W30 #HVW10 - elim (da_scpes_aux … IH4 IH1 IH2 … HW10d … HV1d … HVW10) /2 width=1 by fqup_fpbg/ - #_ #Hd (plus_minus_k_k d 1) in HV1d; // -Hd #HV1d - lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20 - lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1d #HV2d - lapply (IH2 … HW10d … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10d #HW20d - lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 - lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20 - lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20 - @snv_bind /2 width=1 by snv_cast_scpes/ - @(lsubsv_snv_trans … HT20) -HT20 - @(lsubsv_beta … (d-1)) // - @shnv_cast [1,2: // ] #d0 #Hd0 - lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20d … HV2d … d0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20 - /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ - | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4 - elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0 - elim (scpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct - elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct - elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1 - elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H - elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3 - lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2 - lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0 - lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2 - lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2 - elim (lift_total XV 0 1) #XW #HXVW - lapply (scpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2 - lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3 - elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3 - lapply (scpds_cprs_trans … HXWV2 … HXW3) -XW - lapply (scpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W - /3 width=6 by snv_appl, snv_bind/ - ] -| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 - elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1 - elim (cpr_inv_cast1 … H2) -H2 - [ * #W2 #T2 #HW12 #HT12 #H destruct - elim (snv_fwd_da … HW1) #d #HW1d - lapply (scpds_div … HWU1 … HTU1) -U1 -d #HWT1 - lapply (scpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/ - lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ - lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1 - /2 width=1 by snv_cast_scpes/ - | #H -IH3 -IH2 -HW1 -U1 - lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas.etc deleted file mode 100644 index 47c9cae13..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas.etc +++ /dev/null @@ -1,58 +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/snv_lift.ma". -include "basic_2/dynamic/snv_scpes.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on nat-iterated stratified static type assignment for terms ***) - -fact snv_lstas_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas h o G1 L1 T1. -#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #s #HG0 #HL0 #HT0 #_ #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - >(lstas_inv_sort1 … H2) -X // -| #i #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #T #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0 - elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d0 ] #HLK1 [ #Hd1 | #Hd0 #H ] - lapply (drop_mono … HLK0 … HLK1) -HLK0 #H0 destruct - elim (lstas_inv_lref1 … H2) -H2 * #K #Y #X [3,6: #d ] #HLK #HYX [1,2: #HXT #H0 |3,5: #HXT |4,6: #H1 #H2 ] - lapply (drop_mono … HLK … HLK1) -HLK #H destruct - [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ] - lapply (fqup_lref … G1 … HLK1) #H - lapply (drop_fwd_drop2 … HLK1) /4 width=8 by snv_lift, snv_lref, fqup_fpbg/ -| #p #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #HV1 #HT1 - lapply (da_inv_bind … Hd1) -Hd1 #Hd1 - elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/ -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1 - lapply (da_inv_flat … Hd1) -Hd1 #Hd1 - elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct - lapply (IH1 … HT1 … Hd1 … HT10) /2 width=1 by fqup_fpbg/ #HT0 - lapply (lstas_scpds_aux … IH1 IH4 IH3 IH2 … Hd1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -d1 #H - elim (scpes_inv_abst2 … H) -H /3 width=6 by snv_appl, scpds_cprs_trans/ -| #U1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_cast … H1) -H1 - lapply (da_inv_flat … Hd1) -Hd1 - lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc deleted file mode 100644 index ed9b4e2fa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc +++ /dev/null @@ -1,139 +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/snv_aaa.ma". -include "basic_2/dynamic/snv_scpes.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,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h o G1 L1 T1. -#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] -[ #s #_ #_ #_ #_ #d1 #d2 #_ #_ #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 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 - elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0 - elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d ] #HLK1 [ #HVd1 | #HWd1 #H destruct ] - lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct - elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #X0 [3,6: #d0 ] #HK0 #HVX0 [1,2: #HX02 #H |3,5: #HX02 |4,6: #H1 #H2 ] destruct - lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct - [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ] - lapply (fqup_lref … G1 … HLK1) #HKV1 - elim (lpr_drop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #W2 | #V2 ] #HK12 [ #HW12 | #HW12 | #HV12 ] #H destruct - lapply (drop_fwd_drop2 … HLK2) #H2 - elim (cpr_inv_lref1 … H3) -H3 - [1,3,5: #H destruct -HLK1 - |2,4,6: * #K #V #X #H #HVX #HX3 - lapply (drop_mono … H … HLK1) -H -HLK1 #H destruct - ] - [ lapply (IH2 … HWd1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H - elim (da_lstas … H d0) -H - elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 - elim (lift_total V2 0 (i+1)) - /3 width=12 by cpcs_lift, lstas_succ, ex2_intro/ - | elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0 - /3 width=5 by fqup_fpbg, lstas_zero, ex2_intro/ - | elim (IH1 … HVd1 … HVX0 … HV12 … HK12) -IH1 -HVd1 -HVX0 -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 … HVd1 … HVX0 … HVX … HK12) -IH1 -HVd1 -HVX0 -HVX -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -d1 #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 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #_ #HT1 - lapply (da_inv_bind … Hd1) -Hd1 #Hd1 - elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct - elim (cpr_inv_bind1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct - elim (IH1 … Hd1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hd1 -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 … Hd1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hd1 -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, drop_drop, ex2_intro/ - ] -| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1 - lapply (da_inv_flat … Hd1) -Hd1 #Hd1 - elim (lstas_inv_appl1 … H2) -H2 #X #HT1U #H destruct - elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -d0 -W1 -U1 -HV1 -IH4 -IH3 -IH2 - elim (IH1 … Hd1 … HT1U … HT12 … HL12) -IH1 -Hd1 -HT1U - /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 … Hd1) -Hd1 #Hd1 - elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct - elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -d0 - elim (snv_fwd_da … HW2) #d0 #HW2d - lapply (cprs_scpds_div … HW20 … HW2d … HVW1) -W0 #H21 - elim (snv_fwd_da … HV1) #d #HV1d - elim (da_scpes_aux … IH4 IH3 IH2 … HW2d … HV1d … H21) /2 width=1 by fqup_fpbg/ #_ #H - (plus_minus_k_k d 1) in HV1d; // -H #HV1d - lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32 - lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3 - lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 - lapply (IH2 … HW2d … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2d #HW3d - lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV1d #HV2d - elim (IH1 … Hd1 … HT2U … HT23 (L2.ⓛW3)) -HT2U /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23 - elim (lsubsv_lstas_trans … o … HTU3 … Hd21 … (L2.ⓓⓝW3.V2)) -HTU3 - [ #U4 #HT3U4 #HU43 -IH1 -IH2 -IH3 -IH4 -d -d1 -HW3 -HV2 -HT2 - @(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4 - @(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43 - @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/ - /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/ - | -U3 - @(lsubsv_beta … (d-1)) /3 width=7 by fqup_fpbg/ - @shnv_cast [1,2: // ] #d0 #Hd0 - lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3d … HV2d … d0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3d -HV2d -H32 - /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ - | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/ - ] - | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -d0 -W1 -HV1 -IH4 -IH3 -IH2 - elim (snv_inv_bind … HT1) -HT1 #_ #HT0 - lapply (da_inv_bind … Hd1) -Hd1 #Hd1 - elim (lstas_inv_bind1 … HT1U) -HT1U #U0 #HTU0 #H destruct - elim (IH1 … Hd1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hd1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02 - lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10 - lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02 - lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02 - lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02 - lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) - /4 width=3 by lstas_appl, lstas_bind, cpr_theta, ex2_intro/ - ] -| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2 - elim (snv_inv_cast … H1) -H1 #U1 #_ #HT1 #_ #_ -U1 - lapply (da_inv_flat … Hd1) -Hd1 #Hd1 - lapply (lstas_inv_cast1 … H2) -H2 #HTU1 - elim (cpr_inv_cast1 … H3) -H3 - [ * #U2 #T2 #_ #HT12 #H destruct - elim (IH1 … Hd1 … HTU1 … HT12 … HL12) -IH1 -Hd1 -HTU1 -HL12 - /3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/ - | #HT1X3 elim (IH1 … Hd1 … HTU1 … HT1X3 … HL12) -IH1 -Hd1 -HTU1 -HL12 - /2 width=3 by fqup_fpbg, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_preserve.etc deleted file mode 100644 index 482b94451..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_preserve.etc +++ /dev/null @@ -1,94 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fsb_aaa.ma". -include "basic_2/dynamic/snv_da_lpr.ma". -include "basic_2/dynamic/snv_lstas.ma". -include "basic_2/dynamic/snv_lstas_lpr.ma". -include "basic_2/dynamic/snv_lpr.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Main preservation properties *********************************************) - -lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → - ∧∧ IH_da_cpr_lpr h o G L T - & IH_snv_cpr_lpr h o G L T - & IH_snv_lstas h o G L T - & IH_lstas_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT -#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A -#G #L #T #A #_ #IH -A @and4_intro -[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux -| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux -] -@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H // -qed-. - -theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/ -qed-. - -theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/ -qed-. - -theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/ -qed-. - -theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T. -#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/ -qed-. - -(* Advanced preservation properties *****************************************) - -lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G #L1 #T1 #HT1 #T2 #H -@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ -qed-. - -lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. -#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H -@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ -qed-. - -lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2 -[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] → - ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 -elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 -lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_scpes.etc deleted file mode 100644 index 61d7fbdea..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_scpes.etc +++ /dev/null @@ -1,198 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpbg_fpbs.ma". -include "basic_2/equivalence/scpes_cpcs.ma". -include "basic_2/equivalence/scpes_scpes.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,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. - -definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. - -definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. - -definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝ - λh,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → - ∀d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → - ∀U. ⦃G, L⦄ ⊢ T •*[h, d2] U → ⦃G, L⦄ ⊢ U ¡[h, o]. - -(* Properties for the preservation results **********************************) - -fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #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,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. -#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H -@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ -qed-. - -fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → - ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2. -#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d1 #Hd1 #T2 #d2 * #T #d0 #Hd20 #H #HT1 #HT2 #L2 #HL12 -lapply (da_mono … H … Hd1) -H #H destruct -lapply (lstas_da_conf … HT1 … Hd1) #Hd12 -lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12 -/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/ -qed-. - -fact da_scpes_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → - ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → - ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → - ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22. -#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #d11 #Hd11 #d12 #Hd12 #d21 #d22 * #T #HT1 #HT2 -elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd11 … HT1 … L) -Hd11 -HT1 // -elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 // -/3 width=7 by da_mono, and3_intro/ -qed-. - -fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #d1 #d2 #Hd21 #Hd1 #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 … Hd21 … 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 -d1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. -#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #d2 * #W1 #d1 #Hd21 #HTd1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 -elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 -lapply (IH2 … H01 … HTd1 … 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=6 by ex4_2_intro, ex2_intro/ -qed-. - -fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] → - ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2. -#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #d1 #d2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12 -elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 -elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 -elim (cprs_conf … H1 … H2) -T0 -/3 width=5 by scpds_div, scpds_cprs_trans/ -qed-. - -fact lstas_scpds_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] → - ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 → - ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2. -#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2 -lapply (da_mono … H … HTd) -H #H destruct -lapply (lstas_da_conf … HT1 … HTd) #HTd1 -lapply (lstas_da_conf … HTX … HTd) #HXd -lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?) -[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2 -elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12) -[ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd - /5 width=6 by lstas_scpds, scpds_div, cprs_strap1, lstas_cpr, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro/ -| elim (da_lstas … HTd1 0) #X1 #HTX1 #_ - lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1 - elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXd … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXd -HXT1 -HXT2 - /4 width=8 by cpcs_scpes, cpcs_cpr_conf, fpbg_fpbs_trans, lstas_fpbs, lstas_cpr, monotonic_le_minus_l/ -] -qed-. - -fact scpes_le_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → - ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → - ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 → - ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2. -#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20 -elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_ -elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_ -lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10 -[1,2,3: // | >eq_minus_O [2: // ] eq_minus_O [2: // ] commutative_plus in ⊢ (??%); /4 width=7 by ex4_3_intro, or_intror/ - ] - | #m1 #m2 #T0 #H1T10 #H2T10 #HT0 #H #HT2 destruct -H1T1 -H2T1 -HT1 - >associative_plus in ⊢ (??%); /4 width=7 by cpms_step_dx, ex4_3_intro, or_intror/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc deleted file mode 100644 index e73de4930..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( 𝐏 [ term 46 h, term 46 o ] ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Positive $h $o $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc deleted file mode 100644 index 1b6b1197e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc +++ /dev/null @@ -1,63 +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 "static_2/notation/relations/positive_3.ma". -include "static_2/syntax/item_sd.ma". -include "static_2/syntax/term.ma". - -(* DEGREE POSITIVITY ON TERMS ***********************************************) - -inductive tdpos (h) (o): predicate term ≝ -| tdpos_sort: ∀s,d. deg h o s (↑d) → tdpos h o (⋆s) -| tdpos_lref: ∀i. tdpos h o (#i) -| tdpos_gref: ∀l. tdpos h o (§l) -| tdpos_pair: ∀I,V,T. tdpos h o V → tdpos h o T → tdpos h o (②{I}V.T) -. - -interpretation - "context-free degree positivity (term)" - 'Positive h o T = (tdpos h o T). - -(* Basic inversion lemmas ***************************************************) - -fact tdpos_inv_sort_aux (h) (o): - ∀X. 𝐏[h,o]⦃X⦄ → ∀s. X = ⋆s → ∃d. deg h o s (↑d). -#h #o #H * -[ #s #d #Hsd #x #H destruct /2 width=2 by ex_intro/ -| #i #x #H destruct -| #l #x #H destruct -| #I #V #T #_ #_ #x #H destruct -] -qed-. - -lemma tdpos_inv_sort (h) (o): ∀s. 𝐏[h,o]⦃⋆s⦄ → ∃d. deg h o s (↑d). -/2 width=3 by tdpos_inv_sort_aux/ qed-. - -fact tdpos_inv_pair_aux (h) (o): ∀X. 𝐏[h,o]⦃X⦄ → ∀I,V,T. X = ②{I}V.T → - ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄. -#h #o #H * -[ #s #d #_ #Z #X1 #X2 #H destruct -| #i #Z #X1 #X2 #H destruct -| #l #Z #X1 #X2 #H destruct -| #I #V #T #HV #HT #Z #X1 #X2 #H destruct /2 width=1 by conj/ -] -qed-. - -lemma tdpos_inv_pair (h) (o): ∀I,V,T. 𝐏[h,o]⦃②{I}V.T⦄ → - ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄. -/2 width=4 by tdpos_inv_pair_aux/ qed-. - -(* Basic properties *********************************************************) - -axiom tdpos_total (h): ∀T. ∃o. 𝐏[h,o]⦃T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 39ffd838a..ffb7cbb90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -27,13 +27,17 @@ Stage "B" + + + λδ-2A completed with + confluence of rt-computation and + preservation of validity for rt-computation. + Behavioral component rt_computation completed. @@ -75,15 +79,15 @@ Relocation with reference transforming maps (rtmap). - λδ version 2A2 is started. + λδ-2B is started. - Stage "A1": "Extending the Applicability Condition" + Stage "A" - λδ version 2A1 appears too complex and is dismissed. + λδ-2A appears too complex and is dismissed. - λδ version 2A1 is released. + λδ version 2A is released. Iterated static type assignment defined (more elegantly) @@ -151,7 +155,7 @@ Confluence for context-free parallel reduction on terms. - λδ version 2 is started. + λδ-2A is started. Logical Structure of the Specification 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 e34970bbe..9e9a3dbc9 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 @@ -31,7 +31,7 @@ table { *) [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_preserve_sub" + "cnv_preserve" * ] } ] }