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_inv_compatible_dx: ∀s. is_standard (dx:::s) →
  65                                      is_inner s → is_standard s.
  66 #s elim s -s // #a1 * // #a2 #s #IHs * #H
  67 elim (sle_inv_dx … H …) -H [4: // |3: skip ] (**) (* simplify line *)
  68 [ * #_ #H1a1 #_ * #H2a1 #_ -IHs
  69   elim (H2a1 …) -H2a1 -a2 -s //
  70 | * #a #Ha2 #H destruct #H * #_ /3 width=1/
  71 qed-.
  72
  73 lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
  74 #s2 #p2 #s1 elim s1 -s1
  75 [ #p1 * //
  76 | #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
  77 ]
  78 qed-.
  79
  80 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
  81 #p #Hp * // /3 width=1/
  82 qed.
  83
  84 theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
  85 #s elim s -s // #p * //
  86 #q #s #IHs * /3 width=1/
  87 qed.
  88
  89 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
  90 #r elim r -r // #p *
  91 [ #_ * /2 width=1/
  92 | #q #r #IHr * /3 width=1/
  93 ]
  94 qed.
  95
  96 lemma is_standard_fwd_is_whd: ∀s,p,r. in_whd p → is_standard (r@(p::s)) → is_whd r.
  97 #s #p #r elim r -r // #q #r #IHr #Hp #H
  98 lapply (is_standard_fwd_cons … H)
  99 lapply (is_standard_fwd_sle … H) #Hqp
 100 lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/
 101 qed-.
 102
 103 lemma is_standard_fwd_in_inner: ∀s,p. is_standard (p::s) → in_inner p → is_inner s.
 104 #s elim s -s // #q #s #IHs #p * #Hpq #Hs #Hp
 105 lapply (sle_fwd_in_inner … Hpq ?) // -p /3 width=3/
 106 qed.