matita/matita/contribs/lambda/paths/standard_trace.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/trace.ma".
  16 include "paths/standard_order.ma".
  17
  18 (* STANDARD TRACE ***********************************************************)
  19
  20 (* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *)
  21 definition is_standard: predicate trace ≝ Allr … sle.
  22
  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/
  25 qed-.
  26
  27 lemma is_standard_fwd_cons: ∀p,s. is_standard (p::s) → is_standard s.
  28 /2 width=2 by Allr_fwd_cons/
  29 qed-.
  30
  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/
  33 qed-.
  34
  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/
  38 qed.
  39
  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/
  43 qed.
  44
  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/
  48 qed.
  49
  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/
  54 qed-.
  55
  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/
  60 | #a #H destruct
  61 ]
  62 qed-.
  63
  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
  66 [ #p1 * //
  67 | #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
  68 ]
  69 qed-.
  70
  71 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
  72 #p #Hp * // /3 width=1/
  73 qed.
  74
  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/
  78 qed.
  79
  80 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
  81 #r elim r -r // #p *
  82 [ #_ * /2 width=1/
  83 | #q #r #IHr * /3 width=1/
  84 ]
  85 qed.
  86
  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/
  92 qed-.