matita/matita/contribs/lambda/pointer_list_standard.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 "pointer_list.ma".
  16 include "pointer_order.ma".
  17
  18 (* STANDARD POINTER LIST ****************************************************)
  19
  20 (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
  21 definition is_standard: predicate ptrl ≝ Allr … ple.
  22
  23 lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s).
  24 #c #s elim s -s // #p * //
  25 #q #s #IHs * /3 width=1/
  26 qed.
  27
  28 lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
  29 #p #s elim s -s // #q1 * /2 width=1/
  30 #q2 #s #IHs * /4 width=1/
  31 qed.
  32
  33 lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
  34 #r elim r -r /3 width=1/ #p * /2 width=1/
  35 #q #r #IHr * /3 width=1/
  36 qed.
  37
  38 theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
  39 #s elim s -s // #p * //
  40 #q #s #IHs * /3 width=1/
  41 qed.
  42
  43 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
  44 #p #Hp * // /3 width=1/
  45 qed.
  46
  47 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
  48 #r elim r -r // #p *
  49 [ #_ * /2 width=1/
  50 | #q #r #IHr * /3 width=1/
  51 ]
  52 qed.