From: Ferruccio Guidi Date: Thu, 9 May 2013 20:53:51 +0000 (+0000) Subject: partial commit: finaly we issue the "computation" component ... X-Git-Tag: make_still_working~1159 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e02bd4f3df78b5cc374d49d0ddf48b311188f514;p=helm.git partial commit: finaly we issue the "computation" component ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index b7b967e1a..0e63d954c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unfold/ldrops.ma". +include "basic_2/substitution/ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 2ffff40df..b23563f14 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lifts_lifts.ma". -include "basic_2/unfold/ldrops_ldrops.ma". +include "basic_2/substitution/lifts_lifts.ma". +include "basic_2/substitution/ldrops_ldrops.ma". include "basic_2/static/aaa_lifts.ma". include "basic_2/static/aaa_aaa.ma". include "basic_2/computation/lsubc_ldrops.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index e8dfcbfde..a452a9073 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -13,9 +13,9 @@ (**************************************************************************) include "basic_2/grammar/aarity.ma". -include "basic_2/unfold/gr2_gr2.ma". -include "basic_2/unfold/lifts_lift_vector.ma". -include "basic_2/unfold/ldrops_ldrop.ma". +include "basic_2/substitution/gr2_gr2.ma". +include "basic_2/substitution/lifts_lift_vector.ma". +include "basic_2/substitution/ldrops_ldrop.ma". include "basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index 228f9450c..d3aaae5de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -12,13 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cnf.ma". -include "basic_2/computation/tprs.ma". +include "basic_2/reduction/cnf.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) -definition cprs: lenv → relation term ≝ - λL. TC … (cpr L). +(* Basic_1: includes: pr1_pr0 *) +definition cprs: lenv → relation term ≝ LTC … cpr. interpretation "context-sensitive parallel computation (term)" 'PRedStar L T1 T2 = (cprs L T1 T2). @@ -45,41 +44,88 @@ qed-. lemma cpr_cprs: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ➡* T2. /2 width=1/ qed. +lemma cpss_cprs: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➡* T2. +/3 width=1/ qed. + (* Basic_1: was: pr3_refl *) lemma cprs_refl: ∀L,T. L ⊢ T ➡* T. /2 width=1/ qed. lemma cprs_strap1: ∀L,T1,T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → L ⊢ T1 ➡* T2. -/2 width=3/ qed. +normalize /2 width=3/ qed. (* Basic_1: was: pr3_step *) lemma cprs_strap2: ∀L,T1,T,T2. L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. -/2 width=3/ qed. +normalize /2 width=3/ qed. + +lemma cprs_cpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ➡* T2. +/3 width=3/ qed-. + +lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. +/3 width=3/ qed-. + +lemma cprs_lsubr_trans: lsubr_trans … cprs. +/3 width=3 by cpr_lsubr_trans, TC_lsubr_trans/ +qed-. + +(* Basic_1: was: pr3_pr1 *) +lemma tprs_cprs: ∀L,T1,T2. ⋆ ⊢ T1 ➡* T2 → L ⊢ T1 ➡* T2. +#L #T1 #T2 #H @(cprs_lsubr_trans … H) -H // +qed. + +lemma cprs_ext_bind_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2 +/3 width=1/ /3 width=6/ +qed. -(* Note: it does not hold replacing |L1| with |L2| *) -lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → - ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2. -/3 width=3/ +lemma cprs_bind_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 +/3 width=1/ /3 width=3/ qed. (* Basic_1: was only: pr3_thin_dx *) lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 → L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. #I #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/ -#T #T2 #_ #HT2 #IHT2 -@(cprs_strap1 … IHT2) -IHT2 /2 width=1/ +#T #T2 #_ #HT2 #IHT1 +@(cprs_strap1 … IHT1) -V1 -T1 /2 width=1/ qed. -lemma tpss_cprs: ∀L,T1,T2,d,e. L ⊢ T1 ▶*[d, e] T2 → L ⊢ T1 ➡* T2. -#L #T1 #T2 #d #e #HT12 -lapply (cpr_intro … T1 … HT12) // /2 width=1/ +lemma cprs_flat_sn: ∀I,L,T1,T2. L ⊢ T1 ➡ T2 → ∀V1,V2. L ⊢ V1 ➡* V2 → + L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. +#I #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cprs_strap1 … IHV1) -V1 -T1 /2 width=1/ qed. -(* Basic_1: was: pr3_pr1 *) -lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2. -#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/ +lemma cprs_zeta: ∀L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T → + L.ⓓV ⊢ T1 ➡* T → L ⊢ +ⓓV.T1 ➡* T2. +#L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/ +qed. + +lemma cprs_tau: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ∀V. L ⊢ ⓝV.T1 ➡* T2. +#L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/ +qed. + +lemma cprs_beta_dx: ∀a,L,V1,V2,W,T1,T2. + L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → + L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. +#a #L #V1 #V2 #W #T1 #T2 #HV12 #H elim H -T2 /3 width=1/ +#T #T2 #_ #HT2 #IHT1 +@(cprs_strap1 … IHT1) -V1 -T1 /3 width=2/ +qed. + +lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,T1,T2. + L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 → + ∀W2. L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #L #V1 #V #V2 #W1 #T1 #T2 #HV1 #HV2 #H elim H -T2 [ /3 width=3/ ] +#T #T2 #_ #HT2 #IHT1 #W2 #HW12 +lapply (IHT1 W1 ?) -IHT1 // #HT1 +@(cprs_strap1 … HT1) -HT1 -V -V1 /3 width=1/ qed. (* Basic inversion lemmas ***************************************************) @@ -91,6 +137,29 @@ lemma cprs_inv_sort1: ∀L,U2,k. L ⊢ ⋆k ➡* U2 → U2 = ⋆k. >(cpr_inv_sort1 … HU2) -HU2 // qed-. +(* Basic_1: was pr3_gen_appl *) +lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → + ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & + U2 = ⓐV2. T2 + | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 & + L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2 + | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & + L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2. +#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ + | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct + lapply (cprs_strap1 … HV10 … HV02) -V0 /5 width=7/ + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + ] +| /4 width=9/ +| /4 width=11/ +] +qed-. + (* Basic_1: was: pr3_gen_cast *) lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓝW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨ ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓝW2.T2. @@ -108,10 +177,26 @@ lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ qed-. -lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U. -/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-. +(* Basic forward lemmas *****************************************************) + +(* Basic_1: was: pr3_gen_abst *) +lemma cprs_fwd_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡* U2 → ∀I,W. + ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 & + U2 = ⓛ{a}V2. T2. +#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ +#U #U2 #_ #HU2 #IHU1 #I #W +elim (IHU1 I W) -IHU1 #V #T #HV1 #HT1 #H destruct +elim (cpr_fwd_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + +lemma cprs_fwd_abst: ∀a,L,V1,V2,T1,T2. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → ∀I,W. + L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2. +#a #L #V1 #V2 #T1 #T2 #H #I #W +elim (cprs_fwd_abst1 … H I W) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ +qed-. -(* Basic_1: removed theorems 10: +(* Basic_1: removed theorems 13: + pr1_head_1 pr1_head_2 pr1_comp clear_pr3_trans pr3_cflat pr3_gen_bind pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12 pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma index e04e3c784..389e241ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr_aaa.ma". +include "basic_2/reduction/lpr_aaa.ma". include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -21,5 +21,5 @@ include "basic_2/computation/cprs.ma". lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. #L #T1 #A #HT1 #T2 #HT12 -@(TC_Conf3 … HT1 ? HT12) /2 width=3/ -qed. +@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=3 by aaa_cpr_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index 75f74caad..e437136dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -12,156 +12,133 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr_lift.ma". -include "basic_2/reducibility/cpr_cpr.ma". -include "basic_2/reducibility/lfpr_cpr.ma". -include "basic_2/computation/cprs_lfpr.ma". +include "basic_2/reduction/lpr_lpr.ma". +include "basic_2/computation/cprs_lift.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) -(* Advanced properties ******************************************************) +(* Main properties **********************************************************) -lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → - ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2 -[ /3 width=2/ -| /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *) -] -qed. +(* Basic_1: was: pr3_t *) +(* Basic_1: includes: pr1_t *) +theorem cprs_trans: ∀L. Transitive … (cprs L). +#L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) -lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → - ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 -[ /3 width=5/ -| #T1 #T #HT1 #_ #IHT1 - @(cprs_strap2 … IHT1) -IHT1 /2 width=1/ -] +(* Basic_1: was: pr3_confluence *) +(* Basic_1: includes: pr1_confluence *) +theorem cprs_conf: ∀L. confluent2 … (cprs L) (cprs L). +#L @TC_confluent2 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) + +theorem cprs_ext_bind: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #H #V #T1 #T2 #HT12 #a #I @(TC_ind_dx … V1 H) -V1 /2 width=3/ +#V1 #V0 #HV10 #_ #IHV02 +@(cprs_trans … IHV02) /2 width=1/ qed. -lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 → - ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -/3 width=1/ qed. - -lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 → - ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 -lapply (lfpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ +theorem cprs_bind: ∀a,I,L,V1,V2,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 → + L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cprs_trans … IHV1) -V1 /2 width=1/ qed. -(* Basic_1: was: pr3_strip *) -lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 → - ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0. -/3 width=3/ qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was pr3_gen_appl *) -lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → - ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 & - U2 = ⓐV2. T2 - | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 & - L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2 - | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & - L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2. -#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ -#U #U2 #_ #HU2 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpr_inv_appl1 … HU2) -HU2 * - [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ - | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/ - | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct - @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) - ] -| /4 width=9/ -| /4 width=11/ -] -qed-. - -(* Main propertis ***********************************************************) - -(* Basic_1: was: pr3_confluence *) -theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 → - ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0. -/3 width=3/ qed. - -(* Basic_1: was: pr3_t *) -theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. -/2 width=3/ qed. - (* Basic_1: was: pr3_flat *) -lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 → - L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. -#I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ +theorem cprs_flat: ∀I,L,V1,V2,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 → + L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/ #V #V2 #_ #HV2 #IHV1 @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. -lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → - ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I @(cprs_ind … HV12) -V2 -[ lapply (cprs_lsubr_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/ -| #V0 #V2 #_ #HV02 #IHV01 - @(cprs_trans … IHV01) -V1 /2 width=2/ -] +theorem cprs_beta: ∀a,L,V1,V2,W,T1,T2. + L.ⓛW ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 → + L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. +#a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 +@(cprs_trans … IHV1) /2 width=1/ qed. -lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → - ∀a.L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -#L #V1 #T1 #T2 #HT12 #V2 #HV12 #a @(cprs_ind … HV12) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 -@(cprs_trans … IHV1) -IHV1 /2 width=1/ +theorem cprs_theta_rc: ∀a,L,V1,V,V2,W1,W2,T1,T2. + L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 → + L ⊢ W1 ➡* W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/ +#W #W2 #_ #HW2 #IHW1 +@(cprs_trans … IHW1) /2 width=1/ qed. -lemma cprs_bind1: ∀I,L,V1,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → - ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. -* /2 width=1/ /2 width=2/ +theorem cprs_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2. + ⇧[0, 1] V ≡ V2 → L ⊢ W1 ➡* W2 → L.ⓓW1 ⊢ T1 ➡* T2 → + L ⊢ V1 ➡* V → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/ +#V1 #V0 #HV10 #_ #IHV0 +@(cprs_trans … IHV0) /2 width=1/ qed. -lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → - ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 -[ /2 width=1/ -| #T1 #T #HT1 #_ #IHT1 - lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1 - @(cprs_trans … IHT1) -IHT1 /2 width=1/ +(* 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: s_r_trans … cpr lpr. +#L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2 +[ /2 width=3/ +| #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 + elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + lapply (IHV02 … HK12) -K2 #HV02 + lapply (cprs_strap2 … HV10 … HV02) -V0 /2 width=6/ +| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/ +|4,6: /3 width=1/ +| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 + lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/ +| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/ +| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 + lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/ ] -qed. +qed-. -lemma cprs_abbr2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → - ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. -#L #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 #a -lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1 -@(cprs_trans … HV1) -HV1 /2 width=1/ +lemma cpr_bind2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡ T2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lpr_cpr_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ qed. -lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → - ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. -#L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/ -qed. +(* Advanced properties ******************************************************) -lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. - L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → - ∀a.L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. -#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2 -[ /3 width=1/ -| -HV12 #T #T2 #_ #HT2 #IHT1 - lapply (cpr_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2 - @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/ +(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) +lemma lpr_cprs_trans: s_rs_trans … cpr lpr. +/3 width=5 by s_r_trans_TC1, lpr_cpr_trans/ qed-. + +(* Basic_1: was: pr3_strip *) +(* Basic_1: includes: pr1_strip *) +lemma cprs_strip: ∀L. confluent2 … (cprs L) (cpr L). +#L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *) + +lemma cprs_lpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 → + ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #H elim H -T1 +[ #T1 #HT01 #L1 #HL01 + elim (lpr_cpr_conf_dx … HT01 … HL01) -L0 /3 width=3/ +| #T #T1 #_ #HT1 #IHT0 #L1 #HL01 + elim (IHT0 … HL01) #T2 #HT2 #HT02 + elim (lpr_cpr_conf_dx … HT1 … HL01) -L0 #T3 #HT3 #HT13 + elim (cprs_strip … HT2 … HT3) -T #T #HT2 #HT3 + lapply (cprs_strap2 … HT13 … HT3) -T3 + lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/ ] -qed. +qed-. -lemma ltpr_cprs_trans: ∀L1,L2. L1 ➡ L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT2 -@(cprs_trans … IHT2) /2 width=3/ -qed. +lemma cprs_lpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 → + ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 #T #HT1 +lapply (lpr_cprs_trans … HT1 … HL01) -HT1 /2 width=3/ +qed-. -(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) -lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // -#T #T2 #_ #HT2 #IHT2 -@(cprs_trans … IHT2) /2 width=3/ +lemma cprs_bind2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lpr_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma deleted file mode 100644 index 6b7892611..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_delift.ma +++ /dev/null @@ -1,37 +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/reducibility/cpr_delift.ma". -include "basic_2/reducibility/cpr_cpr.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties on inverse basic term relocation ******************************) - -(* Note: this should be stated with tprs *) -lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2. -#L #V #T1 #T2 * #T #HT1 #HT2 -@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *) -qed. - -(* Basic_1: was only: pr3_gen_cabbr *) -lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 → - ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → - ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2. -#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/ -#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 -elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT -elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma deleted file mode 100644 index 799ec7bc6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma +++ /dev/null @@ -1,46 +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/reducibility/ltpr_tps.ma". -include "basic_2/reducibility/cpr_ltpss_sn.ma". -include "basic_2/reducibility/lfpr.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties concerning focalized parallel reduction on local environments *) - -lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃T. L1 ⊢ T1 ▶* [d, e] T & L1 ⊢ T ➡* T2. -#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2 -[ /2 width=3/ -| #T #T2 #_ #HT2 * #T0 #HT10 #HT0 - elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32 - @(ex2_intro … HT10) -T1 (**) (* explicit constructors *) - @(cprs_strap1 … T3 …) /2 width=1/ -HT32 - @(cprs_strap1 … HT0) -HT0 /3 width=3/ -] -qed. - -(* Basic_1: was just: pr3_pr0_pr2_t *) -lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 #T1 #T2 * #T #HT1 -<(ltpr_fwd_length … HL12) #HT2 -elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/ -qed. - -(* Basic_1: was just: pr3_pr2_pr2_t *) -lemma lfpr_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 * /3 width=7/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma deleted file mode 100644 index 33620d01c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfprs.ma +++ /dev/null @@ -1,56 +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/computation/cprs_cprs.ma". -include "basic_2/computation/lfprs_lfprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties on focalized computation for local environments ***************) - -(* Basic_1: was just: pr3_pr3_pr3_t *) -lemma lfprs_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -#L1 #L2 #HL12 @(lfprs_ind … HL12) -L2 // /3 width=3/ -qed. - -lemma lfprs_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → - ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. -/3 width=3 by lfprs_cprs_trans, inj/ qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_1: was pr3_gen_abbr *) -lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 → - (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & - U2 = ⓓ{a}V2. T2 - ) ∨ - ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. -#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ -#U0 #U2 #_ #HU02 * * -[ #V0 #T0 #HV10 #HT10 #H destruct - elim (cpr_inv_abbr1 … HU02) -HU02 * - [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct - lapply (cpr_intro … HV0 … HV2) -HV2 #HV02 - lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02 - lapply (lfprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ - | #T2 #HT02 #HUT2 - lapply (lfprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ - ] -| #U1 #HTU1 #HU01 - elim (lift_total U2 0 1) #U #HU2 - lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma index 36ce0ef83..7e75767b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma @@ -12,11 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cpr_lift.ma". +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: ∀L,K,V,V2,i. + ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ➡* V2 → + ∀W2. ⇧[0, i + 1] V2 ≡ W2 → L ⊢ #i ➡* W2. +#L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ] +#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 +lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK +elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/ +qed. + (* Advanced inversion lemmas ************************************************) (* Basic_1: was: pr3_gen_lref *) @@ -24,55 +36,25 @@ lemma cprs_inv_lref1: ∀L,T2,i. L ⊢ #i ➡* T2 → T2 = #i ∨ ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & K ⊢ V1 ➡* T1 & - ⇧[0, i + 1] T1 ≡ T2 & - i < |L|. + ⇧[0, i + 1] T1 ≡ T2. #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/ #T #T2 #_ #HT2 * [ #H destruct elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/ - * #K #V1 #T1 #HLK #HVT1 #HT12 #Hi - @or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *) -| * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi + * /4 width=6/ +| * #K #V1 #T1 #HLK #HVT1 #HT1 lapply (ldrop_fwd_ldrop2 … HLK) #H0LK - elim (cpr_inv_lift1 … H0LK … HT1 … HT2) -H0LK -T /4 width=6/ + elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/ ] qed-. -(* Basic_1: was: pr3_gen_abst *) -lemma cprs_inv_abst1: ∀I,W,a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡* U2 → - ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 & - U2 = ⓛ{a}V2. T2. -#I #W #a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/ -#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ -qed-. - -lemma cprs_inv_abst: ∀a,L,V1,V2,T1,T2. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → ∀I,W. - L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2. -#a #L #V1 #V2 #T1 #T2 #H #I #W -elim (cprs_inv_abst1 I W … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ -qed-. - (* Relocation properties ****************************************************) (* Basic_1: was: pr3_lift *) -lemma cprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → - ∀T2. K ⊢ T1 ➡* T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → - L ⊢ U1 ➡* U2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #HT12 @(cprs_ind … HT12) -T2 -[ -HLK #T2 #HT12 - <(lift_mono … HTU1 … HT12) -T1 // -| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2 - elim (lift_total T d e) #U #HTU - lapply (cpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/ -] -qed. +lemma cprs_lift: l_liftable cprs. +/3 width=9/ qed. (* Basic_1: was: pr3_gen_lift *) -lemma cprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 #HU12 @(cprs_ind … HU12) -U2 /2 width=3/ --HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 -elim (cpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/ -qed. +lemma cprs_inv_lift1: l_deliftable_sn cprs. +/3 width=5 by l_deliftable_sn_LTC, cpr_inv_lift1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma new file mode 100644 index 000000000..4aedee56d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lpss_cpss.ma". +include "basic_2/reduction/lpr_lpss.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties on parallel substitution for terms ****************************) + +(* Basic_1: was: pr3_subst1 *) +lemma cprs_cpss_conf: ∀L,T0,T1. L ⊢ T0 ➡* T1 → ∀T2. L ⊢ T0 ▶* T2 → + ∃∃T. L ⊢ T1 ▶* T & L ⊢ T2 ➡* T. +#L @TC_strip1 /2 width=3 by cpr_cpss_conf/ qed-. (**) (* auto /3 width=3/ fails because a δ-expansion gets in the way *) + +(* Properties on sn parallel substitution for local environments ************) + +lemma cprs_lpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #H elim H -T1 +[ #T1 #HT01 #L1 #HL01 + elim (cpr_lpss_conf_dx … HT01 … HL01) -L0 /3 width=3/ +| #T #T1 #_ #HT1 #IHT0 #L1 #HL01 + elim (IHT0 … HL01) #T2 #HT2 #HT02 + elim (cpr_lpss_conf_dx … HT1 … HL01) -L0 #T3 #HT13 #HT3 + elim (cpr_cpss_conf … HT3 … HT2) -T #T #HT3 #HT2 + lapply (cpss_trans … HT13 … HT3) -T3 + lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/ +] +qed-. + +lemma cprs_lpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L0 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cprs_lpss_conf_dx … HT01 … HL01) -HT01 #T #HT1 +lapply (lpss_cpss_trans … HL01 … HT1) -HT1 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma deleted file mode 100644 index 2682a7609..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpr.ma +++ /dev/null @@ -1,32 +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/reducibility/cpr_ltpr.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties concerning parallel unfold on terms ***************************) - -(* Basic_1: was only: pr3_subst1 *) -lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 ▶* [d, e] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 ▶* [d, e] U2. -#L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2 -[ #T2 #HT12 - elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/ -| #T #T2 #_ #HT2 * #U #HU1 #HTU - elim (cpr_tpss_ltpr … HT2 … HTU) -L1 -T // /3 width=3/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_dx.ma deleted file mode 100644 index 7f8618007..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_dx.ma +++ /dev/null @@ -1,52 +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/reducibility/cpr_ltpss_dx.ma". -include "basic_2/computation/cprs_tpss.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties concerning dx partial unfold on local environments ************) - -lemma cprs_ltpss_dx_conf: ∀L1,T,U1. L1 ⊢ T ➡* U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∃∃U2. L2 ⊢ T ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2. -#L1 #T #U1 #H @(cprs_ind … H) -U1 /2 width=3/ -#T1 #U1 #_ #HTU1 #IHT1 #L2 #d #e #HL12 -elim (IHT1 … HL12) -IHT1 #U #HTU #HT1U -elim (ltpss_dx_cpr_conf … HTU1 … HL12) -L1 #U0 #HT1U0 #HU10 -elim (cpr_tpss_conf … HT1U0 … HT1U) -T1 #U2 #HU02 #HU2 -lapply (tpss_trans_eq … HU10 HU02) -U0 /3 width=3/ -qed-. - -lemma cprs_ltpss_dx_tpss_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. L2 ⊢ T2 ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2. -#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 -elim (cprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1 -elim (cprs_tpss_conf … HT1U … HT12) -T1 #T #HUT #HT2 -lapply (tpss_trans_eq … HU1 HUT) -U /2 width=3/ -qed-. - -lemma cprs_ltpss_dx_tpss2_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∀U2. L2 ⊢ U1 ▶* [d, e] U2 → - ∃∃U. L2 ⊢ T2 ➡* U & L2 ⊢ U2 ▶* [d, e] U. -#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 #U2 #HU12 -elim (cprs_ltpss_dx_tpss_conf … HTU1 … HL12 … HT12) -L1 -T1 #U #HT2U #HU1 -elim (tpss_conf_eq … HU12 … HU1) -U1 #U0 #HU20 #HU0 -lapply (cprs_tpss_trans … HT2U … HU0) -U /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_sn.ma deleted file mode 100644 index 32009d11d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_ltpss_sn.ma +++ /dev/null @@ -1,34 +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/ltpss_sn_alt.ma". -include "basic_2/computation/cprs_ltpss_dx.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties concerning sn partial unfold on local environments ************) - -lemma cprs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → - ∀T,U1. L1 ⊢ T ➡* U1 → - ∃∃U2. L2 ⊢ T ➡* U2 & L1 ⊢ U1 ▶* [d, e] U2. -#L1 #L2 #d #e #H -lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/ -#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1 -lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1 -lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12 -elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1 -elim (cprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2 -lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 -lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tpss.ma deleted file mode 100644 index 0c575ae02..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tpss.ma +++ /dev/null @@ -1,38 +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/reducibility/cpr_tpss.ma". -include "basic_2/computation/cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) - -(* Properties on partial unfold for terms ***********************************) - -lemma cprs_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → - ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡* T2. -#L #T1 #T #H @(cprs_ind … H) -T /2 width=3/ /3 width=5/ -qed. - -lemma cprs_tps_trans: ∀L,T1,T. L ⊢ T1 ➡* T → - ∀T2,d,e. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ➡* T2. -/3 width=5 by inj, cprs_tpss_trans/ qed. (**) (* auto too slow without trace *) - -lemma cprs_tpss_conf: ∀L,T0,T1. L ⊢ T0 ➡* T1 → - ∀T2,d,e. L ⊢ T0 ▶* [d, e] T2 → - ∃∃T. L ⊢ T1 ▶* [d, e] T & L ⊢ T2 ➡* T. -#L #T0 #T1 #H @(cprs_ind … H) -T1 /2 width=3/ -#T #T1 #_ #HT1 #IHT0 #T2 #d #e #HT02 -elim (IHT0 … HT02) -T0 #T0 #HT0 #HT20 -elim (cpr_tpss_conf … HT1 … HT0) -T /3 width=5/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma index f7afb8df7..143079b0c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc.ma @@ -13,8 +13,7 @@ (**************************************************************************) include "basic_2/grammar/tstc.ma". -include "basic_2/computation/cprs_lift.ma". -include "basic_2/computation/cprs_lfprs.ma". +include "basic_2/computation/lprs_cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -32,11 +31,11 @@ lemma cprs_fwd_beta: ∀a,L,V,W,T,U. L ⊢ ⓐV. ⓛ{a}W. T ➡* U → elim (cprs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1/ | #b #V0 #W0 #T0 #HV0 #HT0 #HU - elim (cprs_inv_abst1 Abbr V … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 + elim (cprs_fwd_abst1 … HT0 Abbr V) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1 @or_intror -W @(cprs_trans … HU) -U /2 width=1/ (**) (* explicit constructor *) | #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ - elim (cprs_inv_abst1 Abbr V … HT1) -HT1 #W2 #T2 #_ #_ #H destruct + elim (cprs_fwd_abst1 … HT1 Abbr V) -HT1 #W2 #T2 #_ #_ #H destruct ] qed-. @@ -47,7 +46,7 @@ lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → #i ≃ U ∨ L ⊢ V2 ➡* U. #L #K #V1 #i #HLK #V2 #HV12 #U #H elim (cprs_inv_lref1 … H) -H /2 width=1/ -* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 #_ +* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/ qed-. @@ -72,11 +71,11 @@ elim (cprs_inv_appl1 … H) -H * @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *) elim (cprs_inv_abbr1 … HT0) -HT0 * [ #V5 #T5 #HV5 #HT5 #H destruct - lapply (cprs_lift (L.ⓓV) … HV12 … HV13 … HV34) -V1 -V3 /2 width=1/ + lapply (cprs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/ /3 width=1/ | #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct - lapply (cprs_lift (L.ⓓV0) … HV12 … HV13 … HV34) -V3 /2 width=1/ #HV24 + lapply (cprs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24 @(cprs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T @(cprs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5 @(cprs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma index 8babd61ba..46377da57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/grammar/tstc_vector.ma". -include "basic_2/substitution/lift_vector.ma". +include "basic_2/relocation/lift_vector.ma". include "basic_2/computation/cprs_tstc.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -120,11 +120,11 @@ elim (cprs_inv_appl1 … H) -H * @(cprs_trans … HU) -U elim (cprs_inv_abbr1 … HT0) -HT0 * [ #V1 #T1 #HV1 #HT1 #H destruct - lapply (cprs_lift (L.ⓓV) … HV12a … HV10a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a + lapply (cprs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a @(cprs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/ | #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct - lapply (cprs_lift (L.ⓓV0) … HV12a … HV10a … HV0a) -V0a [ /2 width=1/ ] #HV2a + lapply (cprs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a @(cprs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s @(cprs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1 @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma index 2a7f4b7b2..5dd59df28 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cnf.ma". +include "basic_2/reduction/cnf.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) @@ -69,6 +69,27 @@ qed. (* Basic forward lemmas *****************************************************) +fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V. +#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +@csn_intro #V2 #HLV2 #HV2 +@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ +qed-. + +(* Basic_1: was: sn3_gen_head *) +lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V. +/2 width=5 by csn_fwd_pair_sn_aux/ qed-. + +fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U → + ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. +#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct +@csn_intro #T2 #HLT2 #HT2 +@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +qed-. + +(* Basic_1: was: sn3_gen_bind *) +lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. +/2 width=4 by csn_fwd_bind_dx_aux/ qed-. + fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T. #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma index 109d93018..9932205f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma @@ -17,9 +17,9 @@ include "basic_2/computation/csn_tstc_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* Properties concerning atomic arity assignment ****************************) +(* Main properties concerning atomic arity assignment ***********************) -lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T. +theorem csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma deleted file mode 100644 index ccfd6015b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr.ma +++ /dev/null @@ -1,41 +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/reducibility/cpr_cpr.ma". -include "basic_2/computation/csn.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Advanced forvard lemmas **************************************************) - -fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V. -#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct -@csn_intro #V2 #HLV2 #HV2 -@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ -qed. - -(* Basic_1: was: sn3_gen_head *) -lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V. -/2 width=5/ qed. - -fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U → - ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. -#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct -@csn_intro #T2 #HLT2 #HT2 -@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ -qed. - -(* Basic_1: was: sn3_gen_bind *) -lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma deleted file mode 100644 index 70c00eb11..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_cpr_vector.ma +++ /dev/null @@ -1,26 +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/computation/csn_cpr.ma". -include "basic_2/computation/csn_vector.ma". - -(* Advanced forward lemmas **************************************************) - -lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T. -#L #T #Vs elim Vs -Vs /2 width=1/ -#V #Vs #IHVs #HVs -lapply (csn_fwd_pair_sn … HVs) #HV -lapply (csn_fwd_flat_dx … HVs) -HVs #HVs -elim (IHVs HVs) -IHVs -HVs /3 width=1/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma deleted file mode 100644 index 444dcf8f3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lfpr.ma +++ /dev/null @@ -1,147 +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/grammar/tstc_tstc.ma". -include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/csn_lift.ma". -include "basic_2/computation/csn_cpr.ma". -include "basic_2/computation/csn_alt.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Advanced properties ******************************************************) - -lemma csn_lfpr_conf: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. -#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT -@csn_intro #T0 #HLT0 #HT0 -@IHT /2 width=2/ -IHT -HT0 /2 width=3/ -qed. - -lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T. -#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 -elim (cpr_inv_abbr1 … H1) -H1 * -[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct - lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1 - lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 - elim (eq_false_inv_tpair_sn … H2) -H2 - [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ - | -IHV -HLV1 * #H destruct /3 width=1/ - ] -| -IHV -IHT -H2 #T0 #HLT0 #HT0 - lapply (csn_cpr_trans … HT … HLT0) -T #HLT0 - lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ -] -qed. - -fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → - ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) #HT -HVT -@csn_intro #X #H #H2 -elim (cpr_inv_appl1 … H) -H * -[ #V0 #Y #HLV0 #H #H0 destruct - elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_beta … H2) -H2 - [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 - @csn_abbr /2 width=3/ -HV - @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ - | -IHW -HLW0 -HV -HT * #H #HVT0 destruct - @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ - ] -| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct - lapply (lfpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3/ -HV - @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ -| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct -] -qed. - -(* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T → - L ⊢ ⬊* ⓐV. ⓛ{a}W. T. -/2 width=3/ qed. - -fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct -lapply (csn_fwd_pair_sn … HVT) #HV -lapply (csn_fwd_bind_dx … HVT) -HVT #HVT -@csn_intro #X #HL #H -elim (cpr_inv_appl1 … HL) -HL * -[ -HV #V0 #Y #HLV10 #HL #H0 destruct - elim (cpr_inv_abbr1 … HL) -HL * - [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct - lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34 - elim (lift_total V0 0 1) #V5 #HV05 - elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3)) - [ -IHVT #H0 destruct - elim (eq_false_inv_tpair_sn … H) -H - [ -HLV10 -HLV34 -HV3 -HLT3 -HVT - >(lift_inj … HV12 … HV05) -V5 - #H elim (H ?) // - | * #_ #H elim (H ?) // - ] - | -H -HVT #H - lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25 - lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3 - @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/ - ] - | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct - lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 - lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY - @(csn_cpr_trans … HVY) /2 width=1/ - ] -| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct -| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct - lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 - lapply (lfpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01 - @csn_abbr /2 width=3/ -HV - @(csn_lfpr_conf (L. ⓓW0)) /2 width=1/ -W1 - @(csn_cprs_trans … HVT) -HVT /2 width=1/ -] -qed. - -lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 → - ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. -/2 width=5/ qed. - -(* Basic_1: was only: sn3_appl_appl *) -lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. - L ⊢ ⬊* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → - 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. -#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csn_intro #X #HL #H -elim (cpr_inv_appl1_simple … HL ?) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (eq_false_inv_tpair_sn … H) -H -[ -IHT1 #HV0 - @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 - @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 - #T2 #HLT12 #HT12 - @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 - @H2T1 -H2T1 // -HLT12 /2 width=1/ -| -IHV -H1T1 -HLV0 * #H #H1T10 destruct - elim (tstc_dec T1 T0) #H2T10 - [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 - #T2 #HLT02 #HT02 - @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ - | -IHT1 -H3T1 -H1T10 - @H2T1 -H2T1 /2 width=1/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma index 4fd784d75..1919c111a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/cnf_lift.ma". +include "basic_2/reduction/cnf_lift.ma". include "basic_2/computation/acp.ma". include "basic_2/computation/csn.ma". @@ -25,7 +25,7 @@ lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬊* T2. #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 @csn_intro #T #HLT2 #HT2 -elim (cpr_inv_lift1 … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10 +elim (cpr_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct >(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/ qed. @@ -36,7 +36,7 @@ lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 → #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 @csn_intro #T #HLT2 #HT2 elim (lift_total T d e) #T0 #HT0 -lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10 +lapply (cpr_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct >(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/ qed. @@ -49,19 +49,18 @@ lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬊* V → L @csn_intro #X #H #Hi elim (cpr_inv_lref1 … H) -H [ #H destruct elim (Hi ?) // -| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 #_ +| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK @(csn_lift … HLK HV1) -HLK -HV1 - @(csn_cpr_trans … HV) -HV - @(cpr_intro … HV01) -HV01 // + @(csn_cpr_trans … HV) -HV // ] qed. lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛ{a}W. T. #a #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 -elim (cpr_inv_abst1 … H1 I V) -H1 +elim (cpr_fwd_abst1 … H1 I V) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ /3 width=5/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma new file mode 100644 index 000000000..da3337eee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpr.ma @@ -0,0 +1,141 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tstc_tstc.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/csn_alt.ma". +include "basic_2/computation/csn_lift.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* Advanced properties ******************************************************) + +lemma csn_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T. +#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT +@csn_intro #T0 #HLT0 #HT0 +@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpr_cpr_trans/ +qed. + +lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T. +#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpr_inv_abbr1 … H1) -H1 * +[ #V1 #T1 #HLV1 #HLT1 #H destruct + elim (eq_false_inv_tpair_sn … H2) -H2 + [ #HV1 @IHV // /2 width=1/ -HV1 + @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ + | -IHV -HLV1 * #H destruct /3 width=1/ + ] +| -IHV -IHT -H2 #T0 #HLT0 #HT0 + lapply (csn_cpr_trans … HT … HLT0) -T #HLT0 + lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/ +] +qed. + +fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U → + ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T. +#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) #HT -HVT +@csn_intro #X #H #H2 +elim (cpr_inv_appl1 … H) -H * +[ #V0 #Y #HLV0 #H #H0 destruct + elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_beta … H2) -H2 + [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 + @csn_abbr /2 width=3/ -HV + @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3/ + | -IHW -HLW0 -HV -HT * #H #HVT0 destruct + @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/ + ] +| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct + lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01 + @csn_abbr /2 width=3/ -HV + @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ +| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was: sn3_beta *) +lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T → + L ⊢ ⬊* ⓐV. ⓛ{a}W. T. +/2 width=3 by csn_appl_beta_aux/ qed. + +fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. +#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) -HVT #HVT +@csn_intro #X #HL #H +elim (cpr_inv_appl1 … HL) -HL * +[ -HV #V0 #Y #HLV10 #HL #H0 destruct + elim (cpr_inv_abbr1 … HL) -HL * + [ #V3 #T3 #HV3 #HLT3 #H0 destruct + elim (lift_total V0 0 1) #V4 #HV04 + elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + [ -IHVT #H0 destruct + elim (eq_false_inv_tpair_sn … H) -H + [ -HLV10 -HV3 -HLT3 -HVT + >(lift_inj … HV12 … HV04) -V4 + #H elim H // + | * #_ #H elim H // + ] + | -H -HVT #H + lapply (cpr_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24 + @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/ + ] + | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct + lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0 + lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY + @(csn_cpr_trans … HVY) /2 width=1/ + ] +| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct +| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct + lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23 + @csn_abbr /2 width=3/ -HV + @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1 + @(csn_cprs_trans … HVT) -HVT /3 width=1/ +] +qed-. + +lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 → + ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T. +/2 width=5 by csn_appl_theta_aux/ qed. + +(* Basic_1: was only: sn3_appl_appl *) +lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1. + L ⊢ ⬊* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) → + 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1. +#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csn_intro #X #HL #H +elim (cpr_inv_appl1_simple … HL ?) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (eq_false_inv_tpair_sn … H) -H +[ -IHT1 #HV0 + @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10 + @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0 + #T2 #HLT12 #HT12 + @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @H2T1 -H2T1 // -HLT12 /2 width=1/ +| -IHV -H1T1 -HLV0 * #H #H1T10 destruct + elim (tstc_dec T1 T0) #H2T10 + [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1 + #T2 #HLT02 #HT02 + @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/ + | -IHT1 -H3T1 -H1T10 + @H2T1 -H2T1 /2 width=1/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma index 81b8696b4..7ed4cb5db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma @@ -14,7 +14,7 @@ include "basic_2/computation/acp_cr.ma". include "basic_2/computation/cprs_tstc_vector.ma". -include "basic_2/computation/csn_lfpr.ma". +include "basic_2/computation/csn_lpr.ma". include "basic_2/computation/csn_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma index 7c26ef429..a0f887d6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma @@ -28,3 +28,13 @@ interpretation lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts. normalize // qed-. + +(* Basic forward lemmas *****************************************************) + +lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T. +#L #T #Vs elim Vs -Vs /2 width=1/ +#V #Vs #IHVs #HVs +lapply (csn_fwd_pair_sn … HVs) #HV +lapply (csn_fwd_flat_dx … HVs) -HVs #HVs +elim (IHVs HVs) -IHVs -HVs /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma index 4656a1595..2b3dc50cb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unwind/sstas.ma". +include "basic_2/unfold/sstas.ma". include "basic_2/computation/cprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) @@ -43,3 +43,17 @@ lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. #h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/ qed. + +lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → + L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. +/3 width=3/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 & + U2 = ⓛ{a}V2. T2. +#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2 +elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct +elim (cprs_fwd_abst1 … H2 Abst V1) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma index 57c72a7b0..80b0c7ceb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/unwind/sstas_aaa.ma". +include "basic_2/unfold/sstas_aaa.ma". include "basic_2/computation/cprs_aaa.ma". include "basic_2/computation/dxprs.ma". @@ -21,5 +21,5 @@ include "basic_2/computation/dxprs.ma". (* Properties on atomic arity assignment for terms **************************) lemma dxprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •*➡*[g] U → L ⊢ U ⁝ A. -#h #g #L #T #A #HT #U * /3 width=5/ +#h #g #L #T #A #HT #U * /3 width=5 by sstas_aaa, aaa_cprs_conf/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma index 9d051adaa..f46e256c6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/unwind/sstas_sstas.ma". -include "basic_2/computation/cprs_lfprs.ma". +include "basic_2/unfold/sstas_sstas.ma". +include "basic_2/computation/lprs_cprs.ma". include "basic_2/computation/dxprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma index eaa73f345..d9c8b5785 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma @@ -12,28 +12,12 @@ (* *) (**************************************************************************) -include "basic_2/unwind/sstas_lift.ma". +include "basic_2/unfold/sstas_lift.ma". include "basic_2/computation/cprs_lift.ma". include "basic_2/computation/dxprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) -(* Advanced inversion lemmas *************************************************) - -lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 → - ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 & - U2 = ⓛ{a}V2. T2. -#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2 -elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct -elim (cprs_inv_abst1 Abst V1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/ -qed-. - -(* Advanced properties ******************************************************) - -lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → - L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. -/3 width=3/ qed. - (* Relocation properties ****************************************************) lemma dxprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → @@ -48,5 +32,5 @@ lemma dxprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •*➡*[g] T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * #U #HU1 #HU2 elim (sstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HT1 #HTU -elim (cprs_inv_lift1 … HLK … HTU … HU2) -U -L /3 width=5/ +elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L /3 width=5/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lpss.ma new file mode 100644 index 000000000..4b1ce0785 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lpss.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/sstas_lpss.ma". +include "basic_2/computation/cprs_lpss.ma". +include "basic_2/computation/dxprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Properties about sn parallel substitution for local environments *********) + +lemma dxprs_lpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → ∀L2. L1 ⊢ ▶* L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* U2. +#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #HL12 +elim (sstas_lpss_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0 +elim (cprs_cpss_conf … HU1 … HU0) -U #U #HU1 #HU0 +elim (cprs_lpss_conf_sn … HU0 … HL12) -HU0 -HL12 #U2 #HU2 #HU02 +lapply (cpss_trans … HU1 … HU2) -U /3 width=3/ +qed-. + +lemma dxprs_cpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 → ∀T2. L ⊢ T1 ▶* T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* U2. +#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 +elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12 +elim (cprs_cpss_conf … HWU1 … HW12) -W1 /3 width=3/ +qed-. + +lemma dxprs_lpss_cpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → + ∀L2. L1 ⊢ ▶* L2 → ∀T2. L1 ⊢ T1 ▶* T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L1 ⊢ U1 ▶* U2. +#h #g #L1 #T1 #U1 #HTU1 #L2 #HL12 #T2 #HT12 +elim (dxprs_cpss_conf … HTU1 … HT12) -T1 #U2 #HTU2 #HU12 +elim (dxprs_lpss_conf … HTU2 … HL12) -HTU2 -HL12 #U #HT2U #HU2 +lapply (cpss_trans … HU12 … HU2) -U2 /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_dx.ma deleted file mode 100644 index 8e3260dd4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_dx.ma +++ /dev/null @@ -1,50 +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/unwind/sstas_ltpss_dx.ma". -include "basic_2/computation/cprs_ltpss_dx.ma". -include "basic_2/computation/dxprs.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -(* Properties about dx parallel unfold **************************************) - -lemma dxprs_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. -#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #d #e #HL12 -elim (sstas_ltpss_dx_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0 -elim (cprs_ltpss_dx_conf … HU1 … HL12) -L1 #U2 #HU2 #HU12 -elim (cprs_tpss_conf … HU2 … HU0) -U #U #HU2 #HU0 -lapply (tpss_trans_eq … HU12 HU2) -U2 /3 width=3/ -qed-. - -lemma dxprs_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 → - ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* [d, e] U2. -#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #d #e #HT12 -elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12 -elim (cprs_tpss_conf … HWU1 … HW12) -W1 /3 width=3/ -qed-. - -lemma dxprs_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & - L2 ⊢ U1 ▶* [d, e] U2. -#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 -elim (dxprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1 -elim (dxprs_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2 -lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_sn.ma deleted file mode 100644 index 553e4658b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_ltpss_sn.ma +++ /dev/null @@ -1,34 +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/ltpss_sn_alt.ma". -include "basic_2/computation/dxprs_ltpss_dx.ma". - -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) - -(* Properties about sn parallel unfold **************************************) - -lemma dxprs_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → - ∀T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → - ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* [d, e] U2. -#h #g #L1 #L2 #d #e #H -lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 [ /2 width=3/ ] -#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1 -lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1 -lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12 -elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1 -elim (dxprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2 -lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 -lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma deleted file mode 100644 index 27ea45c33..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma +++ /dev/null @@ -1,50 +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/reducibility/fpr.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) - -definition fprs: bi_relation lenv term ≝ bi_TC … fpr. - -interpretation "context-free parallel computation (closure)" - 'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. - -lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma fprs_refl: bi_reflexive … fprs. -/2 width=1/ qed. - -lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → - ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → - ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma deleted file mode 100644 index b76637ff7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_aaa.ma +++ /dev/null @@ -1,26 +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/reducibility/cfpr_aaa.ma". -include "basic_2/computation/fprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → - ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A. -#L1 #T1 #A #HT1 #L2 #T2 #HLT12 -@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma deleted file mode 100644 index 9d4d954b8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma +++ /dev/null @@ -1,138 +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/reducibility/fpr_cpr.ma". -include "basic_2/computation/cprs_lfprs.ma". -include "basic_2/computation/lfprs_ltprs.ma". -include "basic_2/computation/lfprs_fprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) - -(* Advanced properties ******************************************************) - -lemma fprs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 → - ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ➡* ⦃L2, ⓕ{I}V2.T2⦄. -#L1 #L2 #T1 #T2 #HT12 @(fprs_ind … HT12) -L2 -T2 /3 width=1/ -#L #L2 #T #T2 #_ #HT2 #IHT2 #V1 #V2 #HV12 #I -lapply (IHT2 … HV12 I) -IHT2 -HV12 /3 width=6/ -qed. - -lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ → - ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ & - U2 = -ⓑ{I}V2.T2. -#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/ -#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct -elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/ -qed-. - -lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ → - ∀d,e,L1. ⇩[d, e] L1 ≡ K1 → - ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → - ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2. -#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2 -[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 - >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/ -| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 - elim (lift_total T d e) #U #HTU - elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL - elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/ -] -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → - ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & - ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ & - L2 = K2.ⓑ{I}V2. -#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/ -#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct -elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/ -qed-. - -lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ → - ∃∃K1,V1. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & - ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ & - L1 = K1.ⓑ{I}V1. -#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/ -#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct -elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b. - ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ & - T = -ⓑ{I}V2.T2. -#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/ -#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct -elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/ -qed-. - -lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → - ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & - ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ & - L2 = K2.ⓑ{I}V2. -#I #K1 #L2 #V1 #T1 #T2 #H #b -elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct -elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/ -qed-. - -lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W. - ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ & - U2 = ⓛ{a}V2.T2. -#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/ -#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct -elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/ -qed-. - -(* Properties on context-sensitive parallel computation for terms ***********) - -lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄. -#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/ -qed. - -(* Forward lemmas on context-sensitive parallel computation for terms *******) - -lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2. -#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // -#L #L2 #T #T2 #H1 #H2 #IH1 -elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2 -lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/ -qed-. -(* -(* Advanced properties ******************************************************) - -lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → - ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄. -#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I -elim (fpr_inv_all … H) /3 width=4/ -qed. - -(* Advanced forward lemmas **************************************************) - -lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2. - ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → - ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2. -* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H -elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 -[ elim (cpr_inv_abbr1 … H) -H * - [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/ - | #T #_ #_ #H destruct - ] -| elim (cpr_inv_abst1 … H Abst V2) -H - #V #T #HV1 #_ #H destruct /3 width=4/ -] -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma deleted file mode 100644 index e0c1b3058..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_fprs.ma +++ /dev/null @@ -1,34 +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/reducibility/fpr_fpr.ma". -include "basic_2/computation/fprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) - -(* Advanced properties ******************************************************) - -lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ → - ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ → - ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄. -#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 -/2 width=4/ qed. - -(* Main propertis ***********************************************************) - -theorem fprs_conf: bi_confluent … fprs. -/2 width=4/ qed. - -theorem fprs_trans: bi_transitive … fprs. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma deleted file mode 100644 index c27e7673b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma +++ /dev/null @@ -1,53 +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/reducibility/lfpr.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -definition lfprs: relation lenv ≝ TC … lfpr. - -interpretation - "focalized parallel computation (environment)" - 'FocalizedPRedStar L1 L2 = (lfprs L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lfprs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → R L → R L2) → - ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → R L2. -#L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lfprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → R L → R L1) → - ∀L1. ⦃L1⦄ ➡* ⦃L2⦄ → R L1. -#L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lfpr_lfprs: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. -/2 width=1/ qed. - -lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄. -/2 width=1/ qed. - -lemma lfprs_strap1: ∀L1,L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. -/2 width=3/ qed. - -lemma lfprs_strap2: ∀L1,L,L2. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. -/2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_aaa.ma deleted file mode 100644 index 5c6cd31cb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_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/reducibility/lfpr_aaa.ma". -include "basic_2/computation/lfprs.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -(* Properties about atomic arity assignment on terms ************************) - -lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → L2 ⊢ T ⁝ A. -#L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma deleted file mode 100644 index 6eb25b377..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma +++ /dev/null @@ -1,30 +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/reducibility/lfpr_cpr.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/lfprs.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -(* Advanced properties ******************************************************) - -lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. -#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 -/3 width=1/ /3 width=5/ -qed. -(* -lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma deleted file mode 100644 index 940a5044d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_fprs.ma +++ /dev/null @@ -1,38 +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/reducibility/lfpr_fpr.ma". -include "basic_2/computation/fprs_fprs.ma". -include "basic_2/computation/lfprs.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -(* Inversion lemmas on context-free parallel reduction for closures *********) - -lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄. -#L1 #L2 #H @(lfprs_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL1 #T -lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/ -qed-. - -(* Properties on context-free parallel computation for closures *************) - -lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. -#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/ -qed. - -lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. -#L1 #L #L2 #T1 #T2 #HL1 #HL2 -lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 width=4/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma deleted file mode 100644 index e3866fd2e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_lfprs.ma +++ /dev/null @@ -1,40 +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/reducibility/lfpr_lfpr.ma". -include "basic_2/computation/lfprs_cprs.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -(* Advanced properties ******************************************************) - -lemma lfprs_strip: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ → - ∃∃L0. ⦃L1⦄ ➡ ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄. -/3 width=3/ qed. - -(* Main properties **********************************************************) - -theorem lfprs_conf: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → - ∃∃L0. ⦃L1⦄ ➡* ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄. -/3 width=3/ qed. - -theorem lfprs_trans: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. -/2 width=3/ qed. - -lemma lfprs_pair: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 → - ∀I. ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄. -#L1 #L2 #H @(lfprs_ind … H) -L2 /2 width=1/ -#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I -@(lfprs_trans … (L.ⓑ{I}V1)) /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma deleted file mode 100644 index 99ae801d7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_ltprs.ma +++ /dev/null @@ -1,23 +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/computation/ltprs.ma". -include "basic_2/computation/lfprs.ma". - -(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) - -(* Properties on context-free parallel computation for local environments ***) - -lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄. -/3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma new file mode 100644 index 000000000..dd290b483 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lpx_sn_tc.ma". +include "basic_2/reduction/lpr.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +definition lprs: relation lenv ≝ TC … lpr. + +interpretation "parallel computation (local environment, sn variant)" + 'PRedSnStar L1 L2 = (lprs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lprs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) → + ∀L2. L1 ⊢ ➡* L2 → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. L1 ⊢ ➡ L → L ⊢ ➡* L2 → R L → R L1) → + ∀L1. L1 ⊢ ➡* L2 → R L1. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lpr_lprs: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ➡* L2. +/2 width=1/ qed. + +lemma lprs_refl: ∀L. L ⊢ ➡* L. +/2 width=1/ qed. + +lemma lprs_strap1: ∀L1,L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lprs_strap2: ∀L1,L,L2. L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lprs_pair_refl: ∀L1,L2. L1 ⊢ ➡* L2 → ∀I,V. L1. ⓑ{I} V ⊢ ➡* L2. ⓑ{I} V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lprs_inv_atom1: ∀L2. ⋆ ⊢ ➡* L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +lemma lprs_inv_atom2: ∀L1. L1 ⊢ ➡* ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lprs_fwd_length: ∀L1,L2. L1 ⊢ ➡* L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma new file mode 100644 index 000000000..c5b653092 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_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/reduction/lpr_aaa.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. +#L1 #T #A #HT #L2 #HL12 +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3 by aaa_lpr_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma new file mode 100644 index 000000000..3a7475d0a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs_cprs.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* alternative definition *) +definition lprsa: relation lenv ≝ lpx_sn … cprs. + +interpretation "parallel computation (local environment, sn variant) alternative" + 'PRedSnStarAlt L1 L2 = (lprsa L1 L2). + +(* Main properties on the alternative definition **********************************) + +theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2. +/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. + +(* Main inversion lemmas on the alternative definition ****************************) + +theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2. +/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-. + +(* Alternative eliminators ********************************************************) + +lemma lprs_ind_alt: ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + K1 ⊢ ➡* K2 → K1 ⊢ V1 ➡* V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. L1 ⊢ ➡* L2 → R L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma new file mode 100644 index 000000000..4608d1b73 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma @@ -0,0 +1,110 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs_cprs.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Advanced properties ******************************************************) + +lemma lprs_pair: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L1 ⊢ V1 ➡* V2 → + L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. +/2 width=1 by TC_lpx_sn_pair/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ⊢ ➡* L2 → + ∃∃K2,V2. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L2 = K2. ⓑ{I} V2. +/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-. + +lemma lprs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➡* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L1 = K1. ⓑ{I} V1. +/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-. + +(* Properties on context-sensitive parallel computation for terms ***********) + +lemma lprs_cpr_trans: s_r_trans … cpr lprs. +/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-. + +(* Basic_1: was just: pr3_pr3_pr3_t *) +lemma lprs_cprs_trans: s_rs_trans … cpr lprs. +/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-. + +lemma lprs_cprs_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 → + ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #HT01 #L1 #H elim H -L1 +[ #L1 #HL01 + elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3/ +| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0 + elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12 + elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03 + elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3 + lapply (cprs_trans … HT03 … HT3) -T3 + lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3/ +] +qed-. + +lemma lprs_cpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 → + ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-. + +lemma lprs_cprs_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 → + ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1 +lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3/ +qed-. + +lemma lprs_cpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 → + ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T. +/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-. + +lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 +lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/ +qed. + +(* Inversion lemmas on context-sensitive parallel computation for terms *****) + +(* Basic_1: was pr3_gen_abbr *) +lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1.T1 ➡* U2 → ( + ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & + U2 = ⓓ{a}V2.T2 + ) ∨ + ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true. +#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02 + lapply (cprs_strap1 … HV10 … HV02) -V0 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5/ + | #T2 #HT02 #HUT2 + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02 + lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/ + ] +| #U1 #HTU1 #HU01 + elim (lift_total U2 0 1) #U #HU2 + lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/ +] +qed-. + +(* More advanced properties *************************************************) + +lemma lprs_pair2: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. +/3 width=3 by lprs_pair, lprs_cprs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma new file mode 100644 index 000000000..73c9281e6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpr_ldrop.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Properies on local environment slicing ***********************************) + +lemma lprs_ldrop_conf: dropable_sn lprs. +/3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-. + +lemma ldrop_lprs_trans: dedropable_sn lprs. +/3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-. + +lemma lprs_ldrop_trans_O1: dropable_dx lprs. +/3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma new file mode 100644 index 000000000..7ef78d271 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpr_lpr.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Advanced properties ******************************************************) + +lemma lprs_strip: confluent2 … lprs lpr. +/3 width=3 by TC_strip1, lpr_conf/ qed-. + +(* Main properties **********************************************************) + +theorem lprs_conf: confluent2 … lprs lprs. +/3 width=3 by TC_confluent2, lpr_conf/ qed-. + +theorem lfprs_trans: Transitive … lprs. +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lpss.ma new file mode 100644 index 000000000..ed9e7d061 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lpss.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpr_lpss.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Properties on sn parallel substitution on local environments *************) + +lemma lprs_lpss_conf: confluent2 … lprs lpss. +/3 width=3 by TC_strip1, lpr_lpss_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma deleted file mode 100644 index 8e0c32e26..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma +++ /dev/null @@ -1,90 +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/reducibility/ltpr.ma". -include "basic_2/computation/tprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) - -definition ltprs: relation lenv ≝ TC … ltpr. - -interpretation - "context-free parallel computation (environment)" - 'PRedStar L1 L2 = (ltprs L1 L2). - -(* Basic eliminators ********************************************************) - -lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 → - (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) → - ∀L2. L1 ➡* L2 → R L2. -#L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → - (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) → - ∀L1. L1 ➡* L2 → R L1. -#L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma ltprs_refl: reflexive … ltprs. -/2 width=1/ qed. - -lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2. -/2 width=1/ qed. - -lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2. -/2 width=3/ qed. - -lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2. -/2 width=3/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆. -#L2 #H @(ltprs_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL1 destruct ->(ltpr_inv_atom1 … HL2) -L2 // -qed-. - -lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 → - ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2. -#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/ -#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/ -qed-. - -lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆. -#L1 #H @(ltprs_ind_dx … H) -L1 // -#L1 #L #HL1 #_ #IHL2 destruct ->(ltpr_inv_atom2 … HL1) -L1 // -qed-. - -lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1. -#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/ -#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct -elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|. -#L1 #L2 #H @(ltprs_ind … H) -L2 // -#L #L2 #_ #HL2 #IHL1 ->IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma deleted file mode 100644 index 7d532c973..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_alt.ma +++ /dev/null @@ -1,34 +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/computation/ltprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) - -(* alternative definition of ltprs *) -definition ltprsa: relation lenv ≝ lpx tprs. - -interpretation - "context-free parallel computation (environment) alternative" - 'PRedStarAlt L1 L2 = (ltprsa L1 L2). - -(* Basic properties *********************************************************) - -lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2. -/2 width=1/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2. -/2 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma deleted file mode 100644 index a7c320089..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ldrop.ma +++ /dev/null @@ -1,27 +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/reducibility/ltpr_ldrop.ma". -include "basic_2/computation/ltprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) - -lemma ltprs_ldrop_conf: dropable_sn ltprs. -/2 width=3/ qed. - -lemma ldrop_ltprs_trans: dedropable_sn ltprs. -/2 width=3/ qed. - -lemma ltprs_ldrop_trans_O1: dropable_dx ltprs. -/2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma deleted file mode 100644 index 7ededf2af..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma +++ /dev/null @@ -1,32 +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/reducibility/ltpr_ltpr.ma". -include "basic_2/computation/ltprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) - -(* Advanced properties ******************************************************) - -lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 → - ∃∃L0. L1 ➡ L0 & L2 ➡* L0. -/3 width=3/ qed. - -(* Main properties **********************************************************) - -theorem ltprs_conf: confluent … ltprs. -/3 width=3/ qed. - -theorem ltprs_trans: Transitive … ltprs. -/2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma deleted file mode 100644 index 22f09eda0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma +++ /dev/null @@ -1,90 +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/reducibility/tpr.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) - -(* Basic_1: includes: pr1_pr0 *) -definition tprs: relation term ≝ TC … tpr. - -interpretation "context-free parallel computation (term)" - 'PRedStar T1 T2 = (tprs T1 T2). - -(* Basic eliminators ********************************************************) - -lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 → - (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) → - ∀T2. T1 ➡* T2 → R T2. -#T1 #R #HT1 #IHT1 #T2 #HT12 -@(TC_star_ind … HT1 IHT1 … HT12) // -qed-. - -lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 → - (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) → - ∀T1. T1 ➡* T2 → R T1. -#T2 #R #HT2 #IHT2 #T1 #HT12 -@(TC_star_ind_dx … HT2 IHT2 … HT12) // -qed-. - -(* Basic properties *********************************************************) - -lemma tprs_refl: reflexive … tprs. -/2 width=1/ qed. - -lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2. -/2 width=1/ qed. - -lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2. -/2 width=3/ qed. - -lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2. -/2 width=3/ qed. - -(* Basic_1: was only: pr1_head_1 *) -lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 → - ②{I} V1. T1 ➡* ②{I} V2. T2. -* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2 -[1,3: /3 width=1/ -|2,4: #V #V2 #_ #HV2 #IHV1 - @(tprs_strap1 … IHV1) -IHV1 /2 width=1/ -] -qed. - -(* Basic_1: was only: pr1_head_2 *) -lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 → - ②{I} V1. T1 ➡* ②{I} V2. T2. -* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2 -[1,3: /3 width=1/ -|2,4: #T #T2 #_ #HT2 #IHT1 - @(tprs_strap1 … IHT1) -IHT1 /2 width=1/ -] -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k. -#U2 #k #H @(tprs_ind … H) -U2 // -#U #U2 #_ #HU2 #IHU1 destruct ->(tpr_inv_atom1 … HU2) -HU2 // -qed-. - -lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨ - ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2. -#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/ -#U #U2 #_ #HU2 * /3 width=3/ * -#W #T #HW1 #HT1 #H destruct -elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ * -#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma deleted file mode 100644 index d0d173470..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_lift.ma +++ /dev/null @@ -1,43 +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/reducibility/tpr_lift.ma". -include "basic_2/computation/tprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) - -(* Advanced inversion lemmas ************************************************) - -lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 → - ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2. -#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/ -#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ -qed-. - -lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → - V1 ➡* V2 ∧ T1 ➡* T2. -#a #V1 #V2 #T1 #T2 #H -elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ -qed-. - -(* Relocation properties ****************************************************) - -(* Note: this was missing in basic_1 *) -lemma tprs_lift: t_liftable tprs. -/3 width=7/ qed. - -(* Note: this was missing in basic_1 *) -lemma tprs_inv_lift1: t_deliftable_sn tprs. -/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma deleted file mode 100644 index 87a4a71ab..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma +++ /dev/null @@ -1,43 +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/reducibility/tpr_tpr.ma". -include "basic_2/computation/tprs.ma". - -(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) - -(* Advanced properties ******************************************************) - -(* Basic_1: was: pr1_strip *) -lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 → - ∃∃T0. T1 ➡ T0 & T2 ➡* T0. -/3 width=3 by TC_strip1, tpr_conf/ qed. - -(* Main propertis ***********************************************************) - -(* Basic_1: was: pr1_confluence *) -theorem tprs_conf: confluent … tprs. -/3 width=3/ qed. - -(* Basic_1: was: pr1_t *) -theorem tprs_trans: Transitive … tprs. -/2 width=3/ qed. - -(* Basic_1: was: pr1_comp *) -lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 → - ②{I} V1. T1 ➡* ②{I} V2. T2. -#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/ -#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 -@(tprs_trans … (②{I}V.T2)) /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_dx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_dx.etc new file mode 100644 index 000000000..7f8618007 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_dx.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr_ltpss_dx.ma". +include "basic_2/computation/cprs_tpss.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning dx partial unfold on local environments ************) + +lemma cprs_ltpss_dx_conf: ∀L1,T,U1. L1 ⊢ T ➡* U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∃∃U2. L2 ⊢ T ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2. +#L1 #T #U1 #H @(cprs_ind … H) -U1 /2 width=3/ +#T1 #U1 #_ #HTU1 #IHT1 #L2 #d #e #HL12 +elim (IHT1 … HL12) -IHT1 #U #HTU #HT1U +elim (ltpss_dx_cpr_conf … HTU1 … HL12) -L1 #U0 #HT1U0 #HU10 +elim (cpr_tpss_conf … HT1U0 … HT1U) -T1 #U2 #HU02 #HU2 +lapply (tpss_trans_eq … HU10 HU02) -U0 /3 width=3/ +qed-. + +lemma cprs_ltpss_dx_tpss_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. L2 ⊢ T2 ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2. +#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 +elim (cprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1 +elim (cprs_tpss_conf … HT1U … HT12) -T1 #T #HUT #HT2 +lapply (tpss_trans_eq … HU1 HUT) -U /2 width=3/ +qed-. + +lemma cprs_ltpss_dx_tpss2_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∀U2. L2 ⊢ U1 ▶* [d, e] U2 → + ∃∃U. L2 ⊢ T2 ➡* U & L2 ⊢ U2 ▶* [d, e] U. +#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 #U2 #HU12 +elim (cprs_ltpss_dx_tpss_conf … HTU1 … HL12 … HT12) -L1 -T1 #U #HT2U #HU1 +elim (tpss_conf_eq … HU12 … HU1) -U1 #U0 #HU20 #HU0 +lapply (cprs_tpss_trans … HT2U … HU0) -U /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_sn.etc new file mode 100644 index 000000000..32009d11d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cprs_ltpss_sn.etc @@ -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/unfold/ltpss_sn_alt.ma". +include "basic_2/computation/cprs_ltpss_dx.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning sn partial unfold on local environments ************) + +lemma cprs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T,U1. L1 ⊢ T ➡* U1 → + ∃∃U2. L2 ⊢ T ➡* U2 & L1 ⊢ U1 ▶* [d, e] U2. +#L1 #L2 #d #e #H +lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/ +#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1 +lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1 +lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12 +elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1 +elim (cprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2 +lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 +lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_dx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_dx.etc new file mode 100644 index 000000000..8e3260dd4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_dx.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/sstas_ltpss_dx.ma". +include "basic_2/computation/cprs_ltpss_dx.ma". +include "basic_2/computation/dxprs.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Properties about dx parallel unfold **************************************) + +lemma dxprs_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #d #e #HL12 +elim (sstas_ltpss_dx_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0 +elim (cprs_ltpss_dx_conf … HU1 … HL12) -L1 #U2 #HU2 #HU12 +elim (cprs_tpss_conf … HU2 … HU0) -U #U #HU2 #HU0 +lapply (tpss_trans_eq … HU12 HU2) -U2 /3 width=3/ +qed-. + +lemma dxprs_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #d #e #HT12 +elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12 +elim (cprs_tpss_conf … HWU1 … HW12) -W1 /3 width=3/ +qed-. + +lemma dxprs_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & + L2 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 +elim (dxprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1 +elim (dxprs_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2 +lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_sn.etc new file mode 100644 index 000000000..553e4658b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/dxprs_ltpss_sn.etc @@ -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/unfold/ltpss_sn_alt.ma". +include "basic_2/computation/dxprs_ltpss_dx.ma". + +(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) + +(* Properties about sn parallel unfold **************************************) + +lemma dxprs_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → + ∀T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #L2 #d #e #H +lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 [ /2 width=3/ ] +#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1 +lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1 +lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12 +elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1 +elim (dxprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2 +lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 +lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma index 328dc55a6..cbb1ed010 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma @@ -24,10 +24,7 @@ inductive simple: predicate term ≝ interpretation "simple (term)" 'Simple T = (simple T). (* Basic inversion lemmas ***************************************************) -(* -lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥. -/3 width=1/ qed. -*) + fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U → ⊥. #T * -T [ #I #a #J #W #U #H destruct @@ -36,7 +33,7 @@ fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U qed. lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥. -/2 width=7/ qed-. (**) (* auto fails if mt is enabled *) +/2 width=7/ qed-. lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. * /2 width=2/ #a #I #V #T #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index 421cc97de..329958fb6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -16,7 +16,7 @@ include "basic_2/unfold/cpqs.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) -(* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx pr2_head_1 *) +(* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx *) (* Note: cpr_flat: does not hold in basic_1 *) inductive cpr: lenv → relation term ≝ | cpr_atom : ∀I,L. cpr L (⓪{I}) (⓪{I}) @@ -73,6 +73,11 @@ lemma cpss_cpr: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➡ T2. lemma cpr_refl: ∀T,L. L ⊢ T ➡ T. /2 width=1/ qed. +(* Basic_1: was: pr2_head_1 *) +lemma cpr_pair_sn: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → + ∀T. L⊢ ②{I}V1.T ➡ ②{I}V2.T. +* /2 width=1/ qed. + lemma cpr_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) → ∃∃T2,T. L ⊢ T1 ➡ T2 & ⇧[d, 1] T ≡ T2. #L #K #V #T1 #d #HLK @@ -321,13 +326,12 @@ lemma cpr_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➡ T → ] qed-. -(* Basic_1: removed theorems 12: +(* Basic_1: removed theorems 11: pr0_subst0_back pr0_subst0_fwd pr0_subst0 pr2_head_2 pr2_cflat clear_pr2_trans pr2_gen_csort pr2_gen_cflat pr2_gen_cbind - pr2_subst1 pr2_gen_ctail pr2_ctail -*) +*) (* Basic_1: removed local theorems 4: pr0_delta_tau pr0_cong_delta pr2_free_free pr2_free_delta diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index d11e148d1..f9a63718a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -220,7 +220,8 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ #HU2 elim (cpr_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ - elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 /4 width=7/ + elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 + /4 width=7 by cpr_bind, cpr_flat, cpr_theta, ex2_intro/ (**) (* timeout=35 *) | #T1 #HT01 #HXT1 #H destruct elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 /2 width=1/ #Y #HYT #HXY @@ -268,7 +269,8 @@ elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 elim (lift_total V 0 1) #U #HVU lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1/ -lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ /4 width=7/ +lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ +/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* timeout 40 *) qed-. theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma index 6ea796b9a..060f21648 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpss.ma @@ -248,6 +248,7 @@ lemma cpr_cpss_conf_lpr_lpss: lpx_sn_confluent cpr cpss. qed-. (* Basic_1: includes: pr0_subst1 *) +(* Basic_1: was: pr2_subst1 *) lemma cpr_cpss_conf: ∀L. confluent2 … (cpr L) (cpss L). /2 width=6 by cpr_cpss_conf_lpr_lpss/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma index a7a4dbde4..e2a52aeef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma @@ -73,21 +73,21 @@ qed-. (* (* Advanced inversion lemmas on plus-iterated supclosure ********************) -lemma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ → +lamma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃L2, T2⦄. #b #J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2 [ #L2 #T2 #H elim (fsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/ | #L #T #L2 #T2 #_ #HT2 * /3 width=4/ ] -qed-. +qad-. -lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ → +lamma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ → ⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⊃* ⦃L2, T2⦄. #J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2 [ #L2 #T2 #H elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ | #L #T #L2 #T2 #_ #HT2 * /3 width=4/ ] -qed-. +qad-. *) 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 a9ccf6682..21fd5fcca 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 @@ -81,13 +81,8 @@ table { ] class "cyan" [ { "computation" * } { - [ { "focalized computation" * } { - [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ] - [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] - } - ] [ { "decomposed extended computation" * } { - [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxprs_dxprs" * ] + [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ] } ] [ { "weakly normalizing computation" * } { @@ -95,13 +90,13 @@ table { } ] [ { "strongly normalizing computation" * } { - [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ] - [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ] + [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_tstc_vector" + "csn_aaa" * ] + [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpr" * ] } ] [ { "context-sensitive computation" * } { - [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ] - [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ] + [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ] + [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_tstc" + "cprs_tstc_vector" + "cprs_lift" + "cprs_lpss" + "cprs_aaa" + "cprs_cprs" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } {