From 9d5724b7a571ce0da2a2691e639f044430f4a73a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 8 Mar 2018 18:40:47 +0100 Subject: [PATCH] update in basic_2 + yet anothe equivalent of lfsx to be used in lfsx_pair_lpxs --- .../lambdadelta/basic_2/etc/lfxs_lex.etc | 12 +++++ .../basic_2/rt_computation/lfsx_lpx.ma | 44 +++++++++++++++++++ .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpx_lpx.ma | 30 +++++++++++++ .../lambdadelta/basic_2/static/lfxs_lex.ma | 17 ++++++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- 6 files changed, 105 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc new file mode 100644 index 000000000..6303d64ec --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs_lex.etc @@ -0,0 +1,12 @@ +(* Note: this is the companion of lfxs_trans_fsle *) +theorem lfxs_trans_fsge: ∀R,R1,R2,R3. + lfxs_transitive_next R1 R R3 → + ∀L1,L,T. L1 ⪤*[R1, T] L → + ∀L2. L ⪤[R2] L2 → L1 ⪤*[R3, T] L2. +#R #R1 #R2 #R3 #HR #L1 #L #T #H +cases H -H #f1 #Hf1 #HL1 #L2 * #f #Hf #HL2 +@(ex2_intro … Hf1) -Hf1 +@(lexs_trans_gen … HL1) -HL1 +[5: @(sle_lexs_conf … HL2) -HL2 /2 width=1 by sle_isid_sn/ |1,2: skip +|4: // +|3: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma new file mode 100644 index 000000000..3fa42466e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.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_transition/lfpx_lpx.ma". +include "basic_2/rt_computation/lfsx_lfsx.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +(* Properties with uncounted rt-transition **********************************) + +lemma lfsx_intro_lpx: ∀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 #L2 #H +elim (lfpx_inv_lpx_lfeq … H) -H +/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfeq_lfdeq/ +qed-. + +lemma lfsx_lpx_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_lfpx_trans, lfpx_lpx/ qed-. + +(* Eliminators with uncounted rt-transition *********************************) + +lemma lfsx_ind_lpx: ∀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, lfpx_lpx/ 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 8bd713ca3..d730cd54f 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_lpxs.ma lfsx_lfpxs.ma lfsx_lfsx.ma +lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.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/rt_transition/lfpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma new file mode 100644 index 000000000..034ce9c7e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfxs_lex.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". +include "basic_2/rt_transition/lpx.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Properties with uncounted parallel rt-transition for local environments **) + +lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2. +/2 width=1 by lfxs_lex/ qed. + +(* Inversion lemmas with uncounted parallel rt-transition for local envs ****) + +lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2. +/3 width=3 by lfpx_fsge_comp, lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma index 11b3ca476..01f578f4e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/relocation/lex.ma". -include "basic_2/static/lfxs_fqup.ma". +include "basic_2/static/lfxs_fsle.ma". +include "basic_2/static/lfeq.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -24,3 +25,17 @@ lemma lfxs_lex: ∀R,L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤*[R, T] L2. elim (frees_total L1 T) #g #Hg /4 width=5 by lexs_sdj, sdj_isid_sn, ex2_intro/ qed. + +(* Inversion lemmas with generic extension of a context sensitive relation **) + +lemma lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → + lfxs_fsge_compatible R → + ∀L1,L2,T. L1 ⪤*[R, T] L2 → + ∃∃L. L1 ⪤[R] L & L ≡[T] L2. +#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL +elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL +[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R +lapply (lexs_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H +elim (frees_lexs_conf … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01 +/4 width=7 by sle_lexs_trans, (* 2x *) ex2_intro/ +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 f35756078..8ea1a603f 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_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "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" * ] @@ -138,7 +138,7 @@ table { ] [ { "uncounted context-sensitive parallel rt-transition" * } { [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] + [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ] -- 2.39.2