From 2f20aaf586f7cb4fd2933d765f4d09fcf077e4c5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 12 May 2018 18:44:43 +0200 Subject: [PATCH] update in basic_2 + moreresults on cpms and cprs --- .../basic_2/relocation/drops_ltc.ma | 95 +++++++++++++++++++ .../basic_2/rt_computation/cpms_drops.ma | 82 ++++++++++++++++ .../basic_2/rt_computation/cprs.ma | 2 +- .../{scpds_lift.ma => cprs_drops.ma} | 32 +++---- .../basic_2/rt_computation/cprs_lift.ma | 60 ------------ .../basic_2/rt_computation/partial.txt | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 7 files changed, 197 insertions(+), 84 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{scpds_lift.ma => cprs_drops.ma} (54%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma new file mode 100644 index 000000000..3f999a5b2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/lib/ltc.ma". +include "basic_2/relocation/lreq_lreq.ma". + +(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) + +(* Properties with labeled transitive closure *******************************) + +lemma d2_liftable_sn_ltc: ∀A,f. associative … f → + ∀C,S,R. (∀n. d_liftable2_sn C S (λL. R L n)) → + ∀n. d_liftable2_sn C S (λL. ltc A f … (R L) n). +#A #g #Hg #C #S #R #HR #n #K #T1 #T2 #H +@(ltc_ind_dx … Hg ???? H) -n -T2 +[ #n #T2 #HT12 #b #g #L #HLK #U1 #HTU1 + elim (HR … HT12 … HLK … HTU1) -b -K -T1 -HR + /3 width=3 by ltc_rc, ex2_intro/ +| #n1 #n2 #T #T2 #_ #IHT1 #HT2 #b #f #L #HLK #U1 #HTU1 + elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1 + elim (HR … HT2 … HLK … HTU) -HR -K -T + /3 width=5 by ltc_dx, ex2_intro/ +] +qed-. + +lemma d2_deliftable_sn_ltc: ∀A,f. associative … f → + ∀C,S,R. (∀n. d_deliftable2_sn C S (λL. R L n)) → + ∀n. d_deliftable2_sn C S (λL. ltc A f … (R L) n). +#A #g #Hg #C #S #R #HR #n #L #U1 #U2 #H +@(ltc_ind_dx … Hg ???? H) -n -U2 +[ #n #U2 #HU12 #b #g #K #HLK #T1 #HTU1 + elim (HR … HU12 … HLK … HTU1) -b -L -U1 -HR + /3 width=3 by ltc_rc, ex2_intro/ +| #n1 #n2 #U #U2 #_ #IHU1 #HU2 #b #f #K #HLK #T1 #HTU1 + elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 + elim (HR … HU2 … HLK … HTU) -L -U -HR + /3 width=5 by ltc_dx, ex2_intro/ +] +qed-. + +lemma co_dropable_sn_ltc: ∀A,f. associative … f → + ∀R. (∀n. co_dropable_sn (λL. R L n)) → + ∀n. co_dropable_sn (λL. ltc A f … (R L) n). +#A #g #Hg #R #HR #n #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H +@(ltc_ind_dx … Hg ???? H) -n -L2 +[ #n #L2 #HL12 #g1 #H + elim (HR … HLK1 … Hf … HL12 … H) -f2 -L1 -HR -Hf + /3 width=3 by ltc_rc, ex2_intro/ +| #n1 #n2 #L #L2 #_ #IH #HL2 #f1 #H + elim (IH … H) -IH #K #HK1 #HLK + elim (HR … HLK … HL2 … H) -f2 -L -HR + /3 width=3 by ltc_dx, ex2_intro/ +] +qed-. + +lemma co_dropable_dx_ltc: ∀A,f. associative … f → + ∀R. (∀n. co_dropable_dx (λL. R L n)) → + ∀n. co_dropable_dx (λL. ltc A f … (R L) n). +#A #g #Hg #R #HR #n #f2 #L1 #L2 #H +@(ltc_ind_dx … Hg ???? H) -n -L2 +[ #n #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 + elim (HR … HL12 … HLK2 … Hf … Hf2) -f2 -L2 -HR -Hf + /3 width=3 by ltc_rc, ex2_intro/ +| #n1 #n2 #L #L2 #_ #IHL1 #HL2 #b #f #K2 #HLK2 #Hf #f1 #Hf2 + elim (HR … HL2 … HLK2 … Hf … Hf2) -L2 -HR #K #HLK #HK2 + elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L + /3 width=5 by ltc_dx, ex2_intro/ +] +qed-. + +lemma co_dedropable_sn_ltc: ∀A,f. associative … f → + ∀R. (∀n. co_dedropable_sn (λL. R L n)) → + ∀n. co_dedropable_sn (λL. ltc A f … (R L) n). +#A #g #Hg #R #HR #n #b #f #L1 #K1 #HLK1 #f1 #K2 #H +@(ltc_ind_dx … Hg ???? H) -n -K2 +[ #n #K2 #HK12 #f2 #Hf + elim (HR … HLK1 … HK12 … Hf) -f1 -K1 -HR + /3 width=4 by ltc_rc, ex3_intro/ +| #n1 #n2 #K #K2 #_ #IH #HK2 #f2 #Hf + elim (IH … Hf) -K1 -IH #L #H1L1 #HLK #H2L1 + elim (HR … HLK … HK2 … Hf) -f1 -K -HR + /3 width=6 by lreq_trans, ltc_dx, ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma new file mode 100644 index 000000000..b719f52b5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops_ltc.ma". +include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Advanced properties ******************************************************) + +(* Note: apparently this was missing in basic_1 *) +(* Basic_2A1: uses: cprs_delta *) +lemma cpms_delta_drops (n) (h) (G): + ∀L,K,V,i. ⬇*[i] L ≘ K.ⓓV → + ∀V2. ⦃G, K⦄ ⊢ V ➡*[n, h] V2 → + ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡*[n, h] W2. +#n #h #G #L #K #V #i #HLK #V2 #H @(cpms_ind_dx … H) -V2 +[ /3 width=6 by cpm_cpms, cpm_delta_drops/ +| #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2 + lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK + elim (lifts_total V1 (𝐔❴↑i❵)) #W1 #HVW1 + /3 width=11 by cpm_lifts_bi, cpms_step_dx/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cpms_inv_lref1_drops (n) (h) (G): + ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[n, h] T2 → + ∨∨ ∧∧ T2 = #i & n = 0 + | ∃∃K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡*[n, h] V2 & + ⬆*[↑i] V2 ≘ T2 + | ∃∃m,K,V,V2. ⬇*[i] L ≘ K.ⓛV & ⦃G, K⦄ ⊢ V ➡*[m, h] V2 & + ⬆*[↑i] V2 ≘ T2 & n = ↑m. +#n #h #G #L #T2 #i #H @(cpms_ind_dx … H) -T2 +[ /3 width=1 by or3_intro0, conj/ +| #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH * + [ #H1 #H2 destruct + elim (cpm_inv_lref1_drops … HT2) -HT2 * + [ /3 width=1 by or3_intro0, conj/ + | /4 width=6 by cpm_cpms, or3_intro1, ex3_3_intro/ + | /4 width=8 by cpm_cpms, or3_intro2, ex4_4_intro/ + ] + | #K #V0 #V #HLK #HV0 #HVT + lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK + elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T + /4 width=6 by cpms_step_dx, ex3_3_intro, or3_intro1/ + | #m #K #V0 #V #HLK #HV0 #HVT #H destruct + lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK + elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T + /4 width=8 by cpms_step_dx, ex4_4_intro, or3_intro2/ + ] +] +qed-. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: uses: scpds_lift *) +(* Basic_2A1: includes: cprs_lift *) +(* Basic_1: includes: pr3_lift *) +lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n). +/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: uses: scpds_inv_lift1 *) +(* Basic_2A1: includes: cprs_inv_lift1 *) +(* Basic_1: includes: pr3_gen_lift *) +lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n). +/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma index e26838e19..36d7644e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma @@ -15,7 +15,7 @@ include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_computation/cpms.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION FOR TERMS *************************) +(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************) (* Basic eliminators ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma similarity index 54% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma index 0a2181adb..19829738f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_drops.ma @@ -12,25 +12,21 @@ (* *) (**************************************************************************) -include "basic_2/static/da_lift.ma". -include "basic_2/unfold/lstas_lift.ma". -include "basic_2/computation/cprs_lift.ma". -include "basic_2/computation/scpds.ma". +include "basic_2/rt_computation/cpms_drops.ma". -(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) +(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************) -(* Relocation properties ****************************************************) +(* Advanced inversion lemmas ************************************************) -lemma scpds_lift: ∀h,o,G,d. d_liftable (scpds h o d G). -#h #o #G #d2 #K #T1 #T2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L #b #l #k -elim (lift_total T l k) -/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/ -qed. - -lemma scpds_inv_lift1: ∀h,o,G,d. d_deliftable_sn (scpds h o d G). -#h #o #G #d2 #L #U1 #U2 * #U #d1 #Hd21 #Hd1 #HU1 #HU2 #K #b #l #k #HLK #T1 #HTU1 -lapply (da_inv_lift … Hd1 … HLK … HTU1) -Hd1 #Hd1 -elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 -elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L -/3 width=8 by ex4_2_intro, ex2_intro/ +(* Basic_1: was: pr3_gen_lref *) +(* Basic_2A1: was: cprs_inv_lref1 *) +lemma cprs_inv_lref1_drops (h) (G): ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h] T2 → + ∨∨ T2 = #i + | ∃∃K,V1,T1. ⬇*[i] L ≘ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡*[h] T1 & + ⬆*[↑i] T1 ≘ T2. +#h #G #L #T2 #i #H elim (cpms_inv_lref1_drops … H) -H * +[ /2 width=1 by or_introl/ +| /3 width=6 by ex3_3_intro, or_intror/ +| #m #K #V #V2 #_ #_ #_ #H destruct +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma deleted file mode 100644 index 7a49ed3c6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma +++ /dev/null @@ -1,60 +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/cpr_lift.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Advanced properties ******************************************************) - -(* Note: apparently this was missing in basic_1 *) -lemma cprs_delta: ∀G,L,K,V,V2,i. - ⬇[i] L ≘ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 → - ∀W2. ⬆[0, i + 1] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡* W2. -#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6 by cpr_cprs, cpr_delta/ ] -#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 -lapply (drop_fwd_drop2 … HLK) -HLK #HLK -elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/ -qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was: pr3_gen_lref *) -lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 → - T2 = #i ∨ - ∃∃K,V1,T1. ⬇[i] L ≘ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 & - ⬆[0, i + 1] T1 ≘ T2. -#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1 by or_introl/ -#T #T2 #_ #HT2 * -[ #H destruct - elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ - * /4 width=6 by cpr_cprs, ex3_3_intro, or_intror/ -| * #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (drop_fwd_drop2 … HLK) #H0LK - elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T - /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/ -] -qed-. - -(* Relocation properties ****************************************************) - -(* Basic_1: was: pr3_lift *) -lemma cprs_lift: ∀G. d_liftable (cprs G). -/3 width=10 by d_liftable_CTC, cpr_lift/ qed. - -(* Basic_1: was: pr3_gen_lift *) -lemma cprs_inv_lift1: ∀G. d_deliftable_sn (cprs G). -/3 width=6 by d_deliftable_sn_CTC, cpr_inv_lift1/ -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 163c752ff..a91bb543e 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 -cprs.ma +cpms.ma cpms_drops.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 3fe65458a..8f938be4f 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 @@ -78,11 +78,11 @@ table { (* [ [ "" ] "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ] *) - [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" (* "cprs_lift" + "cprs_cprs" *) * ] + [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_drops" (* + "cprs_cprs" *) * ] } ] [ { "t-bound context-sensitive parallel rt-computation" * } { - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { @@ -202,7 +202,7 @@ table { class "orange" [ { "relocation" * } { [ { "generic slicing" * } { - [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] + [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] } ] [ { "generic relocation" * } { -- 2.39.2