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

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.