From: Ferruccio Guidi Date: Tue, 18 Sep 2018 18:57:20 +0000 (+0200) Subject: update in static_2 and basic_2 X-Git-Tag: make_still_working~280 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d1dc967bc12041b9d23ee945db9dd91335e8c1d;p=helm.git update in static_2 and basic_2 + restricted rt-computation; more results towards preservation --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma index 85abc0c65..4919e3eae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma @@ -115,6 +115,16 @@ elim (cpm_inv_cast1 … H1) -H1 [ * || * ] ] qed-. +lemma cpm_tdeq_inv_bind_dx (a) (h) (o) (n) (p) (I) (G) (L): + ∀X. ⦃G, L⦄ ⊢ X ![a,h] → + ∀V,T2. ⦃G, L⦄ ⊢ X ➡[n,h] ⓑ{p,I}V.T2 → X ≛[h,o] ⓑ{p,I}V.T2 → + ∃∃T1. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T1. +#a #h #o #n #p #I #G #L #X #H0 #V #T2 #H1 #H2 +elim (tdeq_inv_pair2 … H2) #V0 #T1 #_ #_ #H destruct +elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T0 #HV #HT1 #H1T12 #H2T12 #H destruct +/2 width=5 by ex5_intro/ +qed-. + (* Eliminators with restricted rt-transition for terms **********************) lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …): diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma new file mode 100644 index 000000000..a0bda539d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma @@ -0,0 +1,97 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "basic_2/dynamic/cnv_cpm_tdeq.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +definition IH_cnv_cpm_tdeq_cpm_trans (a) (h) (o): relation3 genv lenv term ≝ + λ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. + +(* Transitive properties restricted rt-transition for terms *****************) + +fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (o) (G0) (L0) (T0): + (∀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⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans a h o G L T) → + ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans a h o G L T1. +#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] +[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -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 #_ #H0T1 #H1T1 #H2T1 #H destruct + elim (cpm_inv_bind1 … HX2) -HX2 * + [ #V2 #T2 #HV12 #HT2 #H destruct + elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02 + lapply (IH2 … H0T1 … HT10 (L.ⓑ{I}V1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0 + lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓑ{I}V2)) -H1T02 #H1T02 + /3 width=6 by cpm_bind, tdeq_pair, ex3_intro/ + | #T2 #HT2 #HTX2 #H1 #H2 destruct -IH2 + elim (tdeq_inv_lifts_dx … H2T1 … HT2) -H2T1 #XT #HXT1 #H2XT2 + lapply (cpm_inv_lifts_bi … H1T1 (Ⓣ) … HXT1 … HT2) -T [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1XT2 + lapply (cnv_inv_lifts … H0T1 (Ⓣ) … HXT1) -H0T1 [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H0XT2 + elim (IH1 … H0XT2 … H1XT2 H2XT2 … HTX2) -T2 -IH1 -H0XT2 [| /2 width=1 by fqup_zeta/ ] #T2 #HXT2 #H1TX2 #H2XT2 + /3 width=4 by cpm_zeta, ex3_intro/ + ] +| #V1 #XT1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct + elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #m #q #W1 #U1 #XT #_ #_ #_ #_ #H0T1 #H1T1 #H2T1 #H destruct -m -q -W1 -U1 + elim (cpm_inv_appl1 … HX2) -HX2 * + [ #V2 #T2 #HV12 #HT2 #H destruct -IH2 + elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -XT -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02 + /3 width=6 by cpm_appl, tdeq_pair, ex3_intro/ + | #p #V2 #W1 #W2 #T #T2 #HV12 #HW12 #HT2 #H1 #H2 destruct + elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct + elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02 + lapply (IH2 … H0T1 … HT10 (L.ⓛW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0 + lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓⓝW2.V2)) -H1T02 #H1T02 + /3 width=6 by cpm_beta, cpm_bind, tdeq_pair, ex3_intro/ + | #p #V2 #V0 #W1 #W2 #T #T2 #HV12 #HV20 #HW12 #HT2 #H1 #H2 destruct + elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct + elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02 + lapply (IH2 … H0T1 … HT10 (L.ⓓW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0 + lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓW2)) -H1T02 + /4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/ + ] +| #U1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -IH2 + elim (cpm_tdeq_inv_cast_sn … H0 … H1X H2X) -H0 -H1X -H2X #U0 #U #T #_ #_ #H0U1 #H1U1 #H2U1 #H0T1 #H1T1 #H2T1 #H destruct -U0 + elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ] + [ #U2 #T2 #HU2 #HT2 #H destruct + elim (IH1 … H0U1 … H1U1 H2U1 … HU2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02 + elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02 + /3 width=6 by cpm_cast, tdeq_pair, ex3_intro/ + | #HTX2 -U -H0U1 + elim (IH1 … H0T1 … H1T1 H2T1 … HTX2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02 + /3 width=4 by cpm_eps, ex3_intro/ + | #m2 #HUX2 #H destruct -T -H0T1 + elim (IH1 … H0U1 … H1U1 H2U1 … HUX2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02 + /3 width=4 by cpm_ee, ex3_intro/ + ] +] +qed-. + +fact cnv_cpm_tdeq_cpm_trans_aux (a) (h) (o) (G0) (L0) (T0): + (∀G,L,T. ⦃G0, L0, T0⦄ >[h, o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) → + IH_cnv_cpm_tdeq_cpm_trans a h o G0 L0 T0. +#a #h #o #G0 #L0 #T0 +@(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0 +/5 width=10 by cnv_cpm_tdeq_cpm_trans_sub, fqup_fpbg_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma new file mode 100644 index 000000000..3950479e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tdeq_trans.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with restricted rt-computation for terms **********************) + +fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (o) (G) (L) (T1): + ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → (T1 ≛[h,o] T2 → ⊥) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → + ∃∃n1,n2,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T0 & T1 ≛[h,o] T0 → ⊥ & ⦃G, L⦄ ⊢ T0 ➡*[n2,h] T2 & n1+n2 = n. +#a #h #n #o #G #L #T1 #T2 #H +@(cpms_ind_sn … H) -n -T1 +[ #_ #H2T2 elim H2T2 -H2T2 // +| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 + elim (tdeq_dec h o T1 T) #H2T1 + [ elim (tdeq_dec h o T T2) #H2T2 + [ -IH -IH2 -IH1 -H0T1 /4 width=7 by tdeq_trans, ex4_3_intro/ + | lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T + elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2 + #m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct + elim (cnv_cpm_tdeq_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0 + #T3 #H1T13 #H1T30 #H2T30 + @(ex4_3_intro … H1T13) /4 width=3 by cpms_step_sn, tdeq_canc_sn/ (**) (* explicit constructor *) + ] + | -IH -IH2 -IH1 -H2T12 /3 width=7 by tdeq_trans, ex4_3_intro/ + ] +] +qed-. + +fact cpms_tdeq_ind_sn (a) (h) (o) (G) (L) (T2) (Q:relation2 …): + (⦃G, L⦄ ⊢ T2 ![a,h] → Q 0 T2) → + (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T → ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G, L⦄ ⊢ T ![a,h] → T ≛[h,o] T2 → Q n2 T → Q (n1+n2) T1) → + ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T2 → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → + Q n T1. +#a #h #o #G #L #T2 #Q #IB1 #IB2 #n #T1 #H +@(cpms_ind_sn … H) -n -T1 +[ -IB2 #H0T2 #_ #_ #_ /2 width=1 by/ +| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 -IB1 + elim (tdeq_dec h o T1 T) #H2T1 + [ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T + lapply (tdeq_canc_sn … H2T1 … H2T12) -H2T12 #H2T2 + /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/ + | -IB2 -IH -IH2 -IH1 + elim (cnv_fpbg_refl_false … o … H0T1) -a -Q + /3 width=8 by cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc new file mode 100644 index 000000000..4cb320959 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc @@ -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/etc/tdpos/cnv_cpms_tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpms_tdpos.etc new file mode 100644 index 000000000..049e0727f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpms_tdpos.etc @@ -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/etc/tdpos/positive_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc new file mode 100644 index 000000000..e73de4930 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc @@ -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/basic_2/etc/tdpos/tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc new file mode 100644 index 000000000..1b6b1197e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc @@ -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/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma index ea81fda63..7584e81c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma @@ -20,10 +20,6 @@ include "basic_2/rt_computation/cpms_fpbs.ma". (* Forward lemmas with proper parallel rst-computation for closures *********) -lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ → - ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. -/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-. - lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ → ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-. @@ -31,3 +27,14 @@ lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T → ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. /3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-. + +lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ → + ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. +/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-. + +lemma cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg (h) (o) (G) (L) (T1): + ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛[h,o] T → ⊥) → + ∀n2,T2. ⦃G,L⦄⊢ T ➡*[n2,h] T2 → T1 ≛[h,o] T2 → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T1⦄. +#h #o #G #L #T1 #n1 #T #H1T1 #H2T1 #n2 #T2 #H1T2 #H2T12 +/4 width=7 by cpms_fwd_fpbs, cpm_fpb, fpbs_tdeq_trans, tdeq_sym, ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma index 3641326f8..d7a1ccae0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "static_2/static/fdeq_fqup.ma". include "static_2/static/fdeq_fdeq.ma". include "basic_2/rt_transition/fpbq_fpb.ma". +include "basic_2/rt_computation/fpbs_fqup.ma". include "basic_2/rt_computation/fpbg.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) @@ -61,6 +61,13 @@ lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L #h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/ qed-. +(* Advanced properties with plus-iterated structural successor for closures *) + +lemma fqup_fpbg_trans (h) (o): + ∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ⊐+ ⦃G,L,T⦄ → + ∀G2,L2,T2. ⦃G,L,T⦄ >[h,o] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ >[h,o] ⦃G2,L2,T2⦄. +/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-. + (* Advanced inversion lemmas of parallel rst-computation on closures ********) (* Basic_2A1: was: fpbs_fpbg *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 4ab5cff51..d0d19e4a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -232,6 +232,13 @@ elim (cpm_inv_bind1 … H) -H ] qed-. +lemma cpm_inv_abst_bi: ∀n,h,p1,p2,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}V1.T1 ➡[n,h] ⓛ{p2}V2.T2 → + ∧∧ ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ➡[n,h] T2 & p1 = p2. +#n #h #p1 #p2 #G #L #V1 #V2 #T1 #T2 #H +elim (cpm_inv_abst1 … H) -H #XV #XT #HV #HT #H destruct +/2 width=1 by and3_intro/ +qed-. + (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *) (* Basic_2A1: includes: cpr_inv_appl1 *) lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 → 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 336b99505..e10340776 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_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tfeq_trans" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index 1d6225393..060f3b805 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -56,6 +56,10 @@ definition deliftable2_bi: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 → ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2. +definition deliftable2_dx: predicate (relation term) ≝ + λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 → + ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2. + (* Basic inversion lemmas ***************************************************) fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s. @@ -329,6 +333,11 @@ qed-. (* Basic properties *********************************************************) +lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R. +#R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2 +elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/ +qed-. + lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2). #T1 #T2 #f1 #H elim H -T1 -T2 -f1 /4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/ diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma index fb5d8247f..12affa3a1 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma @@ -62,6 +62,9 @@ lemma tdeq_inv_lifts_sn: ∀h,o. deliftable2_sn (tdeq h o). ] qed-. +lemma tdeq_inv_lifts_dx (h) (o): deliftable2_dx (tdeq h o). +/3 width=3 by tdeq_inv_lifts_sn, deliftable2_sn_dx, tdeq_sym/ qed-. + lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o). /3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma index d008d5e86..828e2ad0f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma @@ -29,6 +29,19 @@ interpretation "context-free degree-based equivalence (term)" 'StarEq h o T1 T2 = (tdeq h o T1 T2). +(* Basic properties *********************************************************) + +lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o). +#h #o #T elim T -T /2 width=1 by tdeq_pair/ +* /2 width=1 by tdeq_lref, tdeq_gref/ +#s elim (deg_total h o s) /2 width=3 by tdeq_sort/ +qed. + +lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). +#h #o #T1 #T2 #H elim H -T1 -T2 +/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ +qed-. + (* Basic inversion lemmas ***************************************************) fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀s1. X = ⋆s1 → @@ -79,6 +92,14 @@ lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y → ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2. /2 width=3 by tdeq_inv_pair1_aux/ qed-. +lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 → + ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1. +#h #o #I #X1 #V2 #T2 #H +elim (tdeq_inv_pair1 h o I V2 T2 X1) +[ #V1 #T1 #HV #HT #H destruct ] +/3 width=5 by tdeq_sym, ex3_2_intro/ +qed-. + (* Advanced inversion lemmas ************************************************) lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y → ∀d. deg h o s1 d → @@ -122,18 +143,7 @@ lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≛[h, o] Y → ∃J. Y = ⓪{J}. /3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/ qed-. -(* Basic properties *********************************************************) - -lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o). -#h #o #T elim T -T /2 width=1 by tdeq_pair/ -* /2 width=1 by tdeq_lref, tdeq_gref/ -#s elim (deg_total h o s) /2 width=3 by tdeq_sort/ -qed. - -lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). -#h #o #T1 #T2 #H elim H -T1 -T2 -/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ -qed-. +(* Advanced properties ******************************************************) lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2). #h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] 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 1f7d34c0b..4dcb17989 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,10 +111,6 @@ 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" * ]