From be2870b722324a1813ac9e72ebcb2cda6c8733d7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 2 Nov 2017 17:34:36 +0000 Subject: [PATCH] - exclusion binder in local environments the update is now complete, after bugs fixed in lfdeq.ma - minor corrections --- matita/matita/contribs/lambdadelta/Makefile | 8 +++---- .../lfpxs_fqus.ma => etc/lpxs/lpxs_fqus.etc} | 20 ++++++++++++++++ .../basic_2/rt_computation/csx_csx.ma | 8 +++---- .../basic_2/rt_computation/csx_csx_vector.ma | 2 +- .../{csx_fpbs.ma => fpbs_csx.ma} | 0 .../basic_2/rt_computation/lfsx.ma | 8 +++---- .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/static/lfdeq.ma | 24 +++++++++---------- .../lambdadelta/basic_2/web/basic_2_src.tbl | 13 +++------- 9 files changed, 49 insertions(+), 36 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_fqus.ma => etc/lpxs/lpxs_fqus.etc} (85%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_fpbs.ma => fpbs_csx.ma} (100%) diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e0817c219..6bb435082 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -204,20 +204,20 @@ define SUMMARY_TEMPLATE @printf ' SUMMARY $(1)\n' @printf 'name "$$(basename $$(@F))"\n\n' > $$@ @printf 'table {\n' >> $$@ - @printf ' class "gray" [ "category"\n' >> $$@ + @printf ' class "gray" [ "category"\n' >> $$@ @printf ' [ "objects" * ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "water" [ "sizes"\n' >> $$@ + @printf ' class "water" [ "sizes"\n' >> $$@ @printf ' [ "files" "$$(S1)" ]\n' >> $$@ @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "grass" [ "propositions"\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ @printf ' [ "total" "$$(P3)" ]\n' >> $$@ @printf ' ]\n' >> $$@ - @printf ' class "yellow" [ "concepts"\n' >> $$@ + @printf ' class "grass" [ "concepts"\n' >> $$@ @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ @printf ' [ "total" "$$(C3)" ]\n' >> $$@ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc similarity index 85% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc index dd559526f..cfe64e5ae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_fqus.etc @@ -1,3 +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/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + + + (* Properties on supclosure *************************************************) lemma lpx_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index b675ddec7..a0f48f828 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -52,8 +52,8 @@ qed. (* Basic_1: was just: sn3_abbr *) (* Basic_2A1: was: csx_lref_bind *) -lemma csx_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → - ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄. +lemma csx_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄. #h #o #I #G #L #K #V #i #HLK #HV @csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H [ #H destruct elim Hi // @@ -67,8 +67,8 @@ qed. (* Basic_1: was: sn3_gen_def *) (* Basic_2A1: was: csx_inv_lref_bind *) -lemma csx_inv_lref_drops: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → - ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. +lemma csx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ → ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄. #h #o #I #G #L #K #V #i #HLK #Hi elim (lifts_total V (𝐔❴⫯i❵)) /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index fa81a32d2..c010a31a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -41,7 +41,7 @@ lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⬆*[⫯i] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄. #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=11 by csx_inv_lifts, csx_lref_drops, drops_isuni_fwd_drop2/ +[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 24fa630b6..14c939fac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -51,8 +51,8 @@ lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H * [ #H1 #H2 destruct // -| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct - /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/ +| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort, frees_inv_sort/ ] qed. @@ -61,8 +61,8 @@ lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H * [ #H1 #H2 destruct // -| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct - /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/ +| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref, frees_inv_gref/ ] 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 33d4cf482..1e49546fd 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_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 2d219c5ce..2d86a95a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -94,25 +94,25 @@ lemma lfdeq_atom: ∀h,o,I. ⋆ ≡[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. (* Basic_2A1: uses: lleq_sort *) -lemma lfdeq_sort: ∀h,o,I,L1,L2,V1,V2,s. - L1 ≡[h, o, ⋆s] L2 → L1.ⓑ{I}V1 ≡[h, o, ⋆s] L2.ⓑ{I}V2. +lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s. + L1 ≡[h, o, ⋆s] L2 → L1.ⓘ{I1} ≡[h, o, ⋆s] L2.ⓘ{I2}. /2 width=1 by lfxs_sort/ qed. -lemma lfdeq_pair: ∀h,o,I,L1,L2,V. - L1 ≡[h, o, V] L2 → L1.ⓑ{I}V ≡[h, o, #0] L2.ⓑ{I}V. +lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 → V1 ≡[h, o] V2 → + L1.ⓑ{I}V1 ≡[h, o, #0] L2.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. - +(* lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 → L1.ⓤ{I} ≡[h, o, #0] L2.ⓤ{I}. /2 width=3 by lfxs_unit/ qed. - -lemma lfdeq_lref: ∀h,o,I,L1,L2,V1,V2,i. - L1 ≡[h, o, #i] L2 → L1.ⓑ{I}V1 ≡[h, o, #⫯i] L2.ⓑ{I}V2. +*) +lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i. + L1 ≡[h, o, #i] L2 → L1.ⓘ{I1} ≡[h, o, #⫯i] L2.ⓘ{I2}. /2 width=1 by lfxs_lref/ qed. (* Basic_2A1: uses: lleq_gref *) -lemma lfdeq_gref: ∀h,o,I,L1,L2,V1,V2,l. - L1 ≡[h, o, §l] L2 → L1.ⓑ{I}V1 ≡[h, o, §l] L2.ⓑ{I}V2. +lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l. + L1 ≡[h, o, §l] L2 → L1.ⓘ{I1} ≡[h, o, §l] L2.ⓘ{I2}. /2 width=1 by lfxs_gref/ qed. lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term. @@ -128,7 +128,7 @@ lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆. lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. - +(* lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ | ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & @@ -138,7 +138,7 @@ lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → #h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. - +*) lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I1,I2,L1,L2. L1 ≡[h, o, #i] L2 & 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 2123e5fd9..8b1cc6982 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 @@ -88,9 +88,8 @@ table { ] [ { "strongly normalizing rt-computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] - [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_theq_vector" + "csx_aaa" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] + [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] + [ "csx_lleq" + "csx_lpxs" + "csx_fpbs" * ] } ] [ { "parallel qrst-computation" * } { @@ -109,15 +108,9 @@ table { ] *) [ { "uncounted context-sensitive rt-computation" * } { -(* - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] -*) -(* [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] -*) + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } -- 2.39.2