- we enabled a notation for ex2

[helm.git] / matita / matita / contribs / lambda / redex_pointer.ma

diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
index dbc8efe481e76951ed06e1d713d87eb864c58acc..5746787c53acb0739b62192d7818628eab8b50f9 100644 (file)
--- a/matita/matita/contribs/lambda/redex_pointer.ma
+++ b/matita/matita/contribs/lambda/redex_pointer.ma
@@ -21,17 +21,22 @@ include "term.ma".
 *)
 (* 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"
+         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 ≝
-| rpprec_nil : ∀b,q.   rpprec ([]) (b::q)
+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:         rpprec (false::◊) ◊
 .
 
 interpretation "'precedes' on redex pointers"
@@ -43,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.