From 7e6fea0332e132a8cb89c689ba68c5e884c4354c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 23 Sep 2019 15:00:45 +0200 Subject: [PATCH] update in basic_2 + main result on acle proved --- .../lambdadelta/basic_2/dynamic/cnv_acle.ma | 42 +++++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 2 files changed, 43 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma new file mode 100644 index 000000000..4a4a015ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.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 "static_2/syntax/acle.ma". +include "basic_2/dynamic/cnv_aaa.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with preorder for applicability domains ***********************) + +lemma cnv_acle_trans (h) (a1) (a2): + a1 ⊆ a2 → ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a1] → ⦃G,L⦄ ⊢ T ![h,a2]. +#h #a1 #a2 #Ha12 #G #L #T #H elim H -G -L -T +[ /1 width=1 by cnv_sort/ +| /3 width=1 by cnv_zero/ +| /3 width=1 by cnv_lref/ +| /3 width=1 by cnv_bind/ +| #n1 #p #G #L #V #W #T #U #Hn1 #_ #_ #HVW #HTU #IHV #IHT + elim (Ha12 … Hn1) -a1 #n2 #Hn2 #Hn12 + /3 width=11 by cnv_appl_ge/ +| /3 width=3 by cnv_cast/ +] +qed-. + +lemma cnv_acle_omega (h) (a): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L⦄ ⊢ T ![h,𝛚]. +/3 width=3 by cnv_acle_trans, acle_omega/ qed-. + +lemma cnv_acle_one (h) (a) (n): + ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,𝟏] → ad a n → ⦃G,L⦄ ⊢ T ![h,a]. +/3 width=3 by cnv_acle_trans, acle_one/ 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 e719304bf..4176396a0 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 @@ -25,7 +25,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_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "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_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } -- 2.39.2