From c0d38a82464481e3c8fd68e4b00d7b9b448df462 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 3 Sep 2019 19:36:47 +0200 Subject: [PATCH] milestone in basic_2 We parametrize applicability condition with a generic subset of numbers. --- .../lambdadelta/basic_2/dynamic/cnv_cpme.ma | 4 +- .../lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma | 5 +- .../basic_2/dynamic/cnv_cpmuwe_cpme.ma | 35 +++++++++ .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 3 +- .../basic_2/rt_computation/cnuw.ma | 57 +------------- .../basic_2/rt_computation/cnuw_cnuw.ma | 57 +++++++++++++- .../basic_2/rt_computation/cnuw_tdeq.ma | 74 ------------------- .../basic_2/rt_computation/cpme.ma | 13 ++++ .../basic_2/rt_computation/cpms.ma | 30 ++++++++ .../basic_2/rt_computation/cpmuwe_csx.ma | 18 +++-- .../basic_2/rt_computation/cpre_cpms.ma | 2 +- .../basic_2/rt_computation/cpre_cpre.ma | 2 +- .../basic_2/rt_computation/cpre_csx.ma | 4 +- .../basic_2/rt_computation/cprs_tweq.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpm.ma | 25 +++++++ .../lambdadelta/basic_2/web/basic_2.ldw.xml | 7 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 7 +- .../static_2/relocation/lifts_tweq.ma | 2 +- .../static_2/syntax/term_weight.ma | 4 + .../lambdadelta/static_2/syntax/tweq.ma | 6 +- .../lambdadelta/static_2/syntax/tweq_tdeq.ma | 32 ++++++++ .../lambdadelta/static_2/web/static_2_src.tbl | 2 +- 22 files changed, 229 insertions(+), 162 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe_cpme.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw_tdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma index a9091b059..9e0da7d55 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpme.ma @@ -18,7 +18,7 @@ include "basic_2/dynamic/cnv_preserve.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -(* Properties with evaluation for t-bound rt-transition on terms ************) +(* Properties with t-bound evaluation on terms ******************************) lemma cnv_cpme_trans (a) (h) (n) (G) (L): ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → @@ -33,7 +33,7 @@ lemma cnv_cpme_cpms_conf (a) (h) (n) (G) (L): #a #h #n #G #L #T0 #HT0 #T1 #HT01 #T2 * #HT02 #HT2 elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 Stage "B" + + Applicability condition is now parametrized + with a generic subset of numbers. + - Parametrized applicability condition + Applicability condition parametrized + with an initial interval of numbers allows λδ-2B to generalize both λδ-2A and λδ-1B. 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 daa511a89..fdfa71e69 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_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] + [ [ "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" * ] } ] } @@ -67,9 +67,8 @@ table { ] [ { "t-bound context-sensitive parallel rt-computation" * } { [ [ "t-unbound whd evaluation for terms" ] "cpmuwe ( ⦃?,?⦄ ⊢ ? ⬌*𝐍𝐖*[?,?] ? )" "cpmuwe_csx" + "cpmuwe_cpmuwe" * ] - [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_tdeq" + "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ] - - [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ] + [ [ "t-unbound whd normal form for terms" ] "cnuw ( ⦃?,?⦄ ⊢ ⬌𝐍𝐖*[?] ? )" "cnuw_drops" + "cnuw_simple" + "cnuw_cnuw" * ] + [ [ "t-bpund evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ] [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma index 3802cb1d4..addd91c72 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tweq.ma @@ -96,7 +96,7 @@ lemma tweq_inv_lifts_bi: deliftable2_bi tweq. ] qed-. -lemma tweq_inv_abbr_pos_sn_X_lifts_Y_Y (T) (f:rtmap): +lemma tweq_inv_abbr_pos_x_lifts_y_y (T) (f:rtmap): ∀V,U. +ⓓV.U ≅ T → ⬆*[f]T ≘ U → ⊥. @(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma index c8d4c974d..6948a54a8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_weight.ma @@ -31,6 +31,10 @@ lemma tw_pos: ∀T. 1 ≤ ♯{T}. #T elim T -T // qed. +lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}. +#I #V #T /2 width=1 by le_S_S/ +qed. + (* Basic_1: removed theorems 11: wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma index fd31eb05e..91234b9ce 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq.ma @@ -15,10 +15,6 @@ include "static_2/notation/relations/approxeq_2.ma". include "static_2/syntax/term_weight.ma". -lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}. -#I #V #T /2 width=1 by le_S_S/ -qed. - (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************) inductive tweq: relation term ≝ @@ -211,7 +207,7 @@ elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct /2 width=1 by conj/ qed-. -lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥. +lemma tweq_inv_cast_xy_y: ∀T,V. ⓝV.T ≅ T → ⊥. @(f_ind … tw) #n #IH #T #Hn #V #H destruct elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V /2 width=4 by/ diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma new file mode 100644 index 000000000..fb8d7e704 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tweq_tdeq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "static_2/syntax/tdeq.ma". +include "static_2/syntax/tweq.ma". + +(* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************) + +(* Properties with sort-irrelevant equivalence for terms ********************) + +lemma tdeq_tweq: ∀T1,T2. T1 ≛ T2 → T1 ≅ T2. +#T1 #T2 #H elim H -T1 -T2 [||| * [ #p ] * #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT ] +[ /1 width=1 by tweq_sort/ +| /1 width=1 by tweq_lref/ +| /1 width=1 by tweq_gref/ +| cases p -p /2 width=1 by tweq_abbr_pos, tweq_abbr_neg/ +| /1 width=1 by tweq_abst/ +| /2 width=1 by tweq_appl/ +| /2 width=1 by tweq_cast/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 5fb750e3f..257341c6a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -120,7 +120,7 @@ table { } ] [ { "sort-irrelevant whd equivalence" * } { - [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tueq" * ] + [ [ "for terms" ] "tweq" + "( ? ≅ ? )" "tweq_simple" + "tweq_tdeq" + "tweq_tueq" * ] } ] [ { "sort-irrelevant equivalence" * } { -- 2.39.2