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 (* Note: this comes from "star term lsred" *)
  21 inductive lsreds: rpseq → relation term ≝
  22 | lsreds_nil : ∀M. lsreds (◊) M M
  23 | lsreds_cons: ∀p,M1,M. M1 ⇀[p] M →
  24                ∀s,M2. lsreds s M M2 → lsreds (p::s) M1 M2
  25 .
  26
  27 interpretation "labelled sequential computation"
  28    'SeqRedStar M s N = (lsreds s M N).
  29
  30 notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
  31    non associative with precedence 45
  32    for @{ 'SeqRedStar $M $s $N }.
  33
  34 lemma lsred_lsreds: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
  35 /2 width=3/
  36 qed.
  37
  38 lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2.
  39 #s #M1 #M2 * -s -M1 -M2 //
  40 #p #M1 #M #_ #s #M2 #_ #H destruct
  41 qed-.
  42
  43 lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
  44                        ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2.
  45 #s #M1 #M2 * -s -M1 -M2
  46 [ #M #q #r #H destruct
  47 | #p #M1 #M #HM1 #s #M2 #HM2 #q #r #H destruct /2 width=3/
  48 ]
  49 qed-.
  50
  51 lemma lsreds_inv_lsred: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
  52 #p #M1 #M2 #H
  53 elim (lsreds_inv_cons … H ???) -H [4: // |2,3: skip ] #M #HM1 #H (**) (* simplify line *)
  54 <(lsreds_inv_nil … H ?) -H //
  55 qed-.
  56
  57 (* Note: "|s|" should be unparetesized *)
  58 lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
  59 #s #M1 #M2 #H elim H -s -M1 -M2 normalize //
  60 #p #M1 #M #HM1 #s #M2 #_ #IHM2
  61 lapply (lsred_fwd_mult … HM1) -p #HM1
  62 @(transitive_le … IHM2) -M2
  63 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
  64 qed-.
  65
  66 lemma lsreds_lift: ∀s. liftable (lsreds s).
  67 #s #h #M1 #M2 #H elim H -s -M1 -M2 // /3 width=3/
  68 qed.
  69
  70 lemma lsreds_inv_lift: ∀s. deliftable (lsreds s).
  71 #s #h #N1 #N2 #H elim H -s -N1 -N2 /2 width=3/
  72 #p #N1 #N #HN1 #s #N2 #_ #IHN2 #d #M1 #HMN1
  73 elim (lsred_inv_lift … HN1 … HMN1) -N1 #M #HM1 #HMN
  74 elim (IHN2 … HMN) -N /3 width=3/
  75 qed-.
  76
  77 lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
  78 #s #D #M1 #M2 #H elim H -s -M1 -M2 // /3 width=3/
  79 qed.
  80
  81 theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
  82 #s #M #N1 #H elim H -s -M -N1
  83 [ /2 width=3 by lsreds_inv_nil/
  84 | #p #M #M1 #HM1 #s #N1 #_ #IHMN1 #N2 #H
  85   elim (lsreds_inv_cons … H ???) -H [4: // |2,3: skip ] #M2 #HM2 #HMN2 (**) (* simplify line *)
  86   lapply (lsred_mono … HM1 … HM2) -M #H destruct /2 width=1/
  87 ]
  88 qed-.
  89
  90 theorem lsreds_trans: ∀s1,M1,M. M1 ⇀*[s1] M →
  91                       ∀s2,M2. M ⇀*[s2] M2 → M1 ⇀*[s1@s2] M2.
  92 #s1 #M1 #M #H elim H -s1 -M1 -M normalize // /3 width=3/
  93 qed-.