Library Copland.Main
This chapter contains the proof that traces generated from the
small-step semantics are compatible with the related event system.
Require Import List.
Import List.ListNotations.
Open Scope list_scope.
Require Import Omega.
Require Import Preamble More_lists Term LTS Event_system Term_system Trace.
The traces associated with a state.
Inductive traceS: St → list Ev → Prop :=
| tstop: ∀ p e,
traceS (stop p e) []
| tconf: ∀ t tr p e,
trace t p e tr →
traceS (conf t p e) tr
| trem: ∀ st tr j p,
traceS st tr →
traceS (rem j p st)
(tr ++
[(rpy (pred j) p (pl st) (seval st))])
| tls: ∀ st tr1 t tr2,
traceS st tr1 →
trace t (pl st) (seval st) tr2 →
traceS (ls st t) (tr1 ++ tr2)
| tbsl: ∀ st tr1 t p e tr2 j,
traceS st tr1 →
trace t p e tr2 →
traceS (bsl j st t p e)
(tr1 ++ tr2 ++
[(join (pred j) p (seval st)
(aeval t p e)
(ss (seval st) (aeval t p e)))])
| tbsr: ∀ st tr j e,
traceS st tr →
traceS (bsr j e st)
(tr ++ [(join (pred j) (pl st) e
(seval st)
(ss e (seval st)))])
| tbp: ∀ st1 tr1 st2 tr2 tr3 j,
traceS st1 tr1 → traceS st2 tr2 →
shuffle tr1 tr2 tr3 →
traceS (bp j st1 st2)
(tr3 ++ [(join (pred j) (pl st2)
(seval st1)
(seval st2)
(pp (seval st1) (seval st2)))]).
Hint Constructors traceS.
Fixpoint esizeS s:=
match s with
| stop _ _ ⇒ 0
| conf t _ _ ⇒ esize t
| rem _ _ st ⇒ 1 + esizeS st
| ls st t ⇒ esizeS st + esize t
| bsl _ st t _ _ ⇒ 1 + esizeS st + esize t
| bsr _ _ st ⇒ 1 + esizeS st
| bp _ st1 st2 ⇒ 1 + esizeS st1 + esizeS st2
end.
Lemma esize_tr:
∀ t p e tr,
trace t p e tr → length tr = esize t.
Lemma esizeS_tr:
∀ st tr,
traceS st tr → length tr = esizeS st.
Lemma step_silent_tr:
∀ st st' tr,
step st None st' →
traceS st' tr →
traceS st tr.
Lemma step_evt_tr:
∀ st st' ev tr,
step st (Some ev) st' →
traceS st' tr →
traceS st (ev::tr).
Lemma nlstar_trace_helper:
∀ e p n st0 tr st1,
step st0 e st1 →
nlstar n st1 tr (stop p (seval st0)) →
nlstar n st1 tr (stop p (seval st1)).
Lemma nlstar_trace:
∀ n p st tr,
nlstar n st tr (stop p (seval st)) →
traceS st tr.
A trace of the LTS is a trace of the big-step semantics.
Lemma lstar_trace:
∀ t p e tr,
well_formed t →
lstar (conf t p e) tr (stop p (aeval t p e)) →
trace t p e tr.
The key theorem.