matita/matita/lib/lambda/paths/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 "lambda/terms/labeled_sequential_computation.ma".
  16 include "lambda/paths/trace.ma".
  17 include "lambda/paths/labeled_sequential_reduction.ma".
  18
  19 include "lambda/notation/relations/seqredstar_3.ma".
  20
  21 (* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
  22
  23 (* Note: lstar shuld be replaced by l_sreds *)
  24 definition pl_sreds: trace → relation term ≝ lstar … pl_sred.
  25
  26 interpretation "path-labeled sequential computation"
  27    'SeqRedStar M s N = (pl_sreds s M N).
  28
  29 lemma sreds_pl_sreds: ∀M,N. M ↦* N → ∃s. M ↦*[s] N.
  30 /3 width=1 by sreds_l_sreds, sred_pl_sred/
  31 qed-.
  32
  33 lemma pl_sreds_inv_sreds: ∀s,M,N. M ↦*[s] N → M ↦* N.
  34 /3 width=5 by l_sreds_inv_sreds, pl_sred_inv_sred/
  35 qed-.
  36
  37 lemma pl_sreds_refl: reflexive … (pl_sreds (◊)).
  38 //
  39 qed.
  40
  41 lemma pl_sreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
  42 /2 width=3/
  43 qed-.
  44
  45 lemma pl_sreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
  46 /2 width=3/
  47 qed-.
  48
  49 lemma pl_sreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
  50 /2 width=1/
  51 qed.
  52
  53 lemma pl_sreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
  54 /2 width=5 by lstar_inv_nil/
  55 qed-.
  56
  57 lemma pl_sreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
  58                          ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
  59 /2 width=3 by lstar_inv_cons/
  60 qed-.
  61
  62 lemma pl_sreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
  63 /2 width=1 by lstar_inv_step/
  64 qed-.
  65
  66 lemma pl_sreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
  67                         ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
  68 /2 width=1 by lstar_inv_pos/
  69 qed-.
  70
  71 lemma lsred_compatible_rc: ho_compatible_rc pl_sreds.
  72 /3 width=1/
  73 qed.
  74
  75 lemma pl_sreds_compatible_sn: ho_compatible_sn pl_sreds.
  76 /3 width=1/
  77 qed.
  78
  79 lemma pl_sreds_compatible_dx: ho_compatible_dx pl_sreds.
  80 /3 width=1/
  81 qed.
  82
  83 lemma pl_sreds_lift: ∀s. liftable (pl_sreds s).
  84 /2 width=1/
  85 qed.
  86
  87 lemma pl_sreds_inv_lift: ∀s. deliftable_sn (pl_sreds s).
  88 /3 width=3 by lstar_deliftable_sn, pl_sred_inv_lift/
  89 qed-.
  90
  91 lemma pl_sreds_dsubst: ∀s. dsubstable_dx (pl_sreds s).
  92 /2 width=1/
  93 qed.
  94
  95 theorem pl_sreds_mono: ∀s. singlevalued … (pl_sreds s).
  96 /3 width=7 by lstar_singlevalued, pl_sred_mono/
  97 qed-.
  98
  99 theorem pl_sreds_trans: ltransitive … pl_sreds.
 100 /2 width=3 by lstar_ltransitive/
 101 qed-.
 102
 103 lemma pl_sreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
 104                                 @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
 105 #r #B1 #B2 #HB12 #s #A1 #A2 #HA12
 106 @(pl_sreds_trans … (@B2.A1)) /2 width=1/
 107 qed.
 108
 109 lemma pl_sreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
 110                                 @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2.
 111 #r #B1 #B2 #HB12 #s #A1 #A2 #HA12
 112 @(pl_sreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
 113 @(pl_sreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
 114 qed.