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 (* POINTER ******************************************************************)
19 (* Policy: pointer step metavariables: c *)
20 (* Note: this is a step of a path in the tree representation of a term:
21 rc (rectus) : not needed (we use sn instead)
22 sn (sinister): proceed on the left argument of an application
23 or on the argument of an abstraction (this would be rc)
24 dx (dexter) : proceed on the right argument of an application
26 (* Remark: the following breaks destruct because of δ-expansions
27 definition ptr_step: Type[0] ≝ bool.
28 definition sn: bool ≝ true.
29 definition dx: bool ≝ false.
31 inductive ptr_step: Type[0] ≝
36 definition is_dx: predicate ptr_step ≝ λc. dx = c.
38 (* Policy: pointer metavariables: p, q *)
39 (* Note: this is a path in the tree representation of a term, heading to a redex *)
40 definition ptr: Type[0] ≝ list ptr_step.
42 (* Note: a redex is "in the head" when is not under an abstraction nor in the lefr argument of an application *)
43 definition in_head: predicate ptr ≝ All … is_dx.
45 lemma in_head_ind: ∀R:predicate ptr. R (◊) →
46 (∀p. in_head p → R p → R (dx::p)) →
48 #R #H #IH #p elim p -p // -H *
49 #p #IHp * #H1 #H2 destruct /3 width=1/
52 definition compatible_rc: predicate (ptr→relation term) ≝ λR.
53 ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2).
55 definition compatible_sn: predicate (ptr→relation term) ≝ λR.
56 ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
58 definition compatible_dx: predicate (ptr→relation term) ≝ λR.
59 ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).