From 8f5533bd34e93eee2a14cdcfd0595be65651bfa7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 31 May 2018 00:36:31 +0200 Subject: [PATCH] update in basic_2 + lprs started ... --- .../basic_2/rt_computation/cpms_lpr.ma | 75 ++++++++++++++++ .../basic_2/rt_computation/cprs_cprs.ma | 33 ------- .../basic_2/rt_computation/lprs.ma | 67 +++++--------- .../basic_2/rt_computation/lprs_length.ma | 23 +++++ .../basic_2/rt_computation/lprs_lpr.ma | 48 ++++++++++ .../basic_2/rt_computation/partial.txt | 1 + .../lambdadelta/basic_2/rt_transition/cpm.ma | 89 +++++++++++++++++++ 7 files changed, 257 insertions(+), 79 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_length.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma new file mode 100644 index 000000000..f572acf67 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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/star.ma". +include "basic_2/rt_transition/lpr.ma". +include "basic_2/rt_computation/cpms.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Properties concerning sn parallel reduction on local environments ********) + +(* Basic_1: uses: pr3_pr2_pr2_t *) +(* Basic_1: includes: pr3_pr0_pr2_t *) +(* Basic_2A1: uses: lpr_cpr_trans *) +lemma lpr_cpm_trans (n) (h) (G): s_r_transitive … (λL. cpm h G L n) (λ_. lpr h G). +#n #h #G #L2 #T1 #T2 #H @(cpm_ind … H) -G -L2 -T1 -T2 +[ /2 width=3 by/ +| /3 width=2 by cpx_cpxs, cpx_ess/ +| #I #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H + elim (lpx_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct + /4 width=3 by cpxs_delta, cpxs_strap2/ +| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H + elim (lpx_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct + /4 width=3 by cpxs_lref, cpxs_strap2/ +|5,10: /4 width=1 by cpxs_beta, cpxs_bind, lpx_bind_refl_dx/ +|6,8,9: /3 width=1 by cpxs_flat, cpxs_ee, cpxs_eps/ +| /4 width=3 by cpxs_zeta, lpx_bind_refl_dx/ +| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_bind_refl_dx/ +] +qed-. + + + + + + + +#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 +[ /2 width=3 by/ +| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 + elim (lpr_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + /4 width=6 by cprs_strap2, cprs_delta/ +|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/ +|4,6: /3 width=1 by cprs_flat, cprs_eps/ +|5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/ +] +qed-. + +lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +/4 width=5 by lpr_cpr_trans, cprs_bind_dx, lpr_pair/ qed. + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) +lemma lpr_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lpr G). +#G @b_c_trans_CTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *) +qed-. + +lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +/4 width=5 by lpr_cprs_trans, cprs_bind_dx, lpr_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma index 76e2da87e..e69c6b8d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma @@ -100,34 +100,6 @@ lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → ] qed-. -(* Properties concerning sn parallel reduction on local environments ********) - -(* Basic_1: was just: pr3_pr2_pr2_t *) -(* Basic_1: includes: pr3_pr0_pr2_t *) -lemma lpr_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lpr G). -#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 -[ /2 width=3 by/ -| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (lpr_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct - /4 width=6 by cprs_strap2, cprs_delta/ -|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/ -|4,6: /3 width=1 by cprs_flat, cprs_eps/ -|5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/ -] -qed-. - -lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -/4 width=5 by lpr_cpr_trans, cprs_bind_dx, lpr_pair/ qed. - -(* Advanced properties ******************************************************) - -(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) -lemma lpr_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lpr G). -#G @b_c_trans_CTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *) -qed-. - (* Basic_1: was: pr3_strip *) (* Basic_1: includes: pr1_strip *) lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L). @@ -148,8 +120,3 @@ lemma cprs_lpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → #G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 /3 width=3 by lpr_cprs_trans, ex2_intro/ qed-. - -lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -/4 width=5 by lpr_cprs_trans, cprs_bind_dx, lpr_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma index 4bc12d246..02f4a101c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma @@ -12,60 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsnstar_3.ma". -include "basic_2/substitution/lpx_sn_tc.ma". -include "basic_2/reduction/lpr.ma". +include "basic_2/notation/relations/predsnstar_4.ma". +include "basic_2/relocation/lex.ma". +include "basic_2/rt_computation/cpms.ma". -(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) -definition lprs: relation3 genv lenv lenv ≝ - λG. TC … (lpr G). +definition lprs (h) (G): relation lenv ≝ + lex (λL.cpms h G L 0). -interpretation "parallel computation (local environment, sn variant)" - 'PRedSnStar G L1 L2 = (lprs G L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lprs_ind: ∀G,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L2. -#G #L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lprs_ind_dx: ∀G,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ➡* L2 → R L1. -#G #L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. +interpretation + "parallel r-computation on all entries (local environment)" + 'PRedSnStar h G L1 L2 = (lprs h G L1 L2). (* Basic properties *********************************************************) -lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2. -/2 width=1 by inj/ qed. - -lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L. -/2 width=1 by lpr_lprs/ qed. +lemma lprs_refl (h) (G): ∀L. ⦃G, L⦄ ⊢ ➡*[h] L. +/2 width=1 by lex_refl/ qed. -lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2. -/2 width=3 by step/ qed-. - -lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2. -/2 width=3 by TC_strap/ qed-. - -lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V. -/2 width=1 by TC_lpx_sn_pair_refl/ qed. +(* Basic_2A1: uses: lprs_pair_refl *) +lemma lprs_bind_refl_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → + ∀I. ⦃G, L1.ⓘ{I}⦄ ⊢ ➡*[h] L2.ⓘ{I}. +/2 width=1 by lex_bind_refl_dx/ qed. (* Basic inversion lemmas ***************************************************) -lemma lprs_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡* L2 → L2 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. - -lemma lprs_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡* ⋆ → L1 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. - -(* Basic forward lemmas *****************************************************) +(* Basic_2A1: uses: lprs_inv_atom1 *) +lemma lprs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ➡*[h] L2 → L2 = ⋆. +/2 width=2 by lex_inv_atom_sn/ qed-. -lemma lprs_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → |L1| = |L2|. -/2 width=2 by TC_lpx_sn_fwd_length/ qed-. +(* Basic_2A1: uses: lprs_inv_atom2 *) +lemma lprs_inv_atom_dx (h) (G): ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] ⋆ → L1 = ⋆. +/2 width=2 by lex_inv_atom_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_length.ma new file mode 100644 index 000000000..a488b1a3f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_length.ma @@ -0,0 +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/relocation/lex_length.ma". +include "basic_2/rt_computation/lprs.ma". + +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) + +(* Forward lemmas with length for local environments ************************) + +lemma lprs_fwd_length (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → |L1| = |L2|. +/2 width=2 by lex_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma new file mode 100644 index 000000000..96c53c7db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lex_tc.ma". +include "basic_2/rt_computation/cprs_lpr.ma". +include "basic_2/rt_computation/lprs.ma". + +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) + +(* Eliminators with r-transition for full local environments ****************) + +(* Basic_2A1: was: lprs_ind_dx *) +lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1. +/3 width=7 by lpr_cprs_trans, cpr_refl, lex_CTC_ind_sn/ qed-. + +(* Basic_2A1: was: lprs_ind *) +lemma lprs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L2. +/3 width=7 by lpr_cprs_trans, cpr_refl, lex_CTC_ind_dx/ qed-. + +(* Properties with unbound rt-transition for full local environments ********) + +lemma lpr_lprs (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ ➡*[h] L2. +/3 width=3 by lpr_cprs_trans, lex_CTC_inj/ qed. + +(* Basic_2A1: was: lprs_strap2 *) +lemma lprs_step_sn (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → + ∀L2.⦃G, L⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ ➡*[h] L2. +/3 width=3 by lpr_cprs_trans, lex_CTC_step_sn/ qed-. + +(* Basic_2A1: was: lpxs_strap1 *) +lemma lprs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ➡*[h] L → + ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ ➡*[h] L2. +/3 width=3 by lpr_cprs_trans, lex_CTC_step_dx/ 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 1708bccc6..83cac1779 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -10,3 +10,4 @@ fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.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_lsubr.ma cpms_aaa.ma cpms_cpxs.ma cprs.ma cprs_drops.ma +lprs.ma lprs_length.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index fa5499ccb..31dad2da9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -286,3 +286,92 @@ lemma cpm_fwd_bind1_minus: ∀n,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡ #n #h #I #G #L #V1 #T1 #T * #c #Hc #H #p elim (cpg_fwd_bind1_minus … H p) -H /3 width=4 by ex2_2_intro, ex2_intro/ qed-. + +(* Basic eliminators ********************************************************) + +lemma isrt_inv_max_shift_sn: ∀n,c1,c2. 𝐑𝐓⦃n, ↕*c1 ∨ c2⦄ → + ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃n, c2⦄. +#n #c1 #c2 #H +elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct +elim (isrt_inv_shift … Hc1) -Hc1 #Hc1 * -n1 +/2 width=1 by conj/ +qed-. + +lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → eq_t c1 c2 → + ∧∧ 𝐑𝐓⦃n, c1⦄ & 𝐑𝐓⦃n, c2⦄. +#n #c1 #c2 #H #Hc12 +elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct +lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H +<(isrt_inj … H … Hc2) -Hc2 +max_shift #H + elim (isrt_inv_max_shift_sn … H) -H #H #HcT + elim (isrt_O_inv_max … H) -H #HcV #HcW + /3 width=3 by ex2_intro/ +| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #IHV #IHW #IHT #n #H + lapply (isrt_inv_plus_O_dx … H ?) -H // >max_shift #H + elim (isrt_inv_max_shift_sn … H) -H #H #HcT + elim (isrt_O_inv_max … H) -H #HcV #HcW + /3 width=4 by ex2_intro/ +] +qed-. -- 2.39.2