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 (* STANDARD PRECEDENCE ******************************************************)
19 (* Note: standard precedence relation on paths: p ≺ q
20 to serve as base for the order relations: p < q and p ≤ q *)
21 inductive sprec: relation path ≝
22 | sprec_nil : ∀o,q. sprec (◊) (o::q)
23 | sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
24 | sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
25 | sprec_comp: ∀o,p,q. sprec p q → sprec (o::p) (o::q)
26 | sprec_skip: sprec (dx::◊) ◊
29 interpretation "standard 'precedes' on paths"
30 'prec p q = (sprec p q).
32 lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
33 ∃∃q0. p0 ≺ q0 & sn::q0 = q.
35 [ #o #q #p0 #H destruct
36 | #p #q #p0 #H destruct
37 | #p #q #p0 #H destruct
38 | #o #p #q #Hpq #p0 #H destruct /2 width=3/
43 lemma sprec_inv_dx: ∀p,q. p ≺ q → ∀q0. dx::q0 = q →
44 ◊ = p ∨ ∃∃p0. p0 ≺ q0 & dx::p0 = p.
46 [ #o #q #q0 #H destruct /2 width=1/
47 | #p #q #q0 #H destruct
48 | #p #q #q0 #H destruct
49 | #o #p #q #Hpq #q0 #H destruct /3 width=3/
54 lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p →
55 (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨
58 [ #o #q #p0 #H destruct
59 | #p #q #p0 #H destruct
60 | #p #q #p0 #H destruct /3 width=2/
61 | #o #p #q #Hpq #p0 #H destruct /3 width=3/
66 lemma sprec_inv_comp: ∀p1,p2. p1 ≺ p2 →
67 ∀o,q1,q2. o::q1 = p1 → o::q2 = p2 → q1 ≺ q2.
69 [ #o #q #o0 #q1 #q2 #H destruct
70 | #p #q #o0 #q1 #q2 #H1 #H2 destruct
71 | #p #q #o0 #q1 #q2 #H1 #H2 destruct
72 | #o #p #q #Hpq #o0 #q1 #q2 #H1 #H2 destruct //
73 | #o0 #q1 #q2 #_ #H destruct
77 lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
78 #p #q #H elim H -p -q // /2 width=1/
81 | #o #p #q #_ #IHpq * #H destruct /3 width=1/
85 lemma sprec_fwd_in_inner: ∀p,q. p ≺ q → in_inner p → in_inner q.
86 /3 width=3 by sprec_fwd_in_whd/