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