From 5b529743ea1196df21bd937c2c0fb2fd0bc68423 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 11 Jun 2018 14:12:16 +0200 Subject: [PATCH] update in basic_2 + advances on nv ... --- .../lambdadelta/basic_2/dynamic/nv_aaa.ma | 42 ++++++++++ .../lambdadelta/basic_2/dynamic/nv_fqus.ma | 78 +++++++++++++------ .../basic_2/dynamic/{snv_fsb.ma => nv_fsb.ma} | 13 ++-- .../lambdadelta/basic_2/dynamic/partial.txt | 2 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 50 ------------ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 6 files changed, 104 insertions(+), 83 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_aaa.ma rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_fsb.ma => nv_fsb.ma} (70%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_aaa.ma new file mode 100644 index 000000000..2ed2b630a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_aaa.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpms_aaa.ma". +include "basic_2/dynamic/nv.ma". + +(* NATIVE VALIDITY FOR TERMS ************************************************) + +(* Forward lemmas on atomic arity assignment for terms **********************) + +(* Basic_2A1: uses: snv_fwd_aaa *) +lemma nv_fwd_aaa (a) (h): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. +#a #h #G #L #T #H elim H -G -L -T +[ /2 width=2 by aaa_sort, ex_intro/ +| #I #G #L #V #_ * /3 width=2 by aaa_zero, ex_intro/ +| #I #G #L #K #_ * /3 width=2 by aaa_lref, ex_intro/ +| #p * #G #L #V #T #_ #_ * #B #HV * #A #HA + /3 width=2 by aaa_abbr, aaa_abst, ex_intro/ +| #n #p #G #L #V #W #T0 #U0 #_ #_ #_ #HVW #HTU0 * #B #HV * #X #HT + lapply (cpms_aaa_conf … HV … HVW) -HVW #H1W + lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H + elim (aaa_inv_abst … H) -H #B0 #A #H2W #HU #H destruct + lapply (aaa_mono … H2W … H1W) -W #H destruct + /3 width=4 by aaa_appl, ex_intro/ +| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT + lapply (cpms_aaa_conf … HU … HU0) -HU0 #HU0 + lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H + lapply (aaa_mono … H … HU0) -U0 #H destruct + /3 width=3 by aaa_cast, ex_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma index f0649de3e..af3fba488 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma @@ -1,36 +1,64 @@ -(* Properties on subclosure *************************************************) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) -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 +include "basic_2/s_computation/fqus_fqup.ma". +include "basic_2/dynamic/nv_drops.ma". + +(* NATIVE VALIDITY FOR TERMS ************************************************) + +(* Properties with supclosure ***********************************************) + +(* Basic_2A1: uses: snv_fqu_conf *) +lemma nv_fqu_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h]. +#a #h #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 // + elim (nv_inv_zero … H) -H #I2 #L2 #V2 #HV2 #H destruct // +| * [ #p #I1 | * ] #G1 #L1 #V1 #T1 #H + [ elim (nv_inv_bind … H) -H // + | elim (nv_inv_appl … H) -H // + | elim (nv_inv_cast … H) -H // + ] +| #p #I1 #G1 #L1 #V1 #T1 #H + elim (nv_inv_bind … H) -H // +| #p #I1 #G1 #L1 #V1 #T1 #H destruct +| * #G1 #L1 #V1 #T1 #H + [ elim (nv_inv_appl … H) -H // + | elim (nv_inv_cast … H) -H // ] +| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU + /4 width=7 by nv_inv_lifts, drops_refl, drops_drop/ ] 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/ +(* Basic_2A1: uses: snv_fquq_conf *) +lemma nv_fquq_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h]. +#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [|*] +/2 width=5 by nv_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/ +(* Basic_2A1: uses: snv_fqup_conf *) +lemma nv_fqup_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h]. +#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by fqup_strap1, nv_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/ +(* Basic_2A1: uses: snv_fqus_conf *) +lemma nv_fqus_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h]. +#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H [|*] +/2 width=5 by nv_fqup_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fsb.ma similarity index 70% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fsb.ma index ddffd5e9d..47eb36f67 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fsb.ma @@ -12,13 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/computation/fsb_aaa.ma". -include "basic_2/dynamic/snv_aaa.ma". +include "basic_2/rt_computation/fsb_aaa.ma". +include "basic_2/dynamic/nv_aaa.ma". -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) +(* NATIVE VALIDITY FOR TERMS ************************************************) -(* forward lemmas on "qrst" strongly normalizing closures *********************) +(* Forward lemmas with strongly rst-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/ +(* Basic_2A1: uses: snv_fwd_fsb *) +lemma nv_fwd_fsb (a) (h) (o): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ≥[h, o] 𝐒⦃G, L, T⦄. +#a #h #o #G #L #T #H elim (nv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt index e5b27fe2d..71d809d22 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt @@ -1 +1 @@ -nv.ma nv_drops.ma +nv.ma nv_drops.ma nv_fqus.ma nv_aaa.ma nv_fsb.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma deleted file mode 100644 index 73aa7ccd9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ /dev/null @@ -1,50 +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/static/da_aaa.ma". -include "basic_2/computation/scpds_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,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. -#h #o #G #L #T #H elim H -G -L -T -[ /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 #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 * #B #HV * #X #HT - lapply (scpds_aaa_conf … HV … HVW0) -HVW0 #HW0 - lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H - elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct - lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/ -| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT - lapply (scpds_aaa_conf … HU … HU0) -HU0 #HU0 - lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H - lapply (aaa_mono … H … HU0) -U0 #H destruct /3 width=3 by aaa_cast, ex_intro/ -] -qed-. - -(* 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/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index f3ce21a86..413cf84ab 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 @@ -37,7 +37,7 @@ table { (* [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] *) - [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" (* + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ] + [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" "nv_fqus" + "nv_aaa" + "snv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ] } ] } -- 2.39.2