# 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 tesizeS 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.

Theorem ordered:
t p e tr ev0 ev1,
well_formed t
lstar (conf t p e) tr (stop p (aeval t p e))
prec (ev_sys t p e) ev0 ev1
earlier tr ev0 ev1.