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/paths/path.ma".
17 include "lambda/notation/relations/prec_2.ma".
19 (* STANDARD PRECEDENCE ******************************************************)
21 (* Note: standard precedence relation on paths: p ≺ q
22 to serve as base for the order relations: p < q and p ≤ q *)
23 inductive sprec: relation path ≝
24 | sprec_nil : ∀o,q. sprec (◊) (o::q)
25 | sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
26 | sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
27 | sprec_comp: ∀o,p,q. sprec p q → sprec (o::p) (o::q)
28 | sprec_skip: sprec (dx::◊) ◊
31 interpretation "standard 'precedes' on paths"
32 'prec p q = (sprec p q).
34 lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
35 ∃∃q0. p0 ≺ q0 & sn::q0 = q.
37 [ #o #q #p0 #H destruct
38 | #p #q #p0 #H destruct
39 | #p #q #p0 #H destruct
40 | #o #p #q #Hpq #p0 #H destruct /2 width=3/
45 lemma sprec_inv_dx: ∀p,q. p ≺ q → ∀q0. dx::q0 = q →
46 ◊ = p ∨ ∃∃p0. p0 ≺ q0 & dx::p0 = p.
48 [ #o #q #q0 #H destruct /2 width=1/
49 | #p #q #q0 #H destruct
50 | #p #q #q0 #H destruct
51 | #o #p #q #Hpq #q0 #H destruct /3 width=3/
56 lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
57 (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
60 [ #o #q #p0 #H destruct
61 | #p #q #p0 #H destruct
62 | #p #q #p0 #H destruct /3 width=2/
63 | #o #p #q #Hpq #p0 #H destruct /3 width=3/
68 lemma sprec_inv_comp: ∀p1,p2. p1 ≺ p2 →
69 ∀o,q1,q2. o::q1 = p1 → o::q2 = p2 → q1 ≺ q2.
71 [ #o #q #o0 #q1 #q2 #H destruct
72 | #p #q #o0 #q1 #q2 #H1 #H2 destruct
73 | #p #q #o0 #q1 #q2 #H1 #H2 destruct
74 | #o #p #q #Hpq #o0 #q1 #q2 #H1 #H2 destruct //
75 | #o0 #q1 #q2 #_ #H destruct
79 lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
80 #p #q #H elim H -p -q // /2 width=1/
83 | #o #p #q #_ #IHpq * #H destruct /3 width=1/
87 lemma sprec_fwd_in_inner: ∀p,q. p ≺ q → in_inner p → in_inner q.
88 /3 width=3 by sprec_fwd_in_whd/