From eeeaecfafd5ddffa54a41356104fbc60369e5d73 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 8 Sep 2018 21:09:55 +0200 Subject: [PATCH] update in static_2 and basic_2 + cnv_cpms_conf_aux proved for positive terms wrt the system of reference + unused files parked or removed --- .../basic_2/dynamic/cnv_cpm_tdpos.ma | 55 ++++++++++++ .../basic_2/dynamic/cnv_cpms_conf.ma | 83 ++++++++++++++----- .../basic_2/dynamic/cnv_cpms_tdpos.ma | 39 +++++++++ .../lambdadelta/basic_2/dynamic/partial.txt | 3 - .../{dynamic => etc/cnv}/cnv_cpms_tdeq.etc | 0 .../cnv/cnv_preserve_far.etc} | 0 .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../notation/relations/positive_3.ma} | 4 +- .../lambdadelta/static_2/syntax/tdpos.ma | 63 ++++++++++++++ .../lambdadelta/static_2/web/static_2_src.tbl | 4 + 10 files changed, 225 insertions(+), 28 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => etc/cnv}/cnv_cpms_tdeq.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic/cnv_preserve_far.ma => etc/cnv/cnv_preserve_far.etc} (100%) rename matita/matita/contribs/lambdadelta/{basic_2/notation/relations/predstar_7.ma => static_2/notation/relations/positive_3.ma} (85%) create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma new file mode 100644 index 000000000..4cb320959 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdpos.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tdpos.ma". +include "basic_2/dynamic/cnv_cpm_tdeq.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Forward lemmas with positive rt-transition for terms *********************) + +lemma cpm_tdeq_fwd_tdpos_sn (a) (h) (o) (n) (G): + ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → 𝐏[h,o]⦃T1⦄ → + ∧∧ T1 = T2 & 0 = n. +#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2 +@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2 +[ /2 width=1 by conj/ +| #L #s #_ #H1 #H + elim (tdpos_inv_sort … H) -H #d #H2 + lapply (deg_mono … H2 H1) -H1 -H2 #H destruct +| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #H + elim (tdpos_inv_pair … H) -H #_ #HT1 + elim IH // -IH -HT1 #H1 #H2 destruct + /2 width=1 by conj/ +| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #H -a -m -q -G -L -W -U1 + elim (tdpos_inv_pair … H) -H #_ #HT1 + elim IH // -IH -HT1 #H1 #H2 destruct + /2 width=1 by conj/ +| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #H + elim (tdpos_inv_pair … H) -H #HU1 #HT1 + elim IHU // -IHU -HU1 #H1 #H2 destruct + elim IHT // -IHT -HT1 #H1 #H2 destruct + /2 width=1 by conj/ +] +qed-. + +lemma cpm_fwd_tdpos_sn (a) (h) (o) (n) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ → + ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → + ∨∨ ∧∧ T1 = T2 & 0 = n | (T1 ≛[h,o] T2 → ⊥). +#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #HT12 +elim (tdeq_dec h o T1 T2) #H +/3 width=9 by cpm_tdeq_fwd_tdpos_sn, or_intror, or_introl/ +qed-. 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 e6fb158e6..a86d5c311 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,36 +12,51 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predstar_7.ma". include "basic_2/dynamic/cnv_cpm_trans.ma". include "basic_2/dynamic/cnv_cpm_conf.ma". +include "basic_2/dynamic/cnv_cpms_tdpos.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2. - ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n. - -interpretation - "context-sensitive parallel stratified t-bound rt-computarion (term)" - 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2). +(* Sub confluence propery with t-bound rt-computation for terms *************) -definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝ - λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] → - ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T. +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-. -(* Sub confluence propery with t-bound rt-computation for terms *************) +fact cnv_cpms_conf_lpr_refl_step_aux (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] → + ∀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⦄ ⊢ T0 ➡*[m21+m22,h] T& ⦃G0,L2⦄ ⊢ T2 ➡*[h] T. +#a #h #o #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0 +#X2 #HX02 #HnX02 #T2 #HXT2 +#L1 #HL01 #L2 #HL02 +lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 +elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) // +[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_cpsms_conf_lpr a h o G1 L1 T1. -#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0 -#n1 #T1 * #m11 #m12 #X1 #HnX01 #HX01 #HXT1 #H1 -#n2 #T2 * #m21 #m22 #X2 #HnX02 #HX02 #HXT2 #H2 -#L1 #HL01 #L2 #HL02 destruct +fact cnv_cpms_conf_lpr_step_step_aux (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 → + ∀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. +#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 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 @@ -55,3 +70,27 @@ lapply (cpms_trans … HTZ1 … HZ01) -Z1 [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 +#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 + 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/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt deleted file mode 100644 index f4923619f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt +++ /dev/null @@ -1,3 +0,0 @@ -cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma -cnv_preserve_far.ma cnv_cpm_trans.ma cnv_cpm_conf.ma -lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma lsubv_lsubv.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve_far.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve_far.etc 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 a805b584e..eaee5cf14 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_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma similarity index 85% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma rename to matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma index bbd49fddd..e73de4930 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma +++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 n, break term 46 h, break term 46 o ] break term 46 T2 )" +notation "hvbox( 𝐏 [ term 46 h, term 46 o ] ⦃ term 46 T ⦄ )" non associative with precedence 45 - for @{ 'PRedStar $n $h $o $G $L $T1 $T2 }. + for @{ 'Positive $h $o $T }. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma new file mode 100644 index 000000000..1b6b1197e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdpos.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 4dcb17989..1f7d34c0b 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 @@ -111,6 +111,10 @@ table { [ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] + [ { "degree positivity" * } { + [ [ "for terms" ] "tdpos" + "( 𝐏[?,?]⦃?⦄ )" * ] + } + ] [ { "degree-based equivalence" * } { [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ] [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ] -- 2.39.2