From e8971d3db8935436e6dddc27fe1ae168c7f3b315 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Mar 2018 00:41:50 +0100 Subject: [PATCH] update in basic_2 + new equivalent of lfsx opens the road to lfsx_pair_lpxs + minor corrections --- .../basic_2/rt_computation/lfpxs_lpxs.ma | 7 ++- .../basic_2/rt_computation/lfsx_lpxs.ma | 44 +++++++++++++++++++ .../basic_2/rt_computation/lsubsx_lfsx.ma | 9 ++++ .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/static/lfdeq_lfeq.ma | 23 ++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- 6 files changed, 84 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma index fa56ac09c..746bc369e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -22,12 +22,15 @@ include "basic_2/rt_computation/lfpxs.ma". (* Properties with uncounted parallel rt-computation for local environments *) +lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=1 by tc_lfxs_lex/ qed. + lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. /2 width=3 by tc_lfxs_lex_lfeq/ qed. (* Inversion lemmas with uncounted parallel rt-computation for local envs ***) -lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. +lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. /3 width=5 by lfpx_fsle_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma new file mode 100644 index 000000000..8c8bd5a54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfdeq_lfeq.ma". +include "basic_2/rt_computation/lfpxs_lpxs.ma". +include "basic_2/rt_computation/lfsx_lfpxs.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +(* Properties with uncounted rt-computation *********************************) + +lemma lfsx_intro_lpxs: ∀h,o,G,L1,T. + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. +#h #o #G #L1 #T #HT +@lfsx_intro_lfpxs #L2 #H +elim (lfpxs_inv_lpxs_lfeq … H) -H +/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfeq_lfdeq/ +qed-. + +lemma lfsx_lpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +/3 width=3 by lfsx_lfpxs_trans, lfpxs_lpxs/ qed-. + +(* Eliminators with uncounted rt-computation ********************************) + +lemma lfsx_ind_lpxs: ∀h,o,G,T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. +/5 width=6 by lfsx_ind_lfpxs, lfpxs_lpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma index 4ef9cf962..059cb1ece 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma @@ -62,3 +62,12 @@ qed-. lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. /3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-. + +(* Properties with strong normalizing env's for uncounted rt-computation ****) + +lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. +#h #o #G #L #T1 #T2 #H +@(cpxs_ind_dx ???????? H) -T1 // +/3 width=3 by lfsx_cpx_trans/ +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 6b53efa07..8bd713ca3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -4,5 +4,5 @@ lpxs.ma lpxs_length.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma +lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma new file mode 100644 index 000000000..41b2c033e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfeq.ma". +include "basic_2/static/lfdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) + +(* Properties with syntactic equivalence on referred entries ****************) + +lemma lfeq_lfdeq: ∀h,o,L1,L2,T. L1 ≡[T] L2 → L1 ≛[h, o, T] L2. +/2 width=3 by lfxs_co/ 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 3f4cb8fbf..3a40bb09a 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 @@ -108,7 +108,7 @@ table { *) [ { "uncounted context-sensitive parallel rt-computation" * } { [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] - [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] @@ -173,7 +173,7 @@ table { ] [ { "degree-based equivalence" * } { [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] + [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfeq" + "lfdeq_lfdeq" * ] } ] [ { "syntactic equivalence" * } { -- 2.39.2