From e0f7a5025addf275e40372da3a39b0adacc8106f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Jun 2018 19:58:17 +0200 Subject: [PATCH] update in ground_2 and basic_2 + more results on cpm, and cpms --- .../basic_2/rt_computation/cpms.ma | 31 ++- .../basic_2/rt_computation/cpms_cpms.ma | 198 ++++++++++++++++++ .../basic_2/rt_computation/cpms_cpxs.ma | 2 +- .../basic_2/rt_computation/cpms_drops.ma | 109 +++++++--- .../basic_2/rt_computation/cpms_lpr.ma | 63 +++--- .../basic_2/rt_computation/cprs_cprs.ma | 54 +---- .../{lprs_drop.ma => cprs_ext.ma} | 20 +- .../basic_2/rt_computation/lprs.ma | 2 +- .../basic_2/rt_computation/lprs_drops.ma | 34 +++ .../basic_2/rt_computation/lpxs_lpx.ma | 2 +- .../basic_2/rt_computation/partial.txt | 5 +- .../basic_2/rt_computation/scpds_scpds.ma | 93 -------- .../lambdadelta/basic_2/rt_transition/cpm.ma | 17 -- .../basic_2/rt_transition/cpm_drops.ma | 115 +++++++--- .../lambdadelta/basic_2/rt_transition/cpr.ma | 38 +--- .../lambdadelta/basic_2/web/basic_2_src.tbl | 7 +- .../lambdadelta/ground_2/lib/arith.ma | 16 ++ .../lambdadelta/ground_2/steps/rtc_max.ma | 19 ++ 18 files changed, 527 insertions(+), 298 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lprs_drop.ma => cprs_ext.ma} (65%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drops.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma index 8c73990c8..8d27710bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma @@ -47,6 +47,15 @@ lemma cpms_ind_dx (h) (G) (L) (T1) (Q:relation2 …): #h #G #L #T1 #R @ltc_ind_dx_refl // qed-. +(* Basic inversion lemmas ***************************************************) + +lemma cpms_inv_sort1 (n) (h) (G) (L): ∀X2,s. ⦃G, L⦄ ⊢ ⋆s ➡*[n, h] X2 → X2 = ⋆(((next h)^n) s). +#n #h #G #L #X2 #s #H @(cpms_ind_dx … H) -X2 // +#n1 #n2 #X #X2 #_ #IH #HX2 destruct +elim (cpm_inv_sort1 … HX2) -HX2 * // #H1 #H2 destruct +/2 width=3 by refl, trans_eq/ +qed-. + (* Basic properties *********************************************************) (* Basic_1: includes: pr1_pr0 *) @@ -95,6 +104,16 @@ lemma cpms_eps (n) (h) (G) (L): /3 width=3 by cpms_step_sn, cpm_cpms, cpm_eps/ qed. +lemma cpms_ee (n) (h) (G) (L): + ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 → + ∀T. ⦃G, L⦄ ⊢ ⓝU1.T ➡*[↑n, h] U2. +#n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n +[ /3 width=1 by cpm_cpms, cpm_ee/ +| #n1 #n2 #U1 #U #HU1 #HU2 #_ #T >plus_S1 + /3 width=3 by cpms_step_sn, cpm_ee/ +] +qed. + (* Basic_2A1: uses: cprs_beta_dx *) lemma cpms_beta_dx (n) (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → @@ -116,21 +135,13 @@ lemma cpms_theta_dx (n) (h) (G) (L): /4 width=9 by cpms_step_dx, cpm_cpms, cpms_bind_dx, cpms_appl_dx, cpm_theta/ qed. -(* Basic inversion lemmas ***************************************************) - -lemma cpms_inv_sort1 (n) (h) (G) (L): ∀X2,s. ⦃G, L⦄ ⊢ ⋆s ➡*[n, h] X2 → X2 = ⋆(((next h)^n) s). -#n #h #G #L #X2 #s #H @(cpms_ind_dx … H) -X2 // -#n1 #n2 #X #X2 #_ #IH #HX2 destruct -elim (cpm_inv_sort1 … HX2) -HX2 * // #H1 #H2 destruct -/2 width=3 by refl, trans_eq/ -qed-. - (* Basic properties with r-transition ***************************************) (* Basic_1: was: pr3_refl *) lemma cprs_refl: ∀h,G,L. reflexive … (cpms h G L 0). /2 width=1 by cpm_cpms/ qed. -(* Basic_2A1: removed theorems 4: +(* Basic_2A1: removed theorems 5: sta_cprs_scpds lstas_scpds scpds_strap1 scpds_fwd_cprs + scpds_inv_lstas_eq *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma new file mode 100644 index 000000000..5fe790c89 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma @@ -0,0 +1,198 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpms_drops.ma". +include "basic_2/rt_computation/cprs.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Main properties **********************************************************) + +(* Basic_2A1: uses: lstas_scpds_trans scpds_strap2 *) +theorem cpms_trans (h) (G) (L): + ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → + ∀n2,T2. ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2. +/2 width=3 by ltc_trans/ qed-. + +(* Basic_2A1: uses: scpds_cprs_trans *) +theorem cpms_cprs_trans (n) (h) (G) (L): + ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T → + ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2. +#n #h #G #L #T1 #T #HT1 #T2 #HT2 >(plus_n_O … n) +/2 width=3 by cpms_trans/ qed-. + +(* Basic_2A1: includes: cprs_bind *) +theorem cpms_bind (n) (h) (G) (L): + ∀I,V1,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[n, h] T2 → + ∀V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2. +#n #h #G #L #I #V1 #T1 #T2 #HT12 #V2 #H @(cprs_ind_dx … H) -V2 +[ /2 width=1 by cpms_bind_dx/ +| #V #V2 #_ #HV2 #IH #p >(plus_n_O … n) -HT12 + /3 width=3 by cpr_pair_sn, cpms_step_dx/ +] +qed. + +theorem cpms_appl (n) (h) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → + ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 → + ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[n, h] ⓐV2.T2. +#n #h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind_dx … H) -V2 +[ /2 width=1 by cpms_appl_dx/ +| #V #V2 #_ #HV2 #IH >(plus_n_O … n) -HT12 + /3 width=3 by cpr_pair_sn, cpms_step_dx/ +] +qed. + +lemma cpms_inv_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T & ⦃G, L⦄ ⊢ T ➡*[n2, h] T2. +#h #G #L #n1 elim n1 -n1 /2 width=3 by ex2_intro/ +#n1 #IH #n2 #T1 #T2 (plus_n_O … n) -HT12 + /4 width=3 by cpr_pair_sn, cpms_step_dx/ +] +qed. + +(* Basic_2A1: includes: cprs_beta *) +theorem cpms_beta (n) (h) (G) (L): + ∀W1,T1,T2. ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2 → + ∀W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 → + ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 → + ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡*[n, h] ⓓ{p}ⓝW2.V2.T2. +#n #h #G #L #W1 #T1 #T2 #HT12 #W2 #HW12 #V1 #V2 #H @(cprs_ind_dx … H) -V2 +[ /2 width=1 by cpms_beta_rc/ +| #V #V2 #_ #HV2 #IH #p >(plus_n_O … n) -HT12 + /4 width=5 by cpms_step_dx, cpr_pair_sn, cpm_cast/ +] +qed. + +(* Basic_2A1: includes: cprs_theta_rc *) +theorem cpms_theta_rc (n) (h) (G) (L): + ∀V1,V. ⦃G, L⦄ ⊢ V1 ➡[h] V → ∀V2. ⬆*[1] V ≘ V2 → + ∀W1,T1,T2. ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[n, h] T2 → + ∀W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 → + ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n, h] ⓓ{p}W2.ⓐV2.T2. +#n #h #G #L #V1 #V #HV1 #V2 #HV2 #W1 #T1 #T2 #HT12 #W2 #H @(cprs_ind_dx … H) -W2 +[ /2 width=3 by cpms_theta_dx/ +| #W #W2 #_ #HW2 #IH #p >(plus_n_O … n) -HT12 + /3 width=3 by cpr_pair_sn, cpms_step_dx/ +] +qed. + +(* Basic_2A1: includes: cprs_theta *) +theorem cpms_theta (n) (h) (G) (L): + ∀V,V2. ⬆*[1] V ≘ V2 → ∀W1,W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 → + ∀T1,T2. ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[n, h] T2 → + ∀V1. ⦃G, L⦄ ⊢ V1 ➡*[h] V → + ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n, h] ⓓ{p}W2.ⓐV2.T2. +#n #h #G #L #V #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #HT12 #V1 #H @(cprs_ind_sn … H) -V1 +[ /2 width=3 by cpms_theta_rc/ +| #V1 #V0 #HV10 #_ #IH #p >(plus_O_n … n) -HT12 + /3 width=3 by cpr_pair_sn, cpms_step_sn/ +] +qed. +(* +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was pr3_gen_appl *) +lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & + U2 = ⓐV2. T2 + | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T & + ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡* U2 + | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⬆[0,1] V0 ≘ V2 & + ⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T & + ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2. +#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cprs_strap1, or3_intro0, ex3_2_intro/ + | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct + lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12 + lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 + /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_beta, ex2_3_intro, or3_intro1/ + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + /5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/ + ] +| /4 width=9 by cprs_strap1, or3_intro1, ex2_3_intro/ +| /4 width=11 by cprs_strap1, or3_intro2, ex4_5_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma scpds_inv_abst1: ∀h,o,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, o, d] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, o, d] T2 & + U2 = ⓛ{a}V2.T2. +#h #o #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 +lapply (da_inv_bind … Hd1) -Hd1 #Hd1 +elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct +elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct +/3 width=6 by ex4_2_intro, ex3_2_intro/ +qed-. + +lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 → + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true. +#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 +lapply (da_inv_bind … Hd1) -Hd1 #Hd1 +elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct +elim (cprs_inv_abbr1 … H2) -H2 * +[ #V2 #U2 #HV12 #HU12 #H destruct +| /3 width=6 by ex4_2_intro, ex3_intro/ +] +qed-. + +lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → + ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2. +#h #o #G #L #T1 #T2 #d2 * +#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1 +lapply (lstas_mono … HT10 … HT1) #H destruct // +qed-. + +(* Main properties **********************************************************) + +theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 → + ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. +#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2 +lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_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 index 9d07288c3..6d898a9ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma @@ -20,7 +20,7 @@ include "basic_2/rt_computation/cpms.ma". (* Forward lemmas with unbound context-sensitive rt-computation for terms ***) -(* Basic_2A1: includes: cprs_cpxs *) +(* Basic_2A1: includes: scpds_fwd_cpxs 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/ 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 index 568100b54..dce2cecf5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma @@ -18,8 +18,76 @@ include "basic_2/rt_computation/cpms.ma". (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) +(* Properties with generic slicing for local environments *******************) + +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-. + +(* Basic_2A1: uses: scpds_lift *) +(* Basic_2A1: includes: cprs_lift *) +(* Basic_1: includes: pr3_lift *) +lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n). +#n #h #G @d_liftable2_sn_bi +/2 width=6 by cpms_lifts_sn, lifts_mono/ +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-. + +lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n). +#n #h #G @d_deliftable2_sn_bi +/2 width=6 by cpms_inv_lifts_sn, lifts_inj/ +qed-. + (* Advanced properties ******************************************************) +lemma cpms_delta (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 → + ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓓV1⦄ ⊢ #0 ➡*[n, h] W2. +#n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2 +[ /3 width=3 by cpm_cpms, cpm_delta/ +| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2 + elim (lifts_total V (𝐔❴1❵)) #W #HVW + /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/ +] +qed. + +lemma cpms_ell (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 → + ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓛV1⦄ ⊢ #0 ➡*[↑n, h] W2. +#n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2 +[ /3 width=3 by cpm_cpms, cpm_ell/ +| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2 + elim (lifts_total V (𝐔❴1❵)) #W #HVW >plus_S1 + /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/ +] +qed. + +lemma cpms_lref (n) (h) (I) (G): ∀K,T,i. ⦃G, K⦄ ⊢ #i ➡*[n, h] T → + ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #↑i ➡*[n, h] U. +#n #h #I #G #K #T #i #H @(cpms_ind_dx … H) -T +[ /3 width=3 by cpm_cpms, cpm_lref/ +| #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2 + elim (lifts_total T (𝐔❴1❵)) #U #TU + /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/ +] +qed. + +lemma cpms_cast_sn (n) (h) (G) (L): + ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → + ⦃G, L⦄ ⊢ ⓝU1.T1 ➡*[n, h] ⓝU2.T2. +#n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n +[ /3 width=3 by cpm_cpms, cpm_cast/ +| #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H + elim (cpm_fwd_plus … H) -H #T #HT1 #HT2 + /3 width=3 by cpms_step_sn, cpm_cast/ +] +qed. + (* Note: apparently this was missing in basic_1 *) (* Basic_2A1: uses: cprs_delta *) lemma cpms_delta_drops (n) (h) (G): @@ -65,28 +133,21 @@ lemma cpms_inv_lref1_drops (n) (h) (G): ] qed-. -(* Properties with generic slicing for local environments *******************) - -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-. - -(* Basic_2A1: uses: scpds_lift *) -(* Basic_2A1: includes: cprs_lift *) -(* Basic_1: includes: pr3_lift *) -lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n). -#n #h #G @d_liftable2_sn_bi -/2 width=6 by cpms_lifts_sn, lifts_mono/ -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-. - -lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n). -#n #h #G @d_deliftable2_sn_bi -/2 width=6 by cpms_inv_lifts_sn, lifts_inj/ +fact cpms_inv_succ_sn (n) (h) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[↑n, h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[1, h] T & ⦃G, L⦄ ⊢ T ➡*[n, h] T2. +#n #h #G #L #T1 #T2 +@(insert_eq_0 … (↑n)) #m #H +@(cpms_ind_sn … H) -T1 -m +[ #H destruct +| #x1 #n2 #T1 #T #HT1 #HT2 #IH #H + elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H + [ #H1 #H2 destruct -HT2 + elim IH -IH // #T0 #HT0 #HT02 + /3 width=3 by cpms_step_sn, ex2_intro/ + | #n1 #H1 #H2 destruct -IH + elim (cpm_fwd_plus … 1 n1 T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0 + /3 width=5 by cpms_step_sn, cpm_cpms, ex2_intro/ + ] +] qed-. 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 index f572acf67..a23d8948a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_lpr.ma @@ -12,51 +12,45 @@ (* *) (**************************************************************************) -include "ground_2/lib/star.ma". include "basic_2/rt_transition/lpr.ma". -include "basic_2/rt_computation/cpms.ma". +include "basic_2/rt_computation/cpms_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 +lemma lpr_cpm_trans (n) (h) (G): + ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 → + ∀L1. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2. +#n #h #G #L2 #T1 #T2 #H @(cpm_ind … H) -n -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/ +| /3 width=2 by cpm_cpms/ +| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H + elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct + /4 width=3 by cpms_delta, cpms_step_sn/ +| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H + elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct + /4 width=3 by cpms_ell, cpms_step_sn/ +| #n #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H + elim (lpr_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct + /4 width=3 by cpms_lref, cpms_step_sn/ +| /4 width=1 by cpms_bind, lpr_bind_refl_dx/ +| /3 width=1 by cpms_appl/ +| /3 width=1 by cpms_cast/ +| /4 width=3 by cpms_zeta, lpr_bind_refl_dx/ +| /3 width=1 by cpms_eps/ +| /3 width=1 by cpms_ee/ +| /4 width=1 by lpr_bind_refl_dx, cpms_beta/ +| /4 width=3 by lpr_bind_refl_dx, cpms_theta/ ] 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-. +(* Basic_1: uses: pr3_pr2_pr2_t *) +(* Basic_1: includes: pr3_pr0_pr2_t *) +(* Basic_2A1: includes: lpr_cpr_trans *) +lemma lpr_cpm_trans (n) (h) (G): s_r_transitive … (λL. cpm h G L n) (λ_. lpr h G). 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. @@ -73,3 +67,4 @@ 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. +*) \ No newline at end of file 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 e69c6b8d2..fe6b36fcd 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 @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpr_lpr.ma". -include "basic_2/computation/cprs_lift.ma". +include "basic_2/rt_transition/lpr_lpr.ma". +include "basic_2/rt_computation/cpms_cpms.ma". -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION FOR TERMS *************************) (* Main properties **********************************************************) @@ -29,47 +29,15 @@ normalize /2 width=3 by trans_TC/ qed-. theorem cprs_conf: ∀G,L. confluent2 … (cprs G L) (cprs G L). normalize /3 width=3 by cpr_conf, TC_confluent2/ qed-. -theorem cprs_bind: ∀a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 -/3 width=5 by cprs_trans, cprs_bind_dx/ -qed. - (* Basic_1: was: pr3_flat *) -theorem cprs_flat: ∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → - ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡* ⓕ{I}V2.T2. -#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 -/3 width=3 by cprs_flat_dx, cprs_strap1, cpr_pair_sn/ -qed. - -theorem cprs_beta_rc: ∀a,G,L,V1,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2. -#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1 by cprs_beta_dx/ -#W #W2 #_ #HW2 #IHW1 (**) (* fulla uto too slow 14s *) -@(cprs_trans … IHW1) -IHW1 /3 width=1 by cprs_flat_dx, cprs_bind/ -qed. - -theorem cprs_beta: ∀a,G,L,V1,V2,W1,W2,T1,T2. - ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2. -#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1 by cprs_beta_rc/ -#V #V2 #_ #HV2 #IHV1 -@(cprs_trans … IHV1) -IHV1 /3 width=1 by cprs_flat_sn, cprs_bind/ -qed. - -theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ➡ V → ⬆[0, 1] V ≘ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → - ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cprs_ind … H) -W2 -/3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/ -qed. - -theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. - ⬆[0, 1] V ≘ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → - ⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(cprs_ind_dx … H) -V1 -/3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/ +theorem cprs_flat (h) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → + ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h] ⓕ{I}V2.T2. +#h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind_dx … H) -V2 +[ /2 width=3 by cprs_flat_dx/ +| /3 width=3 by cpr_pair_sn, cprs_step_dx/ +] qed. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_ext.ma similarity index 65% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_ext.ma index f52b71147..01da390f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_ext.ma @@ -12,18 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpr_drop.ma". -include "basic_2/computation/lprs.ma". +include "basic_2/syntax/cext2.ma". +include "basic_2/rt_computation/cpms.ma". -(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) +(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR BINDERS *********************) -(* Properties on local environment slicing ***********************************) +definition cprs_ext (h) (G): relation3 lenv bind bind ≝ + cext2 (λL. cpms h G L 0). -lemma lprs_drop_conf: ∀G. dropable_sn (lprs G). -/3 width=3 by dropable_sn_TC, lpr_drop_conf/ qed-. - -lemma drop_lprs_trans: ∀G. dedropable_sn (lprs G). -/3 width=3 by dedropable_sn_TC, drop_lpr_trans/ qed-. - -lemma lprs_drop_trans_O1: ∀G. dropable_dx (lprs G). -/3 width=3 by dropable_dx_TC, lpr_drop_trans_O1/ qed-. +interpretation + "context-sensitive parallel r-computation (binder)" + 'PRedStar h G L I1 I2 = (cprs_ext h G L I1 I2). 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 02f4a101c..c06e0278d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/predsnstar_4.ma". include "basic_2/relocation/lex.ma". -include "basic_2/rt_computation/cpms.ma". +include "basic_2/rt_computation/cprs_ext.ma". (* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drops.ma new file mode 100644 index 000000000..aeef8e87a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_drops.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lex.ma". +include "basic_2/rt_computation/cpms_drops.ma". + +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: was: drop_lprs_trans *) +lemma drops_lprs_trans (h) (G): dedropable_sn (λL.cpms h G L 0). +/3 width=6 by lex_liftable_dedropable_sn, cpms_lifts_sn/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: was: lprs_drop_conf *) +lemma lprs_drops_conf (h) (G): dropable_sn (λL.cpms h G L 0). +/2 width=3 by lex_dropable_sn/ qed-. + +(* Basic_2A1: was: lprs_drop_trans_O1 *) +lemma lprs_drops_trans (h) (G): dropable_dx (λL.cpms h G L 0). +/2 width=3 by lex_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma index 7bc58ea45..f64f762ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/relocation/lex_tc.ma". -include "basic_2/rt_computation/lpxs.ma". include "basic_2/rt_computation/cpxs_lpx.ma". +include "basic_2/rt_computation/lpxs.ma". (* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) 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 83cac1779..7c1902149 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -8,6 +8,7 @@ lsubsx.ma lsubsx_rdsx.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_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma 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 +cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_lpr.ma cpms_cpxs.ma cpms_cpms.ma cprs.ma cprs_drops.ma -lprs.ma lprs_length.ma +cprs_ext.ma +lprs.ma lprs_length.ma lprs_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma deleted file mode 100644 index ae37338ac..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma +++ /dev/null @@ -1,93 +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_da.ma". -include "basic_2/computation/lprs_cprs.ma". -include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/scpds.ma". - -(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) - -(* Advanced properties ******************************************************) - -lemma scpds_strap2: ∀h,o,G,L,T1,T,T2,d1,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1+1 → - ⦃G, L⦄ ⊢ T1 •*[h, 1] T → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] T2 → - ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d+1] T2. -#h #o #G #L #T1 #T #T2 #d1 #d #Hd1 #HT1 * -#T0 #d0 #Hd0 #HTd0 #HT0 #HT02 -lapply (lstas_da_conf … HT1 … Hd1) commutative_plus -/3 width=6 by le_S_S, ex4_2_intro/ -qed. - -lemma scpds_cprs_trans: ∀h,o,G,L,T1,T,T2,d. - ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2. -#h #o #G #L #T1 #T #T2 #d * /3 width=8 by cprs_trans, ex4_2_intro/ -qed-. - -lemma lstas_scpds_trans: ∀h,o,G,L,T1,T,T2,d1,d2,d. - d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → - ⦃G, L⦄ ⊢ T1 •*[h, d2] T → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d2+d] T2. -#h #o #G #L #T1 #T #T2 #d1 #d2 #d #Hd21 #HTd1 #HT1 * #T0 #d0 #Hd0 #HTd0 #HT0 #HT02 -lapply (lstas_da_conf … HT1 … HTd1) #HTd12 -lapply (da_mono … HTd12 … HTd0) -HTd12 -HTd0 #H destruct -lapply (le_minus_to_plus_c … Hd21 Hd0) -Hd21 -Hd0 -/3 width=7 by lstas_trans, ex4_2_intro/ -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma scpds_inv_abst1: ∀h,o,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, o, d] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, o, d] T2 & - U2 = ⓛ{a}V2.T2. -#h #o #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct -elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct -/3 width=6 by ex4_2_intro, ex3_2_intro/ -qed-. - -lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 → - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true. -#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct -elim (cprs_inv_abbr1 … H2) -H2 * -[ #V2 #U2 #HV12 #HU12 #H destruct -| /3 width=6 by ex4_2_intro, ex3_intro/ -] -qed-. - -lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → - ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2. -#h #o #G #L #T1 #T2 #d2 * -#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1 -lapply (lstas_mono … HT10 … HT1) #H destruct // -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma scpds_fwd_cpxs: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2. -#h #o #G #L #T1 #T2 #d * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/ -qed-. - -(* Main properties **********************************************************) - -theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 → - ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. -#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2 -lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/ -qed-. 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 31dad2da9..8d917e55f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -289,23 +289,6 @@ 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 -