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_compatible: ∀o,s. is_standard s → is_standard (o:::s).
  32 #o #s elim s -s // #p * //
  33 #q #s #IHs * /3 width=1/
  34 qed.
  35
  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/
  39 qed.
  40
  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/
  44 qed.
  45
  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
  48 [ #p1 * //
  49 | #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
  50 ]
  51 qed-.
  52
  53 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
  54 #p #Hp * // /3 width=1/
  55 qed.
  56
  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/
  60 qed.
  61
  62 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
  63 #r elim r -r // #p *
  64 [ #_ * /2 width=1/
  65 | #q #r #IHr * /3 width=1/
  66 ]
  67 qed.
  68
  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/
  74 qed-.