| Co-inductive program execution traces |
Set Implicit Arguments.
Section trace.
Variable A : Set.
CoInductive trace : Set :=
| Call : trace -> trace
| Crash : trace
| Output : A -> trace.
Inductive traceShape : Set :=
| CallShape : trace -> traceShape
| CrashShape : traceShape
| OutputShape : A -> traceShape.
Definition get_traceShape (tr : trace) :=
match tr with
| Call tr' => CallShape tr'
| Crash => CrashShape
| Output out => OutputShape out
end.
Theorem traceShape_eq : forall tr1 tr2,
get_traceShape tr1 = get_traceShape tr2
-> tr1 = tr2.
Inductive runTrace : trace -> A -> Prop :=
| RunOutput : forall output,
runTrace (Output output) output
| RunCall : forall tr output,
runTrace tr output
-> runTrace (Call tr) output.
Inductive runTrace' : traceShape -> A -> Prop :=
| RunOutput' : forall output,
runTrace' (OutputShape output) output
| RunCall' : forall tr output,
runTrace tr output
-> runTrace' (CallShape tr) output.
Hint Constructors runTrace runTrace'.
Theorem runTrace_shape : forall tr output,
runTrace' (get_traceShape tr) output
-> runTrace tr output.
Theorem runTrace_shape_inv : forall tr output,
runTrace tr output
-> runTrace' (get_traceShape tr) output.
Theorem trace_eq : forall tr1 tr2,
get_traceShape tr1 = get_traceShape tr2
-> tr1 = tr2.
Inductive runsTo : trace -> trace -> Prop :=
| RunTo_Self : forall tr,
runsTo tr tr
| RunTo_Call : forall tr1 tr2,
runsTo tr1 tr2
-> runsTo (Call tr1) tr2.
Hint Constructors runsTo.
Theorem runsTo_Self : forall tr1 tr2,
tr1 = tr2
-> runsTo tr1 tr2.
Theorem runsTo_Call : forall tr1 tr2 tr3,
tr1 = Call tr3
-> runsTo tr3 tr2
-> runsTo tr1 tr2.
Theorem runsTo_runTrace_trans : forall tr1 tr2 ans,
runsTo tr1 tr2
-> runTrace tr2 ans
-> runTrace tr1 ans.
Theorem runsTo_trans : forall tr1 tr2 tr3,
runsTo tr1 tr2
-> runsTo tr2 tr3
-> runsTo tr1 tr3.
Inductive runsTo' : traceShape -> trace -> Prop :=
| RunTo_Self' : forall trs tr,
trs = get_traceShape tr
-> runsTo' trs tr
| RunTo_Call' : forall tr1 tr2,
runsTo tr1 tr2
-> runsTo' (CallShape tr1) tr2.
Hint Constructors runsTo'.
Theorem runsTo_shape : forall tr1 tr2,
runsTo' (get_traceShape tr1) tr2
-> runsTo tr1 tr2.
End trace.
Implicit Arguments Crash [A].