1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "terms/labeled_sequential_computation.ma".
16 include "paths/trace.ma".
17 include "paths/labeled_sequential_reduction.ma".
19 (* PATH-LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
21 (* Note: lstar shuld be replaced by l_sreds *)
22 definition pl_sreds: trace → relation term ≝ lstar … pl_sred.
24 interpretation "path-labeled sequential computation"
25 'SeqRedStar M s N = (pl_sreds s M N).
27 lemma sreds_pl_sreds: ∀M,N. M ↦* N → ∃s. M ↦*[s] N.
28 /3 width=1 by sreds_l_sreds, sred_pl_sred/
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/
35 lemma pl_sreds_refl: reflexive … (pl_sreds (◊)).
39 lemma pl_sreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
43 lemma pl_sreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
47 lemma pl_sreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
51 lemma pl_sreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
52 /2 width=5 by lstar_inv_nil/
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/
60 lemma pl_sreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
61 /2 width=1 by lstar_inv_step/
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/
69 lemma lsred_compatible_rc: ho_compatible_rc pl_sreds.
73 lemma pl_sreds_compatible_sn: ho_compatible_sn pl_sreds.
77 lemma pl_sreds_compatible_dx: ho_compatible_dx pl_sreds.
81 lemma pl_sreds_lift: ∀s. liftable (pl_sreds s).
85 lemma pl_sreds_inv_lift: ∀s. deliftable_sn (pl_sreds s).
86 /3 width=3 by lstar_deliftable_sn, pl_sred_inv_lift/
89 lemma pl_sreds_dsubst: ∀s. dsubstable_dx (pl_sreds s).
93 theorem pl_sreds_mono: ∀s. singlevalued … (pl_sreds s).
94 /3 width=7 by lstar_singlevalued, pl_sred_mono/
97 theorem pl_sreds_trans: ltransitive … pl_sreds.
98 /2 width=3 by lstar_ltransitive/
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/
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/