From 18d7afd216aee6c815eac30982d8ad4fa4521070 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 13 Mar 2017 19:29:33 +0000 Subject: [PATCH] cpx_tsts completed --- .../lambdadelta/basic_2/etc/cpxs/cpxs.etc | 9 -- .../basic_2/etc/lfpxs/lfpxs_cpxs.etc | 28 +++++++ .../lambdadelta/basic_2/etc/tsts/tsts.etc | 11 +++ .../basic_2/rt_computation/cpxs_cnx.ma | 26 ++++++ .../basic_2/rt_computation/cpxs_lsubr.ma | 24 ++++++ .../basic_2/rt_computation/cpxs_tsts.ma | 82 ++++++++++--------- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/cnx_cnx.ma | 28 +++++++ .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/syntax/tsts_vector.ma | 12 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 14 ++-- .../contribs/lambdadelta/partial_compile.sh | 1 + 12 files changed, 177 insertions(+), 62 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc index ada873d81..05e7c375d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc @@ -1,18 +1,9 @@ -lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr. -/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/ -qed-. lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. #h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/ qed. -lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U. -#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T // -#T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ -qed-. - lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) → ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2. #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc new file mode 100644 index 000000000..6edda23e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc @@ -0,0 +1,28 @@ +(* Advanced inversion lemmas ************************************************) + +lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2. +/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. + +lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1. +/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. + +(* Advanced eliminators *****************************************************) + +lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. + + +(* More advanced properties *************************************************) + +lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → + ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2. +/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc new file mode 100644 index 000000000..174cedd1d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tsts/tsts.etc @@ -0,0 +1,11 @@ +fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1.U1. +#T1 #T2 * -T1 -T2 +[ #J #I #W2 #U2 #H destruct +| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/ +] +qed-. + +lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1.U1. +/2 width=5 by tsts_inv_pair2_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma new file mode 100644 index 000000000..1dfedff90 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cnx_cnx.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Inversion lemmas with normal terms ***************************************) + +lemma cpxs_inv_cnx1: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ → + T1 ≡[h, o] T2. +#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 +/5 width=8 by cnx_tdeq_trans, tdeq_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma new file mode 100644 index 000000000..163f7a109 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cpx_lsubr.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with restricted refinement for local environments *************) + +lemma lsubr_cpxs_trans: ∀h,G. lsub_trans … (cpxs h G) lsubr. +/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma index 64f1facd2..65c32bf7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma @@ -12,21 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts.ma". +include "basic_2/syntax/tsts_tdeq.ma". +include "basic_2/rt_computation/cpxs_lsubr.ma". +include "basic_2/rt_computation/cpxs_cnx.ma". include "basic_2/rt_computation/lfpxs_cpxs.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) (* Forward lemmas with same top term structure ******************************) -(* -lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → T ≂ U. -#h #o #G #L #T #HT #U #H ->(cpxs_inv_cnx1 … H HT) -G -L -T // -qed-. -*) -lemma cpxs_fwd_sort: ∀h,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → - ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. -#h #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * + +lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → + ⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. +#h #o #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * [ #H destruct /2 width=1 by or_introl/ | #n #H destruct @or_intror >iter_S <(iter_n_Sm … (next h)) // (**) @@ -34,9 +31,9 @@ lemma cpxs_fwd_sort: ∀h,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → qed-. (* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → - ⓐV.ⓛ{p}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. -#h #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * +lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → + ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. +#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct @@ -48,52 +45,59 @@ lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U qed-. (* Note: probably this is an inversion lemma *) -lemma cpxs_fwd_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → - ∀V2. ⬆[0, i + 1] V1 ≡ V2 → - ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h, o] U → - #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h, o] U. +(* Basic_2A1: was: cpxs_fwd_delta *) +lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → + ∀V2. ⬆*[⫯i] V1 ≡ V2 → + ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h] U → + #i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h] U. #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H -elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/ +elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/ * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0 -lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct -/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/ +lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct +elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H +<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/ qed-. -lemma cpxs_fwd_theta: ∀h,o,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ⬈*[h, o] U → - ∀V2. ⬆[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨ - ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ⬈*[h, o] U. -#h #o #a #G #L #V1 #V #T #U #H #V2 #HV12 +lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U → + ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨ + ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U. +#h #o #p #G #L #V1 #V #T #U #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * [ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ -| #b #W #T0 #HT0 #HU +| #q #W #T0 #HT0 #HU elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct | #X #HT2 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct + elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) - @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] - /4 width=7 by cpx_zeta, lift_bind, lift_flat/ + @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ] + /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU +| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *) elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V5 #T5 #HV5 #HT5 #H destruct - lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 - /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/ + elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/ | #X #HT1 #H #H0 destruct - elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct - lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by drop_drop/ #HV24 - @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T - @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 - @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ + elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct + elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H + <(lifts_mono … HV34 … H) -V3 -X #HV24 + @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T + @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5 + @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/ ] ] qed-. -lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h, o] U → - ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ⬈*[h, o] U | ⦃G, L⦄ ⊢ W ⬈*[h, o] U. +lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h] U → + ∨∨ ⓝW. T ⩳[h, o] U | ⦃G, L⦄ ⊢ T ⬈*[h] U | ⦃G, L⦄ ⊢ W ⬈*[h] U. #h #o #G #L #W #T #U #H elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * #W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ qed-. + +lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → + ∀U. ⦃G, L⦄ ⊢ T ⬈*[h] U → T ⩳[h, o] U. +/3 width=4 by cpxs_inv_cnx1, tdeq_tsts/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 2cb53faaa..57e422368 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ -cpxs.ma cpxs_tdeq.ma cpxs_drops.ma cpxs_lfpx.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma new file mode 100644 index 000000000..a60e62ada --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/tdeq_tdeq.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". +include "basic_2/rt_transition/cnx.ma". + +(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******) + +(* Advanced properties ******************************************************) + +lemma cnx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ → + ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄. +#h #o #G #L #T1 #HT1 #T2 #HT12 #T #HT2 +elim (tdeq_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0 +lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by tdeq_repl/ (**) (* full auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 67ed58697..e8f5e6cd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,7 +1,7 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma lfpx_lfpx.ma -cnx.ma cnx_simple.ma cnx_drops.ma +cnx.ma cnx_simple.ma cnx_drops.ma cnx_cnx.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma index 9341af67b..aba746929 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_vector.ma @@ -13,18 +13,20 @@ (**************************************************************************) include "basic_2/syntax/term_vector.ma". -include "basic_2/syntax/tsts.ma". +include "basic_2/syntax/tsts_simple.ma". (* SAME TOP TERM STRUCTURE **************************************************) -(* Advanced inversion lemmas ************************************************) - +(* Advanced inversion lemmas with simple (neutral) terms ********************) +(* (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) -lemma tsts_inv_bind_applv_simple: ∀p,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{p,I}V2.T2 → +(* Basic_2A1: was: tsts_inv_bind_applv_simple *) +lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥. -#p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H +#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize [ #H destruct #H /2 width=5 by simple_inv_bind/ | #V #Vs #_ #H destruct ] 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 20b1e11d6..305dbb057 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 @@ -111,12 +111,12 @@ table { [ { "uncounted context-sensitive rt-transition" * } { (* [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -142,7 +142,7 @@ table { } ] [ { "uncounted context-sensitive rt-transition" * } { - [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ] + [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" *+ "cnx_cnx" ] [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] } @@ -240,12 +240,12 @@ table { [ "append ( ? @@ ? )" "append_length" * ] } ] - [ { "degree-based equivalence for terms" * } { - [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ] + [ { "same top term structure" * } { + [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_vector" * ] } ] - [ { "same top term structure" * } { - [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ] + [ { "degree-based equivalence for terms" * } { + [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ] } ] [ { "closures" * } { diff --git a/matita/matita/contribs/lambdadelta/partial_compile.sh b/matita/matita/contribs/lambdadelta/partial_compile.sh index 319fa8704..61fb60662 100644 --- a/matita/matita/contribs/lambdadelta/partial_compile.sh +++ b/matita/matita/contribs/lambdadelta/partial_compile.sh @@ -1,3 +1,4 @@ +../../matitac.opt `cat partial.txt` cd basic_2/rt_transition/ ../../../../matitac.opt `cat partial.txt` cd ../rt_computation/ -- 2.39.2