matita/matita/contribs/lambda/terms/labeled_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 "terms/pointer_list.ma".
  16 include "terms/parallel_computation.ma".
  17
  18 (* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
  19
  20 definition lsreds: ptrl → 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 lsreds_refl: reflexive … (lsreds (◊)).
  30 //
  31 qed.
  32
  33 lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
  34 /2 width=3/
  35 qed-.
  36
  37 lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
  38 /2 width=3/
  39 qed-.
  40
  41 lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
  42 /2 width=1/
  43 qed.
  44
  45 lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
  46 /2 width=5 by lstar_inv_nil/
  47 qed-.
  48
  49 lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
  50                        ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
  51 /2 width=3 by lstar_inv_cons/
  52 qed-.
  53
  54 lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
  55 /2 width=1 by lstar_inv_step/
  56 qed-.
  57
  58 lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
  59                       ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
  60 /2 width=1 by lstar_inv_pos/
  61 qed-.
  62
  63 lemma lsred_compatible_rc: ho_compatible_rc lsreds.
  64 /3 width=1/
  65 qed.
  66
  67 lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
  68 /3 width=1/
  69 qed.
  70
  71 lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
  72 /3 width=1/
  73 qed.
  74
  75 lemma lsreds_lift: ∀s. liftable (lsreds s).
  76 /2 width=1/
  77 qed.
  78
  79 lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
  80 /3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
  81 qed-.
  82
  83 lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
  84 /2 width=1/
  85 qed.
  86
  87 theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
  88 /3 width=7 by lstar_singlevalued, lsred_mono/
  89 qed-.
  90
  91 theorem lsreds_trans: ltransitive … lsreds.
  92 /2 width=3 by lstar_ltransitive/
  93 qed-.
  94
  95 lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
  96                               @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
  97 #r #B1 #B2 #HB12 #s #A1 #A2 #HA12
  98 @(lsreds_trans … (@B2.A1)) /2 width=1/
  99 qed.
 100
 101 lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
 102                               @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2.
 103 #r #B1 #B2 #HB12 #s #A1 #A2 #HA12
 104 @(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
 105 @(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
 106 qed.
 107
 108 (* Note: "|s|" should be unparetesized *)
 109 lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → ♯{M2} ≤ ♯{M1} ^ (2 ^ (|s|)).
 110 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
 111 #p #s #M1 #M #HM1 #_ #IHM2
 112 lapply (lsred_fwd_mult … HM1) -p #HM1
 113 @(transitive_le … IHM2) -M2
 114 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
 115 qed-.
 116
 117 theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
 118 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
 119 #a #s #M1 #M #HM1 #_ #IHM2
 120 @(preds_step_sn … IHM2) -M2 /2 width=2/
 121 qed.
 122
 123 lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
 124 #M1 #M2 #H elim H -M1 -M2 /2 width=2/
 125 [ #A1 #A2 #_ * /3 width=2/
 126 | #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
 127 | #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
 128 qed-.
 129
 130 theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
 131 #M1 #M2 #H elim H -M2 /2 width=2/
 132 #M #M2 #_ #HM2 * #r #HM1
 133 elim (pred_lsreds … HM2) -HM2 #s #HM2
 134 lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
 135 qed-.
 136
 137 theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
 138                      ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
 139 #s1 #M0 #M1 #HM01 #s2 #M2 #HM02
 140 lapply (lsreds_preds … HM01) -s1 #HM01
 141 lapply (lsreds_preds … HM02) -s2 #HM02
 142 elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
 143 elim (preds_lsreds … HM1) -HM1
 144 elim (preds_lsreds … HM2) -HM2 /2 width=5/
 145 qed-.