From 55472556fddad19323a80bda2ff8d9e6dc8a8f38 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 25 Oct 2011 12:21:04 +0000 Subject: [PATCH] old pr2_subst1 (Basic-1) closed! --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 2 +- .../lambda_delta/Basic_2/reduction/cpr.ma | 2 - .../Basic_2/reduction/cpr_ltpr.ma | 47 +++++++++++++++++++ .../lambda_delta/Basic_2/reduction/ltpr.ma | 6 +++ .../Basic_2/reduction/tpr_tpss.ma | 4 +- 5 files changed, 57 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index b45870449..f8c868a71 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -265,13 +265,13 @@ pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta pr2/clen pr2_gen_ctail +pr2/subst1 pr2_gen_cabbr # check ###################################################################### pr2/fwd pr2_gen_void pr2/props pr2_ctail - # waiting #################################################################### pr3/fwd pr3_gen_sort diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma index 3d1280a65..e70b9c537 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma @@ -93,6 +93,4 @@ qed. (* pr2/fwd pr2_gen_appl pr2/fwd pr2_gen_abbr -pr2/subst1 pr2_subst1 -pr2/subst1 pr2_gen_cabbr *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma new file mode 100644 index 000000000..3f80fb59c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_ltpr.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpr_tpss.ma". +include "Basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Unfold properties ********************************************************) + +(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *) + +(* Basic_1: was only: pr2_subst1 *) +lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 → + ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → + ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. +#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1 +elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU +elim (tpss_conf_eq … HT2 … HTU) -T /3/ +qed. + +lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 → + ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T. +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +>(ltpr_fwd_length … HL12) in HT2 #HT2 +elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/ +qed. + +lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 → + ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → + ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2. +#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 +elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 +elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2 +lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma index 9cbd3d6c8..b7a01f3df 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/ltpr.ma @@ -80,4 +80,10 @@ lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 → ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. /2/ qed. +(* Basic forward lemmas *****************************************************) + +lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|. +#L1 #L2 #H elim H -H L1 L2; normalize // +qed. + (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma index 9aaf5c423..30d7a4bb8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/tpr_tpss.ma @@ -17,6 +17,8 @@ include "Basic_2/reduction/ltpr_ldrop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) +(* Unfold properties ********************************************************) + (* Basic_1: was: pr0_subst1 *) lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → @@ -89,4 +91,4 @@ lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 → elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2 lapply (tpss_trans_eq … HT2 … HTU2) -T /2/ ] -qed. \ No newline at end of file +qed. -- 2.39.2