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 "paths/trace.ma".
16 include "paths/standard_order.ma".
18 (* STANDARD TRACE ***********************************************************)
20 (* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *)
21 definition is_standard: predicate trace ≝ Allr … sle.
23 lemma is_standard_fwd_append_sn: ∀s,r. is_standard (s@r) → is_standard s.
24 /2 width=2 by Allr_fwd_append_sn/
27 lemma is_standard_fwd_cons: ∀p,s. is_standard (p::s) → is_standard s.
28 /2 width=2 by Allr_fwd_cons/
31 lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s).
32 #o #s elim s -s // #p * //
33 #q #s #IHs * /3 width=1/
36 lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
37 #p #s elim s -s // #q1 * /2 width=1/
38 #q2 #s #IHs * /4 width=1/
41 lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
42 #r elim r -r /3 width=1/ #p * /2 width=1/
43 #q #r #IHr * /3 width=1/
46 lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
47 #s2 #p2 #s1 elim s1 -s1
49 | #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
53 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
54 #p #Hp * // /3 width=1/
57 theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
58 #s elim s -s // #p * //
59 #q #s #IHs * /3 width=1/
62 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
65 | #q #r #IHr * /3 width=1/
69 lemma is_standard_fwd_is_whd: ∀s,p,r. in_whd p → is_standard (r@(p::s)) → is_whd r.
70 #s #p #r elim r -r // #q #r #IHr #Hp #H
71 lapply (is_standard_fwd_cons … H)
72 lapply (is_standard_fwd_sle … H) #Hqp
73 lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/