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 (**************************************************************************)
15 include "lambda/terms/term.ma".
17 (* PATH *********************************************************************)
19 (* Policy: path step metavariables: o *)
20 (* Note: this is a step of a path in the tree representation of a term:
21 rc (rectus) : proceed on the argument of an abstraction
22 sn (sinister): proceed on the left argument of an application
23 dx (dexter) : proceed on the right argument of an application
25 inductive step: Type[0] ≝
31 definition is_dx: predicate step ≝ λo. dx = o.
33 (* Policy: path metavariables: p, q *)
34 (* Note: this is a path in the tree representation of a term, heading to a redex *)
35 definition path: Type[0] ≝ list step.
37 definition compatible_rc: predicate (path→relation term) ≝ λR.
38 ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
40 definition compatible_sn: predicate (path→relation term) ≝ λR.
41 ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
43 definition compatible_dx: predicate (path→relation term) ≝ λR.
44 ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
46 (* Note: a redex is "in the whd" when is not under an abstraction nor in the left argument of an application *)
47 definition in_whd: predicate path ≝ All … is_dx.
49 lemma in_whd_ind: ∀R:predicate path. R (◊) →
50 (∀p. in_whd p → R p → R (dx::p)) →
52 #R #H #IH #p elim p -p // -H *
53 #p #IHp * #H1 #H2 destruct /3 width=1/
56 (* Note: a redex is "inner" when is not in the whd *)
57 definition in_inner: predicate path ≝ λp. in_whd p → ⊥.
59 lemma in_inner_rc: ∀p. in_inner (rc::p).
60 #p * normalize #H destruct
63 lemma in_inner_sn: ∀p. in_inner (sn::p).
64 #p * normalize #H destruct
67 lemma in_inner_cons: ∀o,p. in_inner p → in_inner (o::p).
68 #o #p #H1p * /2 width=1/
71 lemma in_inner_inv_dx: ∀p. in_inner (dx::p) → in_inner p.
75 lemma in_whd_or_in_inner: ∀p. in_whd p ∨ in_inner p.
76 #p elim p -p /2 width=1/ #o #p * #Hp /3 width=1/ cases o -o /2 width=1/ /3 width=1/
79 lemma in_inner_ind: ∀R:predicate path.
80 (∀p. R (rc::p)) → (∀p. R (sn::p)) →
81 (∀p. in_inner p → R p → R (dx::p)) →
83 #R #H1 #H2 #IH #p elim p -p
86 lapply (in_inner_inv_dx … H) -H /3 width=1/
90 lemma in_inner_inv: ∀p. in_inner p →
91 ∨∨ ∃q. rc::q = p | ∃q. sn::q = p
92 | ∃∃q. in_inner q & dx::q = p.
93 @in_inner_ind /3 width=2/ /3 width=3/