1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 (* REDEX POINTER ************************************************************)
19 (* Policy: boolean metavariables: a, b
20 pointer metavariables: p, q
22 (* Note: this is a path in the tree representation of a term
23 in which abstraction nodes are omitted;
24 on application nodes, "false" means "proceed right"
25 and "true" means "proceed left"
27 definition rptr: Type[0] ≝ list bool.
29 (* Note: a redex is "in the spine" when is not in the argument of an application *)
30 definition in_spine: predicate rptr ≝ λp.
33 (* Note: precedence relation on redex pointers: p ≺ q
34 to serve as base for the order relations: p < q and p ≤ q *)
35 inductive rpprec: relation rptr ≝
36 | rpprec_nil : ∀b,q. rpprec (◊) (b::q)
37 | rppprc_cons: ∀p,q. rpprec (false::p) (true::q)
38 | rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
39 | rpprec_skip: rpprec (false::◊) ◊
42 interpretation "'precedes' on redex pointers"
43 'prec p q = (rpprec p q).
45 (* Note: this should go to core_notation *)
46 notation "hvbox(a break ≺ b)"
47 non associative with precedence 45
50 (* Note: this is p < q *)
51 definition rplt: relation rptr ≝ TC … rpprec.
53 interpretation "'less than' on redex pointers"
56 (* Note: this is p ≤ q *)
57 definition rple: relation rptr ≝ star … rpprec.
59 interpretation "'less or equal to' on redex pointers"
60 'leq p q = (rple p q).
62 lemma rpprec_rple: ∀p,q. p ≺ q → p ≤ q.
66 lemma rple_false: false::◊ ≤ ◊.
70 lemma rple_nil: ∀p. ◊ ≤ p.
74 lemma rple_comp: ∀p1,p2. p1 ≤ p2 → ∀b. (b::p1) ≤ (b::p2).
75 #p1 #p2 #H elim H -p2 // /3 width=3/