]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/paths/standard_precedence.ma
a55770aa8374f816a745108ea9c0b5a58a70d1c4
[helm.git] / matita / matita / contribs / lambda / paths / standard_precedence.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "paths/path.ma".
16
17 (* STANDARD PRECEDENCE ******************************************************)
18
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::◊) ◊
27 .
28
29 interpretation "standard 'precedes' on paths"
30    'prec p q = (sprec p q).
31
32 lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
33                     ∃∃q0. p0 ≺ q0 & sn::q0 = q.
34 #p #q * -p -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/
39 | #p0 #H destruct
40 ]
41 qed-.
42
43 lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
44 #p #q #H elim H -p -q // /2 width=1/
45 [ #p #q * #H destruct
46 | #p #q * #H destruct
47 | #o #p #q #_ #IHpq * #H destruct /3 width=1/
48 ]
49 qed-.