From b6a8600c3c4381809f1ab8d3e28628e17d9c3d3d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 28 Nov 2012 14:33:17 +0000
Subject: [PATCH] - relations.ma:   we introduced the reflexive closure (RC)
 for use in lambda and lambda_delta - lambda:   we introduced pointers to
 redexes   notation bug fix in delifting_substitution.ma

---
 .../contribs/lambda/delifting_substitution.ma | 54 +++++++++----------
 matita/matita/contribs/lambda/preamble.ma     |  2 +
 .../matita/contribs/lambda/redex_pointer.ma   | 51 ++++++++++++++++++
 matita/matita/lib/basics/relations.ma         |  8 +++
 4 files changed, 88 insertions(+), 27 deletions(-)
 create mode 100644 matita/matita/contribs/lambda/redex_pointer.ma

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index 344ad8490..3d4c2150b 100644
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -17,39 +17,39 @@ include "lift.ma".
 (* DELIFTING SUBSTITUTION ***************************************************)
 
 (* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst C d M on M ≝ match M with
-[ VRef i   ⇒ tri … i d (#i) (↑[i] C) (#(i-1))
-| Abst A   ⇒ 𝛌. (dsubst C (d+1) A)
-| Appl B A ⇒ @ (dsubst C d B). (dsubst C d A)
+let rec dsubst D d M on M ≝ match M with
+[ VRef i   ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
+| Abst A   ⇒ 𝛌. (dsubst D (d+1) A)
+| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
 ].
 
 interpretation "delifting substitution"
-   'DSubst C d M = (dsubst C d M).
+   'DSubst D d M = (dsubst D d M).
 
 (* Note: the notation with "/" does not work *)
-notation "hvbox( [ term 46 d ⬐ break term 46 C ] break term 46 M )"
+notation "hvbox( [ term 46 d ⬐ break term 46 D ] break term 46 M )"
    non associative with precedence 46
-   for @{ 'DSubst $C $d $M }.
+   for @{ 'DSubst $D $d $M }.
 
-notation > "hvbox( [ ⬐ term 46 C ] break term 46 M )"
+notation > "hvbox( [ ⬐ term 46 D ] break term 46 M )"
    non associative with precedence 46
-   for @{ 'DSubst $C 0 $M }.
+   for @{ 'DSubst $D 0 $M }.
 
-lemma dsubst_vref_lt: ∀i,d,C. i < d → [d ⬐ C] #i = #i.
+lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ⬐ D] #i = #i.
 normalize /2 width=1/
 qed.
 
-lemma dsubst_vref_eq: ∀d,C. [d ⬐ C] #d = ↑[d]C.
+lemma dsubst_vref_eq: ∀d,D. [d ⬐ D] #d = ↑[d]D.
 normalize //
 qed.
 
-lemma dsubst_vref_gt: ∀i,d,C. d < i → [d ⬐ C] #i = #(i-1).
+lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ⬐ D] #i = #(i-1).
 normalize /2 width=1/
 qed.
 
-theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 →
-                        [d2 ⬐ ↑[d1 - d2, h] C] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ C] M.
-#h #C #M elim M -M
+theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
+                        [d2 ⬐ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ D] M.
+#h #D #M elim M -M
 [ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
     >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
@@ -67,9 +67,9 @@ theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 →
 ]
 qed.
 
-theorem dsubst_lift_be: ∀h,C,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
-                        [d2 ⬐ C] ↑[d1, h + 1] M = ↑[d1, h] M.
-#h #C #M elim M -M
+theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+                        [d2 ⬐ D] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #D #M elim M -M
 [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
@@ -84,9 +84,9 @@ theorem dsubst_lift_be: ∀h,C,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
 ]
 qed.
 
-theorem dsubst_lift_ge: ∀h,C,M,d1,d2. d1 + h ≤ d2 →
-                        [d2 ⬐ C] ↑[d1, h] M = ↑[d1, h] [d2 - h ⬐ C] M.
-#h #C #M elim M -M
+theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
+                        [d2 ⬐ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ⬐ D] M.
+#h #D #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
   [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
     [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
@@ -111,9 +111,9 @@ theorem dsubst_lift_ge: ∀h,C,M,d1,d2. d1 + h ≤ d2 →
 ]
 qed.
 
-theorem subst_subst_ge: ∀C1,C2,M,d1,d2. d1 ≤ d2 →
-                        [d2 ⬐ C2] [d1 ⬐ C1] M = [d1 ⬐ [d2 - d1 ⬐ C2] C1] [d2 + 1 ⬐ C2] M.
-#C1 #C2 #M elim M -M
+theorem subst_subst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
+                        [d2 ⬐ D2] [d1 ⬐ D1] M = [d1 ⬐ [d2 - d1 ⬐ D2] D1] [d2 + 1 ⬐ D2] M.
+#D1 #D2 #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
     >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
@@ -134,9 +134,9 @@ theorem subst_subst_ge: ∀C1,C2,M,d1,d2. d1 ≤ d2 →
 ]
 qed.
 
-theorem subst_subst_lt: ∀C1,C2,M,d1,d2. d2 < d1 →
-                        [d2 ⬐ [d1 - d2 -1 ⬐ C1] C2] [d1 ⬐ C1] M = [d1 - 1 ⬐ C1] [d2 ⬐ C2] M.
-#C1 #C2 #M #d1 #d2 #Hd21
+theorem subst_subst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
+                        [d2 ⬐ [d1 - d2 -1 ⬐ D1] D2] [d1 ⬐ D1] M = [d1 - 1 ⬐ D1] [d2 ⬐ D2] M.
+#D1 #D2 #M #d1 #d2 #Hd21
 lapply (ltn_to_ltO … Hd21) #Hd1
 >subst_subst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
 qed.
diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index afaacb5f2..fa36983af 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/star.ma".
+include "basics/lists/list.ma".
 include "arithmetics/nat.ma".
 
 include "xoa_notation.ma".
diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
new file mode 100644
index 000000000..dbc8efe48
--- /dev/null
+++ b/matita/matita/contribs/lambda/redex_pointer.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "term.ma".
+
+(* REDEX POINTER ************************************************************)
+
+(* Policy: boolean metavariables: a, b
+           pointer metavariables: p, q
+*)
+(* Note: this is a path in the tree representation of a term
+         in which abstraction nodes are omitted;
+         on application nodes, "false" means "proceed left"
+         and "true" means "proceed right"
+*)
+definition rpointer: Type[0] ≝ list bool.
+
+(* Note: precedence relation on redex pointers: p ≺ q
+         to serve as base for the order relations: p < q and p ≤ q *)
+inductive rpprec: relation rpointer ≝
+| rpprec_nil : ∀b,q.   rpprec ([]) (b::q)
+| rppprc_cons: ∀p,q.   rpprec (false::p) (true::q)
+| rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
+.
+
+interpretation "'precedes' on redex pointers"
+   'prec p q = (rpprec p q).
+
+(* Note: this should go to core_notation *)
+notation "hvbox(a break ≺ b)"
+   non associative with precedence 45
+   for @{ 'prec $a $b }.
+
+(* Note: this is p < q *)
+interpretation "'less than' on redex pointers"
+   'lt p q = (TC rpointer rpprec p q).
+
+(* Note: this is p ≤ q, that *really* is p < q ∨ p = q *)
+interpretation "'less or equal to' on redex pointers"
+   'leq x y = (RC rpointer (TC rpointer rpprec) x y).
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index f469ddca2..ed5130955 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -48,6 +48,14 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop
 definition antisymmetric: ∀A.∀R:relation A.Prop
 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
 
+(* Reflexive closure ************)
+
+definition RC: ∀A:Type[0]. relation A → relation A ≝
+               λA,R,x,y. R … x y ∨ x = y.
+
+lemma RC_reflexive: ∀A,R. reflexive A (RC … R).
+/2 width=1/ qed.
+
 (********** operations **********)
 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
   ∃am.R1 a1 am ∧ R2 am a2.
-- 
2.39.2