matita/matita/lib/lambda/terms/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 "lambda/terms/parallel_computation.ma".
  16
  17 include "lambda/notation/relations/seqredstar_2.ma".
  18
  19 (* SEQUENTIAL COMPUTATION (MULTISTEP) ***************************************)
  20
  21 definition sreds: relation term ≝ star … sred.
  22
  23 interpretation "sequential computation"
  24    'SeqRedStar M N = (sreds M N).
  25
  26 lemma sreds_refl: reflexive … sreds.
  27 //
  28 qed.
  29
  30 lemma sreds_step_sn: ∀M1,M. M1 ↦ M → ∀M2. M ↦* M2 → M1 ↦* M2.
  31 /2 width=3/
  32 qed-.
  33
  34 lemma sreds_step_dx: ∀M1,M. M1 ↦* M → ∀M2. M ↦ M2 → M1 ↦* M2.
  35 /2 width=3/
  36 qed-.
  37
  38 lemma sreds_step_rc: ∀M1,M2. M1 ↦ M2 → M1 ↦* M2.
  39 /2 width=1/
  40 qed.
  41
  42 lemma lsred_compatible_abst: compatible_abst sreds.
  43 /3 width=1/
  44 qed.
  45
  46 lemma sreds_compatible_sn: compatible_sn sreds.
  47 /3 width=1/
  48 qed.
  49
  50 lemma sreds_compatible_dx: compatible_dx sreds.
  51 /3 width=1/
  52 qed.
  53
  54 lemma sreds_compatible_appl: compatible_appl sreds.
  55 /3 width=3/
  56 qed.
  57
  58 lemma sreds_lift: liftable sreds.
  59 /2 width=1/
  60 qed.
  61
  62 lemma sreds_inv_lift: deliftable_sn sreds.
  63 /3 width=3 by star_deliftable_sn, sred_inv_lift/
  64 qed-.
  65
  66 lemma sreds_dsubst: dsubstable_dx sreds.
  67 /2 width=1/
  68 qed.
  69
  70 theorem sreds_trans: transitive … sreds.
  71 /2 width=3 by trans_star/
  72 qed-.
  73
  74 (* Note: the substitution should be unparentesized *)
  75 lemma sreds_compatible_beta: ∀B1,B2. B1 ↦* B2 → ∀A1,A2. A1 ↦* A2 →
  76                              @B1.𝛌.A1 ↦* ([↙B2] A2).
  77 #B1 #B2 #HB12 #A1 #A2 #HA12
  78 @(sreds_trans … (@B2.𝛌.A1)) /2 width=1/ -B1
  79 @(sreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
  80 qed.
  81
  82 theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2.
  83 #M1 #M2 #H @(star_ind_l … M1 H) -M1 //
  84 #M1 #M #HM1 #_ #IHM2
  85 @(preds_step_sn … IHM2) -M2 /2 width=2/
  86 qed.
  87
  88 lemma pred_sreds: ∀M1,M2. M1 ⤇ M2 → M1 ↦* M2.
  89 #M1 #M2 #H elim H -M1 -M2 // /2 width=1/
  90 qed-.
  91
  92 theorem preds_sreds: ∀M1,M2. M1 ⤇* M2 → M1 ↦* M2.
  93 #M1 #M2 #H elim H -M2 //
  94 #M #M2 #_ #HM2 #HM1
  95 lapply (pred_sreds … HM2) -HM2 #HM2
  96 @(sreds_trans … HM1 … HM2)
  97 qed-.
  98
  99 theorem sreds_conf: ∀M0,M1. M0 ↦* M1 → ∀M2. M0 ↦* M2 →
 100                     ∃∃M. M1 ↦* M & M2 ↦* M.
 101 #M0 #M1 #HM01 #M2 #HM02
 102 lapply (sreds_preds … HM01) #HM01
 103 lapply (sreds_preds … HM02) #HM02
 104 elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
 105 lapply (preds_sreds … HM1) -HM1
 106 lapply (preds_sreds … HM2) -HM2 /2 width=3/
 107 qed-.