# Library Stalmarck.algoDilemma1

Require Export algoDotriplets.
Require Export interImplement2.
Require Export stalmarck.
Section odilemma1.
Variable getT : rZ -> list triplet.
Variable LL : list triplet.
Hypothesis getTCorrect : forall a : rZ, incl (getT a) LL.

Definition dT (a b : rZ) (T1 T2 : Trace) :=
match T1, T2 with
| emptyTrace, emptyTrace => emptyTrace
| _, _ => dilemmaTrace a b T1 T2
end.

Theorem dTCorrect :
forall (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 (dT a b t1 t2) S4.
intros t1; case t1; simpl in |- *; auto.
intros t1'; case t1'; simpl in |- *; auto.
intros a b S1 S2 S3 S4 H' H'0 H'1.
apply emptyTraceEval; auto.
apply eqStateTrans with (2 := H'1).
inversion_clear H'.
inversion_clear H'0.
apply
eqStateTrans with (interState (addEq (a, b) S1) (addEq (a, rZComp b) S1)).
apply CompInterR; auto.
apply interStateEq; auto.
intros t a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros t t0 a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros r r0 t t0 a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros t t2 a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros t t0 t2 a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
intros r r0 t t0 t2 a b S1 S2 S3 S4 H' H'0 H'1.
apply dilemmaTraceEval with (S2 := S2) (S3 := S3); auto.
Qed.

Definition dilemma1 (f : list rZ -> rArray vM -> mbDT)
(Ar : rArray vM) (a b : rZ) : mbDT :=
match addEqMem Ar a b with
| triple Ar1 true L1 => quatuor _ _ _ _ Ar false nil emptyTrace
| triple Ar1 false L1 =>
match addEqMem Ar a (rZComp b) with
| triple Ar2 true L2 => quatuor _ _ _ _ Ar false nil emptyTrace
| triple Ar2 false L2 =>
match f L1 Ar1 with
| quatuor Ar1' true L1' T1' =>
match f L2 Ar2 with
| quatuor Ar2' true L2' T2' =>
quatuor _ _ _ _ Ar true nil (dT a b T1' T2')
| quatuor Ar2' false L2' T2' =>
quatuor _ _ _ _ Ar2' false (appendRz L2 L2')
(dT a b T1' T2')
end
| quatuor Ar1' false L1' T1' =>
match f L2 Ar2 with
| quatuor Ar2' true L2' T2' =>
quatuor _ _ _ _ Ar1' false (appendRz L1 L1')
(dT a b T1' T2')
| quatuor Ar2' false L2' T2' =>
match
interMem Ar1' Ar2' Ar (appendRz L1 L1') (appendRz L2 L2')
with
| (Ar', nil) => quatuor _ _ _ _ Ar' false nil emptyTrace
| (Ar', L') =>
quatuor _ _ _ _ Ar' false L' (dT a b T1' T2')
end
end
end
end
end.

Theorem dilemma1Correct :
forall (f : list rZ -> rArray vM -> mbDT) (Ar : rArray vM)
(a b : rZ) (S : State),
(forall (L : list rZ) (Ar : rArray vM) (S : State),
FStalCorrect Ar LL S (f L Ar)) -> FStalCorrect Ar LL S (dilemma1 f Ar a b).
intros f Ar a b S H'; unfold dilemma1 in |- *.
generalize (addEqMemCorrect Ar a b S).
intros Ar1 b1 L1; case b1.
intros H'0.
apply FStalCorrect0; auto.
intros H'0.
generalize (addEqMemCorrect Ar a (rZComp b) S).
case (addEqMem Ar a (rZComp b)).
intros Ar2 b2 L2; case b2.
intros H'1.
apply FStalCorrect0; auto.
intros H'1.
generalize (H' L1 Ar1).
case (f L1 Ar1); auto.
intros Ar1' b1' L1' T1'; case b1'.
intros H'2.
generalize (H' L2 Ar2).
case (f L2 Ar2); auto.
intros Ar2' b2' L2' T2'; case b2'.
generalize H'2; unfold FStalCorrect in |- *; simpl in |- *.
intros H'3 H'4 H'5 H'6.
elim H'1;
[ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14;
clear H'12 H'10 H'1
| clear H'1
| clear H'1 ]; auto.
elim H'0;
[ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17;
clear H'15 H'10 H'0
| clear H'0
| clear H'0 ]; auto.
elim (H'3 (addEq (pair a b) S));
[ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19;
clear H'15 E
| idtac
| idtac ]; auto.
elim (H'4 (addEq (pair a (rZComp b)) S));
[ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22;
clear H'20 E
| idtac
| idtac ]; auto.
cut (eqState (interState S' S'0) S'); [ intros Eq1 | idtac ].
exists S'; repeat (split; auto).
apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'0); auto.
apply dTCorrect with (S2 := S') (S3 := S'0); auto.
split; auto.
red in |- *.
intros i j H'0.
apply interMemEqStateRz; auto.
inversion H'21.
apply eqStateRzContr with (a := x); auto.
generalize H'2; unfold FStalCorrect in |- *; simpl in |- *.
intros H'3 H'4 H'5 H'6.
elim H'1;
[ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14;
clear H'12 H'10 H'1
| clear H'1
| clear H'1 ]; auto.
elim H'0;
[ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17;
clear H'15 H'10 H'0
| clear H'0
| clear H'0 ]; auto.
elim (H'3 (addEq (pair a b) S));
[ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19;
clear H'15 E
| idtac
| idtac ]; auto.
elim (H'4 (addEq (pair a (rZComp b)) S));
[ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22;
clear H'20 E
| idtac
| idtac ]; auto.
repeat (split; auto).
elim H'15; intros S'1 E; elim E; intros H'0 H'1; elim H'1; intros H'7 H'20;
clear H'1 E H'15.
cut (eqState (interState S' S'1) S'1); [ intros Eq1 | idtac ].
exists S'1; repeat (split; auto).
apply stalmarckPSplit with (a := a) (b := b) (S2 := S') (S3 := S'1); auto.
apply dTCorrect with (S2 := S') (S3 := S'1); auto.
split; auto.
red in |- *.
intros i j H'1.
apply interMemEqStateRz; auto.
inversion H'18.
apply eqStateRzContr with (a := x); auto.
unfold appendRz in |- *; red in |- *; apply appendfOlist; auto.
try exact rZltEqComp.
intros e H'0.
rewrite H'22.
apply H'14; auto.
cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')).
intros H'1; inversion H'1; red in |- *; auto.
apply appendfInclEq1; auto.
cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')).
intros H'1; inversion H'1; red in |- *; auto.
apply appendfInclEq2; auto.
generalize (H' L2 Ar2).
case (f L2 Ar2); auto.
intros Ar2' b2' L2' T2'; case b2'.
unfold FStalCorrect in |- *; simpl in |- *.
intros H'3 H'4 H'5 H'6.
elim H'1;
[ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14;
clear H'12 H'10 H'1
| clear H'1
| clear H'1 ]; auto.
elim H'0;
[ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17;
clear H'15 H'10 H'0
| clear H'0
| clear H'0 ]; auto.
elim (H'3 (addEq (pair a (rZComp b)) S));
[ intros S' E; elim E; intros H'10 H'15; elim H'15; intros H'18 H'19;
clear H'15 E
| idtac
| idtac ]; auto.
elim (H'4 (addEq (pair a b) S));
[ intros S'0 E; elim E; intros H'15 H'20; elim H'20; intros H'21 H'22;
clear H'20 E
| idtac
| idtac ]; auto.
repeat (split; auto).
elim H'15; intros S'1 E; elim E; intros H'0 H'1; elim H'1; intros H'7 H'20;
clear H'1 E H'15.
cut (eqState (interState S'1 S') S'1); [ intros Eq1 | idtac ].
exists S'1; repeat (split; auto).
apply stalmarckPSplit with (a := a) (b := b) (S2 := S'1) (S3 := S'); auto.
apply dTCorrect with (S2 := S'1) (S3 := S'); auto.
split; auto.
red in |- *.
intros i j H'1.
apply interMemEqStateRz; auto.
inversion H'18.
apply eqStateRzContr with (a := x); auto.
unfold appendRz in |- *; red in |- *; apply appendfOlist; auto.
try exact rZltEqComp.
intros e H'0.
rewrite H'22.
apply H'17; auto.
cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')); auto.
intros H'1; inversion H'1; red in |- *; auto.
apply appendfInclEq1; auto.
cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')); auto.
intros H'1; inversion H'1; red in |- *; auto.
apply appendfInclEq2; auto.
unfold FStalCorrect in |- *; simpl in |- *.
intros H'3 H'4 H'5 H'6.
elim H'1;
[ intros H'9 H'10; elim H'10; intros H'11 H'12; elim H'12; intros H'13 H'14;
clear H'12 H'10 H'1
| clear H'1
| clear H'1 ]; auto.
elim H'0;
[ intros H'8 H'10; elim H'10; intros H'12 H'15; elim H'15; intros H'16 H'17;
clear H'15 H'10 H'0
| clear H'0
| clear H'0 ]; auto.
elim (H'3 (addEq (pair a (rZComp b)) S));
[ intros H'7 H'10; elim H'10; intros H'15 H'18; elim H'18; intros H'19 H'20;
clear H'18 H'10
| idtac
| idtac ]; auto.
elim (H'4 (addEq (pair a b) S));
[ intros H'10 H'18; elim H'18; intros H'21 H'22; elim H'22; intros H'23 H'24;
clear H'22 H'18
| idtac
| idtac ]; auto.
cut (OlistRz (appendRz L1 L1'));
[ intros O1
| unfold appendRz in |- *; red in |- *; apply appendfOlist; auto;
exact rZltEqComp ].
cut (OlistRz (appendRz L2 L2'));
[ intros O2
| unfold appendRz in |- *; red in |- *; apply appendfOlist; auto;
exact rZltEqComp ].
elim H'15; intros S' E; elim E; intros H'0 H'1; elim H'1; intros H'2 H'18;
clear H'1 E H'15.
elim H'21; intros S'0 E; elim E; intros H'1 H'15; elim H'15; intros H'22 H'25;
clear H'15 E H'21.
generalize
(interMemProp Ar1' Ar2' Ar H'10 H'7 H'5 (appendRz L1 L1')
(appendRz L2 L2') O1 O2 _ _ _ H'22 H'2 H'6).
case (interMem Ar1' Ar2' Ar (appendRz L1 L1') (appendRz L2 L2')).
intros Ar' L' H'15; elim H'15;
[ intros H'29 H'30; elim H'30; intros H'31 H'32; elim H'32;
clear H'32 H'30 H'15
| clear H'15
| clear H'15
| clear H'15
| clear H'15 ]; auto.
case L'; auto.
intros H'15 H'21; repeat (split; auto).
exists S; split; [ idtac | split ]; auto.
apply rArrayStateGet with (Ar := Ar); auto.
intros e; apply H'15; auto.
red in |- *; intros H'26; inversion H'26.
intros r l H'15 H'21; repeat (split; auto).
exists (interState S'0 S'); split; [ idtac | split ]; auto.
apply stalmarckPSplit with (a := a) (b := b) (S2 := S'0) (S3 := S'); auto.
apply dTCorrect with (S2 := S'0) (S3 := S'); auto.
apply inclStateTrans with (addEq (pair a b) S); auto.
apply stalmarckIncl with (L := LL); auto.
apply inclStateTrans with (addEq (pair a (rZComp b)) S); auto.
apply stalmarckIncl with (L := LL); auto.
intros e H'15; rewrite H'24; auto.
apply H'17; auto.
cut (InclEq _ eqRz L1 (appendf _ rZlt eqRz rZltEDec L1 L1')); auto.
intros H'21; inversion H'21; red in |- *; auto.
apply appendfInclEq1; auto.
cut (InclEq _ eqRz L1' (appendf _ rZlt eqRz rZltEDec L1 L1')); auto.
intros H'21; inversion H'21; red in |- *; auto.
apply appendfInclEq2; auto.
intros e H'15; rewrite H'20; auto.
apply H'14; auto.
cut (InclEq _ eqRz L2 (appendf _ rZlt eqRz rZltEDec L2 L2')).
intros H'21; inversion H'21; red in |- *; auto.
apply appendfInclEq1; auto.
cut (InclEq _ eqRz L2' (appendf _ rZlt eqRz rZltEDec L2 L2')).
intros H'21; inversion H'21; red in |- *; auto.
apply appendfInclEq2; auto.
Qed.

Fixpoint dilemma1R (f : list rZ -> rArray vM -> mbDT)
(v : rNat) (n : nat) {struct n} : rArray vM -> mbDT :=
fun Ar =>
match rArrayGet _ Ar v with
| ref _ =>
match n with
| O => quatuor _ _ _ _ Ar false nil emptyTrace
| S m => dilemma1R f (rnext v) m Ar
end
| class _ =>
match dilemma1 f Ar (rZPlus v) rZTrue with
| quatuor Ar1 true L1 T1 => quatuor _ _ _ _ Ar1 true L1 T1
| quatuor Ar1 false L1 T1 =>
match n with
| O => quatuor _ _ _ _ Ar1 false L1 T1
| S m =>
match dilemma1R f (rnext v) m Ar1 with
| quatuor Ar2 b L2 T2 =>
quatuor _ _ _ _ Ar2 b (appendRz L1 L2) (appTrace T1 T2)
end
end
end
end.

Theorem dilemma1RCorrect :
forall (f : list rZ -> rArray vM -> _) (n1 : nat)
(v : rNat) (Ar : rArray vM) (S : State),
(forall (L : list rZ) (Ar : rArray vM) (S : State),
FStalCorrect Ar LL S (f L Ar)) ->
FStalCorrect Ar LL S (dilemma1R f v n1 Ar).
intros f n1; elim n1; simpl in |- *; auto.
intros v Ar S H'; case (rArrayGet vM Ar v); auto.
intros H'0.
apply FStalCorrect0; auto.
intros L; generalize (dilemma1Correct f Ar (rZPlus v) rZTrue S H').
case (dilemma1 f Ar (rZPlus v) rZTrue).
intros Ar1 b1 L1 T1; case b1; auto.
intros n0 H' v Ar S H'0.
case (rArrayGet vM Ar v); auto.
intros L; generalize (dilemma1Correct f Ar (rZPlus v) rZTrue S H'0).
case (dilemma1 f Ar (rZPlus v) rZTrue).
intros Ar1 b1 L1 T1; case b1; auto.
intros H'1.
generalize (fun S : State => H' (rnext v) Ar1 S H'0).
case (dilemma1R f (rnext v) n0 Ar1).
intros r b l t H'2.
apply FStalCorrectComp with (Ar' := Ar1); auto.
Qed.
Variable n : nat.

Fixpoint dilemma1RR (f : list rZ -> rArray vM -> mbDT)
(n1 : nat) {struct n1} : rArray vM -> mbDT :=
fun Ar =>
match dilemma1R f zero n Ar with
| quatuor Ar1 true L1 T1 => quatuor _ _ _ _ Ar1 true L1 T1
| quatuor Ar1 false nil T1 => quatuor _ _ _ _ Ar1 false nil T1
| quatuor Ar1 false L1 T1 =>
match n1 with
| O => quatuor _ _ _ _ Ar1 false L1 T1
| S m =>
match dilemma1RR f m Ar1 with
| quatuor Ar2 b L2 T2 =>
quatuor _ _ _ _ Ar2 b (appendRz L1 L2) (appTrace T1 T2)
end
end
end.

Theorem dilemma1RRCorrect :
forall (f : list rZ -> rArray vM -> _) (n1 : nat)
(Ar : rArray vM) (S : State),
(forall (L : list rZ) (Ar : rArray vM) (S : State),
FStalCorrect Ar LL S (f L Ar)) -> FStalCorrect Ar LL S (dilemma1RR f n1 Ar).
intros f n1; elim n1; simpl in |- *; auto.
intros Ar S H'.
generalize (dilemma1RCorrect f n zero Ar S H').
case (dilemma1R f zero n Ar).
intros Ar1 b1 L1 T1; case b1; auto.
case L1; auto.
intros n0 H' Ar S H'0.
generalize (dilemma1RCorrect f n zero Ar S H'0).
case (dilemma1R f zero n Ar).
intros Ar1 b1 L1 T1; case b1; auto.
case L1; auto.
intros r l H'1.
generalize (fun S : State => H' Ar1 S H'0).
case (dilemma1RR f n0 Ar1).
intros r0 b l0 t H'2.
apply FStalCorrectComp with (Ar' := Ar1); auto.
Qed.

Definition dilemma1RRL (f : list rZ -> rArray vM -> mbDT)
(Lt : list rZ) (n : nat) (Ar : rArray vM) : mbDT :=
match doTripletsN getT Lt n Ar with
| quatuor Ar1 true L1 T1 => quatuor _ _ _ _ Ar1 true L1 T1
| quatuor Ar1 false L1 T1 =>
match dilemma1RR f n Ar1 with
| quatuor Ar2 b L2 T2 =>
quatuor _ _ _ _ Ar2 b (appendRz L1 L2) (appTrace T1 T2)
end
end.

Theorem dilemma1RRLCorrect :
forall (f : list rZ -> rArray vM -> _) (Lt : list rZ)
(n1 : nat) (Ar : rArray vM) (S : State),
(forall (L : list rZ) (Ar : rArray vM) (S : State),
FStalCorrect Ar LL S (f L Ar)) ->
FStalCorrect Ar LL S (dilemma1RRL f Lt n1 Ar).
intros f Lt n1 Ar S H'; unfold dilemma1RRL in |- *.
generalize (doTripletFsNCorrect getT LL getTCorrect n1 Ar Lt S).
case (doTripletsN getT Lt n1 Ar); auto.
intros Ar1 b1 L1 T1; case b1; auto.
intros H'0.
generalize (fun S : State => dilemma1RRCorrect f n1 Ar1 S H').
case (dilemma1RR f n1 Ar1); auto.
intros r b l t H'1.
apply FStalCorrectComp with (Ar' := Ar1); auto.
Qed.

Fixpoint dilemmaN (L : list rZ) (m n : nat) {struct n} :
rArray vM -> mbDT :=
match n with
| O => doTripletsN getT L m
| S n1 => dilemma1RRL (fun L : list rZ => dilemmaN L m n1) L m
end.

Theorem dilemmaNCorrect :
forall (L : list rZ) (m n : nat) (Ar : rArray vM) (S : State),
FStalCorrect Ar LL S (dilemmaN L m n Ar).
intros L m n0; generalize L; elim n0; auto; clear L.
intros L Ar S;
change (FStalCorrect Ar LL S (doTripletsN getT L m Ar)) in |- *.
apply doTripletFsNCorrect; auto.
intros n1 H' L Ar S0; simpl in |- *; auto.
apply dilemma1RRLCorrect; auto.
Qed.