From 258d2e384e8bf7008d2fb01c7d3fee5126d65120 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 12 May 2018 22:42:14 +0200 Subject: [PATCH] update in ground_2 and basic_2 + more results on cpms --- .../cprs_etc.ma => etc/cprs/cprs.etc} | 4 --- .../lambdadelta/basic_2/etc/cpxs/cpxs.etc | 5 ---- .../{cprs_aaa.ma => cpms_aaa.ma} | 20 ++++++-------- .../basic_2/rt_computation/cpms_cpxs.ma | 27 +++++++++++++++++++ .../{scpds_aaa.ma => cpms_lsubr.ma} | 16 +++++------ .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +-- .../contribs/lambdadelta/ground_2/lib/ltc.ma | 10 +++++++ 8 files changed, 56 insertions(+), 32 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/cprs_etc.ma => etc/cprs/cprs.etc} (78%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cprs_aaa.ma => cpms_aaa.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{scpds_aaa.ma => cpms_lsubr.ma} (71%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc similarity index 78% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc index 254261657..a51dba5d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc @@ -1,7 +1,3 @@ -lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr. -/3 width=5 by lsubr_cpr_trans, CTC_lsub_trans/ -qed-. - (* Basic_1: was: pr3_pr1 *) lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. /2 width=3 by lsubr_cprs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc deleted file mode 100644 index 920d114f5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc +++ /dev/null @@ -1,5 +0,0 @@ - -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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma index 2266edbad..f4fdb524f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma @@ -12,18 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_aaa.ma". -include "basic_2/computation/cpxs.ma". +include "basic_2/rt_computation/cpxs_aaa.ma". +include "basic_2/rt_computation/cpms_cpxs.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) -(* Properties about atomic arity assignment on terms ************************) +(* Properties with atomic arity assignment on terms *************************) -lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -#h #o #G #L #T1 #A #HT1 #T2 #HT12 -@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/ -qed-. - -lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. -/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-. +(* Basic_2A1: uses: scpds_aaa_conf *) +(* Basic_2A1: includes: cprs_aaa_conf *) +lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n). +/3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma new file mode 100644 index 000000000..9d07288c3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpm_cpx.ma". +include "basic_2/rt_computation/cpxs.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Forward lemmas with unbound context-sensitive rt-computation for terms ***) + +(* Basic_2A1: includes: cprs_cpxs *) +lemma cpms_fwd_cpxs (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. +#n #h #G #L #T1 #T2 #H @(cpms_ind_dx … H) -T2 +/3 width=4 by cpxs_strap1, cpm_fwd_cpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lsubr.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lsubr.ma index eef78441b..300e2eff0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lsubr.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lstas_aaa.ma". -include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/scpds.ma". +include "basic_2/rt_transition/cpm_lsubr.ma". +include "basic_2/rt_computation/cpms.ma". -(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) -(* Properties on atomic arity assignment for terms **************************) +(* Properties with restricted refinement for local environments *************) -lemma scpds_aaa_conf: ∀h,o,G,L,d. Conf3 … (aaa G L) (scpds h o d G L). -#h #o #G #L #d #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/ -qed. +(* Basic_2A1: uses: lsubr_cprs_trans *) +lemma lsubr_cpms_trans (n) (h): ∀G. lsub_trans … (λL. cpms h G L n) lsubr. +/3 width=5 by lsubr_cpm_trans, ltc_lsub_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 a91bb543e..be67912d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -9,5 +9,5 @@ lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma -cpms.ma cpms_drops.ma +cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_cpxs.ma cprs.ma cprs_drops.ma 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 8f938be4f..e5ec82baf 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 @@ -70,7 +70,7 @@ table { [ { "rt-computation" * } { (* [ { "decomposed rt-computation" * } { - [ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ] + "scpds_scpds" } ] *) @@ -82,7 +82,7 @@ table { } ] [ { "t-bound context-sensitive parallel rt-computation" * } { - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_aaa" + "cpms_cpxs" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma index 4bfd5c7c7..e5ea2770d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma @@ -77,3 +77,13 @@ lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1): @(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12 >(H2f a) -H2f /3 width=4 by ltc_rc/ qed-. + +(* Properties with lsub *****************************************************) + +lemma ltc_lsub_trans: ∀A,f. associative … f → + ∀B,C,R,S. (∀n. lsub_trans B C (λL. R L n) S) → + ∀n. lsub_trans B C (λL. ltc A f … (R L) n) S. +#A #f #Hf #B #C #R #S #HRS #n #L2 #T1 #T2 #H +@(ltc_ind_dx … Hf ???? H) -n -T2 +/3 width=5 by ltc_dx, ltc_rc/ +qed-. -- 2.39.2