From: Ferruccio Guidi Date: Sat, 12 May 2018 20:42:14 +0000 (+0200) Subject: update in ground_2 and basic_2 X-Git-Tag: make_still_working~319 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=258d2e384e8bf7008d2fb01c7d3fee5126d65120 update in ground_2 and basic_2 + more results on cpms --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc new file mode 100644 index 000000000..a51dba5d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc @@ -0,0 +1,10 @@ +(* 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. + +(* Basic_1: was: nf2_pr3_unfold *) +lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U. +#G #L #T #U #H @(cprs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ +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/cpms_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma new file mode 100644 index 000000000..f4fdb524f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/cpxs_aaa.ma". +include "basic_2/rt_computation/cpms_cpxs.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Properties with atomic arity assignment on terms *************************) + +(* 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/cpms_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lsubr.ma new file mode 100644 index 000000000..300e2eff0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lsubr.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lsubr.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Properties with restricted refinement for local environments *************) + +(* 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/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma deleted file mode 100644 index 2266edbad..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reduction/lpx_aaa.ma". -include "basic_2/computation/cpxs.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) - -(* Properties about 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma deleted file mode 100644 index 254261657..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_etc.ma +++ /dev/null @@ -1,14 +0,0 @@ -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. - -(* Basic_1: was: nf2_pr3_unfold *) -lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U. -#G #L #T #U #H @(cprs_ind_dx … H) -T // -#T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ -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/rt_computation/scpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma deleted file mode 100644 index eef78441b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_aaa.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/unfold/lstas_aaa.ma". -include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/scpds.ma". - -(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) - -(* Properties on atomic arity assignment for terms **************************) - -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. 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-.