matita/matita/contribs/lambda/labelled_sequential_computation.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 "redex_pointer_sequence.ma".
  16 include "labelled_sequential_reduction.ma".
  17
  18 (* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
  19
  20 definition lsreds: rpseq → relation term ≝ lstar … lsred.
  21
  22 interpretation "labelled sequential computation"
  23    'SeqRedStar M s N = (lsreds s M N).
  24
  25 notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
  26    non associative with precedence 45
  27    for @{ 'SeqRedStar $M $s $N }.
  28
  29 lemma lsred_lsreds: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
  30 /2 width=1/
  31 qed.
  32
  33 lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2.
  34 /2 width=5 by lstar_inv_nil/
  35 qed-.
  36
  37 lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
  38                        ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2.
  39 /2 width=3 by lstar_inv_cons/
  40 qed-.
  41
  42 lemma lsreds_inv_lsred: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
  43 /2 width=1 by lstar_inv_step/
  44 qed-.
  45
  46 lemma lsreds_lift: ∀s. liftable (lsreds s).
  47 /2 width=1/
  48 qed.
  49
  50 lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
  51 /3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
  52 qed-.
  53
  54 lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
  55 /2 width=1/
  56 qed.
  57
  58 theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
  59 /3 width=7 by lstar_singlevalued, lsred_mono/
  60 qed-.
  61
  62 theorem lsreds_trans: ∀s1,M1,M. M1 ⇀*[s1] M →
  63                       ∀s2,M2. M ⇀*[s2] M2 → M1 ⇀*[s1@s2] M2.
  64 /2 width=3 by lstar_trans/
  65 qed-.
  66
  67 (* Note: "|s|" should be unparetesized *)
  68 lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
  69 #s #M1 #M2 #H elim H -s -M1 -M2 normalize //
  70 #p #M1 #M #HM1 #s #M2 #_ #IHM2
  71 lapply (lsred_fwd_mult … HM1) -p #HM1
  72 @(transitive_le … IHM2) -M2
  73 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
  74 qed-.