# Library Stalmarck.trace

Require Export stalmarck.

Inductive Trace : Set :=
| emptyTrace : Trace
| tripletTrace : triplet Trace
| seqTrace : Trace Trace Trace
| dilemmaTrace : rZ rZ Trace Trace Trace.

Inductive evalTrace : State Trace State Prop :=
| emptyTraceEval :
S1 S2 : State, eqState S1 S2 evalTrace S1 emptyTrace S2
| tripletTraceEval :
(t : triplet) (S1 S2 S3 : State),
doTripletP S1 t S2 eqState S2 S3 evalTrace S1 (tripletTrace t) S3
| seqTraceEval :
(t1 t2 : Trace) (S1 S2 S3 : State),
evalTrace S1 t1 S2
evalTrace S2 t2 S3 evalTrace S1 (seqTrace t1 t2) S3
| dilemmaTraceEval :
(t1 t2 : Trace) (a b : rZ) (S1 S2 S3 S4 : State),
evalTrace (addEq (a, b) S1) t1 S2
evalTrace (addEq (a, rZComp b) S1) t2 S3
eqState (interState S2 S3) S4
evalTrace S1 (dilemmaTrace a b t1 t2) S4.
Hint Resolve emptyTraceEval tripletTraceEval.

Theorem evalTraceEq :
(S1 S2 : State) (t : Trace),
evalTrace S1 t S2
S3 S4 : State, evalTrace S3 t S4 eqState S1 S3 eqState S2 S4.
intros S1 S2 t H'; elim H'; clear H' t S2 S1; auto.
intros S1 S2 H' S3 S4 H'0; inversion H'0; auto.
intros H'1.
apply eqStateTrans with (S2 := S1); auto.
apply eqStateTrans with (S2 := S3); auto.
intros t S1 S2 S3 H' H'0 S4 S5 H'1 H'2; inversion H'1; auto.
apply eqStateTrans with (S2 := S2); auto.
apply eqStateTrans with (S2 := S6); auto.
apply doTripletEqComp with (t := t) (S1 := S1) (S2 := S4); auto.
intros t1 t2 S1 S2 S3 H' H'0 H'1 H'2 S0 S4 H'3; inversion H'3; auto.
intros H'4.
apply H'2 with (S4 := S6); auto.
apply H'0 with (S3 := S0); auto.
intros t1 t2 a b S1 S2 S3 S4 H' H'0 H'1 H'2 H'3 S0 S5 H'4; inversion H'4;
auto.
intros H'5.
apply eqStateTrans with (S2 := interState S7 S8); auto.
apply eqStateTrans with (S2 := interState S2 S3); auto.
apply interStateEq; auto.
apply H'0 with (S3 := addEq (a, b) S0); auto.
apply H'2 with (S4 := addEq (a, rZComp b) S0); auto.
Qed.

Theorem evalTraceComp :
(S1 S2 : State) (t : Trace),
evalTrace S1 t S2
S3 S4 : State, eqState S1 S3 eqState S2 S4 evalTrace S3 t S4.
intros S1 S2 t H'; elim H'; clear H' t S2 S1; auto.
intros S1 S2 H' S3 S4 H'0 H'1.
apply emptyTraceEval; auto.
apply eqStateTrans with (S2 := S1); auto.
apply eqStateTrans with (S2 := S2); auto.
intros t S1 S2 S3 H' H'0 S4 S5 H'1 H'2.
case (doTripletEqCompEx S1 S2 S4 t); auto.
intros S6 H'3; elim H'3; intros H'4 H'5; clear H'3.
apply tripletTraceEval with (S2 := S6); auto.
apply eqStateTrans with (S2 := S2); auto.
apply eqStateTrans with (S2 := S3); auto.
intros t1 t2 S1 S2 S3 H' H'0 H'1 H'2 S4 S5 H'3 H'4.
apply seqTraceEval with (S2 := S2); auto.
intros t1 t2 a b S1 S2 S3 S4 H' H'0 H'1 H'2 H'3 S5 S6 H'4 H'5.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
apply eqStateTrans with (S2 := S4); auto.
Qed.

Fixpoint TraceInList (T : Trace) : list triplet Prop :=
fun L : list triplet
match T with
| emptyTraceTrue
| tripletTrace tIn t L
| seqTrace T1 T2TraceInList T1 L TraceInList T2 L
| dilemmaTrace a b T1 T2TraceInList T1 L TraceInList T2 L
end.

Theorem doTripletsExTrace :
(L : list triplet) (S1 S2 : State),
doTripletsP S1 L S2
t : Trace, evalTrace S1 t S2 TraceInList t L.
intros L S1 S2 H'; elim H'; clear H' S1 S2 L.
intros S1 S2 H' H'0; emptyTrace; simpl in |- *; auto.
intros S1 S2 S3 L t H' H'0 H'1 H'2; elim H'2; intros t0 E; elim E;
intros H'3 H'4; clear E H'2.
(seqTrace (tripletTrace t) t0); simpl in |- *; repeat split; auto.
apply seqTraceEval with (S2 := S2); auto.
apply tripletTraceEval with (S2 := S2); auto.
Qed.

Theorem stalmarckExTrace :
(L : list triplet) (S1 S2 : State),
stalmarckP S1 L S2 t : Trace, evalTrace S1 t S2 TraceInList t L.
intros L S1 S2 H'; elim H'; clear H' S2 S1 L; auto.
intros S1 S2 L H'; apply doTripletsExTrace with (L := L); auto.
intros a b S1 S2 S3 S4 L H' H'0 H'1 H'2 H'3.
elim H'0; intros t E; elim E; intros H'4 H'5; clear E H'0.
elim H'2; intros t0 E; elim E; intros H'0 H'6; clear E H'2.
(dilemmaTrace a b t t0); simpl in |- *; repeat split; auto.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros S1 S2 S3 L H' H'0 H'1 H'2.
elim H'0; intros t E; elim E; intros H'4 H'5; clear E H'0.
elim H'2; intros t0 E; elim E; intros H'0 H'6; clear E H'2.
(seqTrace t t0); simpl in |- *; repeat split; auto.
apply seqTraceEval with (S2 := S2); auto.
Qed.