From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 25 Oct 2011 12:21:04 +0000 (+0000)
Subject: old pr2_subst1 (Basic-1) closed!
X-Git-Tag: make_still_working~2158
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55472556fddad19323a80bda2ff8d9e6dc8a8f38;p=helm.git

old pr2_subst1 (Basic-1) closed!
---

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.