X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fredex_pointer.ma;h=5746787c53acb0739b62192d7818628eab8b50f9;hb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;hp=f6e05c93fa740e664bad3e766e73cde027eb232d;hpb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;p=helm.git

diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
index f6e05c93f..5746787c5 100644
--- a/matita/matita/contribs/lambda/redex_pointer.ma
+++ b/matita/matita/contribs/lambda/redex_pointer.ma
@@ -24,15 +24,19 @@ include "term.ma".
          on application nodes, "false" means "proceed right"
          and "true" means "proceed left"
 *)
-definition rpointer: Type[0] ≝ list bool.
+definition rptr: Type[0] ≝ list bool.
+
+(* Note: a redex is "in the spine" when is not in the argument of an application *)
+definition in_spine: predicate rptr ≝ λp.
+                     All … is_false p.
 
 (* 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 ≝
+inductive rpprec: relation rptr ≝
 | 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)
-| rpprec_skip: ∀p,q.   rpprec (false::p) q → rpprec p q
+| rpprec_skip:         rpprec (false::◊) ◊
 .
 
 interpretation "'precedes' on redex pointers"
@@ -44,9 +48,29 @@ notation "hvbox(a break ≺ b)"
    for @{ 'prec $a $b }.
 
 (* Note: this is p < q *)
+definition rplt: relation rptr ≝ TC … rpprec.
+
 interpretation "'less than' on redex pointers"
-   'lt p q = (TC rpointer rpprec p q).
+   'lt p q = (rplt p q).
+
+(* Note: this is p ≤ q *)
+definition rple: relation rptr ≝ star … rpprec.
 
-(* 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).
+   'leq p q = (rple p q).
+
+lemma rpprec_rple: ∀p,q. p ≺ q → p ≤ q.
+/2 width=1/
+qed.
+
+lemma rple_false: false::◊ ≤ ◊.
+/2 width=1/
+qed.
+
+lemma rple_nil: ∀p. ◊ ≤ p.
+* // /2 width=1/
+qed.
+
+lemma rple_comp: ∀p1,p2. p1 ≤ p2 → ∀b. (b::p1) ≤ (b::p2).
+#p1 #p2 #H elim H -p2 // /3 width=3/
+qed.