- tentative definition of lcpr (contex-sensitive parallel reduction on

local environments)
- some refactoring

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
index d4302a32a8b6d350aff395297974666ec774a62c..d4dd5a5de69b5e24dfddf9e47fe6a5ffe6bfe1be 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma
@@ -79,3 +79,7 @@ notation "hvbox( T1 ⇒ break T2 )"
 notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
    non associative with precedence 45
    for @{ 'PRed $L $T1 $T2 }.
+
+notation "hvbox( L1 ⊢ ⇒ break L2 )"
+   non associative with precedence 45
+   for @{ 'CPRed $L1 $L2 }.

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma
new file mode 100644 (file)
index 0000000..1b19df7
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+inductive lcpr: lenv → lenv → Prop ≝
+| lcpr_sort: lcpr (⋆) (⋆)
+| lcpr_item: ∀K1,K2,I,V1,V2.
+             lcpr K1 K2 → K1 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+  "context-sensitive parallel reduction (environment)"
+  'CPRed L1 L2 = (lcpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+                          ∃∃K2,V2. K1 ⊢ ⇒ K2 & K1 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 * -L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+lemma lcpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⊢ ⇒ L2 →
+                      ∃∃K2,V2. K1 ⊢ ⇒ K2 & K1 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/2/ qed.

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.ma
deleted file mode 100644 (file)
index a08a653..0000000
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lpr.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/reduction/tpr.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-inductive lpr: lenv → lenv → Prop ≝
-| lpr_sort: lpr (⋆) (⋆)
-| lpr_item: ∀K1,K2,I,V1,V2.
-            lpr K1 K2 → V1 ⇒ V2 → lpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
-.
-
-interpretation
-  "context-free parallel reduction (environment)"
-  'PRed L1 L2 = (lpr L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
-                         ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 * -L1 L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
-]
-qed.
-
-lemma lpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
-                     ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-/2/ 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
new file mode 100644 (file)
index 0000000..ac3ff7b
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+inductive ltpr: lenv → lenv → Prop ≝
+| ltpr_sort: ltpr (⋆) (⋆)
+| ltpr_item: ∀K1,K2,I,V1,V2.
+             ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+  "context-free parallel reduction (environment)"
+  'PRed L1 L2 = (ltpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+                          ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 * -L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+lemma ltpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
+                      ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/2/ qed.

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
index 6fae790d80e23ed26bb728d13ea625d6696561e6..3a00c62c6b98a298ffb6ed1952f40bbdae09d769 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic-2/reduction/lpr.ma".
+include "Basic-2/reduction/ltpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
-axiom tpr_tps_lpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
-                   ∀d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
-                   ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2.
+axiom tpr_tps_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
+                    ∀d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
+                    ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2.
 
 lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
                     ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →