*)
(* 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"
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.