X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcprs_cprs.ma;h=fe6b36fcd2ef2edb7be9cac9ee64e9547db062cf;hb=e0f7a5025addf275e40372da3a39b0adacc8106f;hp=a6d78f1156a549c97107a73a0c5990f566ed15bf;hpb=e9f96fa56226dfd74de214c89d827de0c5018ac7;p=helm.git 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 a6d78f115..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 ************************************************) @@ -80,7 +48,7 @@ lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → 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 & + | ∃∃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/ @@ -100,34 +68,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. c_r_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. c_rs_transitive … (cpr G) (λ_. lpr G). -#G @c_r_trans_LTC1 /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 +88,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.