matita/matita/contribs/lambda/parallel_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 "parallel_reduction.ma".
  16
  17 (* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
  18
  19 definition preds: relation term ≝ star … pred.
  20
  21 interpretation "parallel computation"
  22    'ParRedStar M N = (preds M N).
  23
  24 notation "hvbox( M ⤇* break term 46 N )"
  25    non associative with precedence 45
  26    for @{ 'ParRedStar $M $N }.
  27
  28 lemma preds_refl: reflexive … preds.
  29 //
  30 qed.
  31
  32 lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
  33 /2 width=3/
  34 qed-.
  35
  36 lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
  37 /2 width=3/
  38 qed-.
  39
  40 lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
  41 /2 width=1/
  42 qed.
  43
  44 lemma preds_compatible_abst: compatible_abst preds.
  45 /3 width=1/
  46 qed.
  47
  48 lemma preds_compatible_sn: compatible_sn preds.
  49 /3 width=1/
  50 qed.
  51
  52 lemma preds_compatible_dx: compatible_dx preds.
  53 /3 width=1/
  54 qed.
  55
  56 lemma preds_compatible_appl: compatible_appl preds.
  57 /3 width=1/
  58 qed.
  59
  60 lemma preds_lift: liftable preds.
  61 /2 width=1/
  62 qed.
  63
  64 lemma preds_inv_lift: deliftable_sn preds.
  65 /3 width=3 by star_deliftable_sn, pred_inv_lift/
  66 qed-.
  67
  68 lemma preds_dsubst_dx: dsubstable_dx preds.
  69 /2 width=1/
  70 qed.
  71
  72 lemma preds_dsubst: dsubstable preds.
  73 /2 width=1/
  74 qed.
  75
  76 theorem preds_trans: transitive … preds.
  77 /2 width=3 by trans_star/
  78 qed-.
  79
  80 lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
  81                    ∃∃M. M1 ⤇ M & M2 ⤇* M.
  82 /3 width=3 by star_strip, pred_conf/
  83 qed-.
  84
  85 theorem preds_conf: confluent … preds.
  86 /3 width=3 by star_confluent, pred_conf/
  87 qed-.