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_fwd_append_dx: ∀s,r. is_standard (s@r) → is_standard r.
32 /2 width=2 by Allr_fwd_append_dx/
35 lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s).
36 #o #s elim s -s // #p * //
37 #q #s #IHs * /3 width=1/
40 lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
41 #p #s elim s -s // #q1 * /2 width=1/
42 #q2 #s #IHs * /4 width=1/
45 lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
46 #r elim r -r /3 width=1/ #p * /2 width=1/
47 #q #r #IHr * /3 width=1/
50 lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s.
51 #s elim s -s // #a1 * // #a2 #s #IHs * #H
52 elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
53 #a #Ha1 #H destruct /3 width=1/
56 lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s.
57 #s elim s -s // #a1 * // #a2 #s #IHs * #H
58 elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
59 [ #a #Ha1 #H destruct /3 width=1/
64 lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
65 #s2 #p2 #s1 elim s1 -s1
67 | #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
71 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
72 #p #Hp * // /3 width=1/
75 theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
76 #s elim s -s // #p * //
77 #q #s #IHs * /3 width=1/
80 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
83 | #q #r #IHr * /3 width=1/
87 lemma is_standard_fwd_is_whd: ∀s,p,r. in_whd p → is_standard (r@(p::s)) → is_whd r.
88 #s #p #r elim r -r // #q #r #IHr #Hp #H
89 lapply (is_standard_fwd_cons … H)
90 lapply (is_standard_fwd_sle … H) #Hqp
91 lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/