From: Ferruccio Guidi Date: Sat, 8 Sep 2018 19:09:55 +0000 (+0200) Subject: update in static_2 and basic_2 X-Git-Tag: make_still_working~283 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=eeeaecfafd5ddffa54a41356104fbc60369e5d73 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 --- 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 + iter_n_Sm - /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/ - ] -| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct - elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct - elim (cpm_inv_bind1 … HX2) -HX2 * - [ #V2 #T2 #HV12 #HT2 #H destruct - elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02 - @(ex3_intro … (ⓑ{p,I}V2.T0)) - [ /2 width=1 by cpm_bind/ - | - | /2 width=1 by tdeq_pair/ - -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma new file mode 100644 index 000000000..049e0727f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdpos.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tdpos.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Forward lemmas with positive rt-computation for terms ********************) + +lemma cpms_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 + | ∃∃n1,n2,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T & (T1 ≛[h,o] T → ⊥) & ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2=n. +#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #H +@(cpms_ind_dx … H) -n -T2 +[ /3 width=1 by or_introl, conj/ +| #n1 #n2 #T #T2 #HT1 * * + [ #H1 #H2 #HT2 destruct -HT1 + elim (cpm_fwd_tdpos_sn … H1T1 H2T1 … HT2) -H1T1 -H2T1 + [ * #H1 #H2 destruct -HT2 /3 width=1 by or_introl, conj/ + | #HnT2 >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/cnv_preserve_far.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma deleted file mode 100644 index 7ab0ff8a2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma +++ /dev/null @@ -1,33 +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/cnv_cpm_trans.ma". - -(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) - -(* Far properties for preservation ******************************************) - -fact cnv_cpms_trans_lpr_far (a) (h) (o): - ∀G0,L0,T0. - (∀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, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1. -#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct -@(cpms_ind_dx … H) -n -T2 -[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 // -| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct - @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH - /3 width=4 by cpms_fpbg_trans/ -] -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/etc/cnv/cnv_cpms_tdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc new file mode 100644 index 000000000..da155423c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc @@ -0,0 +1,52 @@ +(* +axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) → + ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n. +axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥. + +lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h]. +#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 +#G0 #L0 #T0 #IH #G #L * [| * [| * ]] +[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0 + elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X * + [ #H #_ destruct // + | #s #H #_ #_ #_ destruct // + ] +| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct + elim (cnv_inv_bind … H0) #HV1 #_ + elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct + /3 width=6 by cnv_bind/ +| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct + elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1 + elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct + @(cnv_appl … Hm … HVW1) + +(* Properties with restricted rt-transition for terms ***********************) + +lemma pippo (a) (h) (o) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → + ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T → + ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2. +#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 +#G0 #L0 #T0 #IH #G #L * [| * [| * ]] +[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0 + elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X * + [ #H1 #H2 destruct /2 width=4 by ex3_intro/ + | #s #H1 #H2 #H3 #Hs destruct + elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm + /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/ + ] +| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct + elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct + elim (cpm_inv_bind1 … HX2) -HX2 * + [ #V2 #T2 #HV12 #HT2 #H destruct + elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02 + @(ex3_intro … (ⓑ{p,I}V2.T0)) + [ /2 width=1 by cpm_bind/ + | + | /2 width=1 by tdeq_pair/ + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve_far.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve_far.etc new file mode 100644 index 000000000..7ab0ff8a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_preserve_far.etc @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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_trans.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Far properties for preservation ******************************************) + +fact cnv_cpms_trans_lpr_far (a) (h) (o): + ∀G0,L0,T0. + (∀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, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1. +#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct +@(cpms_ind_dx … H) -n -T2 +[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 // +| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct + @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH + /3 width=4 by cpms_fpbg_trans/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma deleted file mode 100644 index bbd49fddd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma +++ /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 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 )" - non associative with precedence 45 - for @{ 'PRedStar $n $h $o $G $L $T1 $T2 }. 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/static_2/notation/relations/positive_3.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma new file mode 100644 index 000000000..e73de4930 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/positive_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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" * ]