# Library Stalmarck.doTriplets

Require Export doTriplet.
Require Import PolyListAux.

Inductive doTripletsP : State list triplet State Prop :=
| doTripletsRef :
(S1 S2 : State) (L : list triplet),
eqState S1 S2 doTripletsP S1 L S2
| doTripletsTrans :
(S1 S2 S3 : State) (L : list triplet) (t : triplet),
In t L
doTripletP S1 t S2 doTripletsP S2 L S3 doTripletsP S1 L S3.
Hint Resolve doTripletsRef.

Theorem doTripletsComp :
(S1 S2 S3 S4 : State) (L : list triplet),
doTripletsP S1 L S2 eqState S3 S1 eqState S4 S2 doTripletsP S3 L S4.
intros S1 S2 S3 S4 L H'; generalize S3 S4; elim H'; clear H' L S1 S2 S3 S4;
auto.
intros S1 S2 L H' S3 S4 H'0 H'1.
apply doTripletsRef; auto.
apply eqStateTrans with (S2 := S1); auto.
apply eqStateTrans with (S2 := S2); auto.
intros S1 S2 S3 L t H' H'0 H'1 H'2 S0 S4 H'3 H'4.
elim (doTripletEqCompEx S1 S2 S0 t);
[ intros S6 E; Elimc E; intros H'11 H'12 | idtac | idtac ];
auto.
apply doTripletsTrans with (S2 := S6) (t := t); auto.
Qed.

Theorem doTripletsRTrans :
(S1 S2 S3 : State) (L : list triplet),
doTripletsP S1 L S2 doTripletsP S2 L S3 doTripletsP S1 L S3.
intros S1 S2 S3 L H'; elim H'; auto.
intros S4 S5 L0 H'0 H'1.
apply doTripletsComp with (S1 := S5) (S2 := S3); auto.
intros S4 S5 S0 L0 t H'0 H'1 H'2 H'3 H'4.
apply doTripletsTrans with (S2 := S5) (t := t); auto.
Qed.

Theorem doTripletsUnionEx :
(S1 S2 : State) (L : list triplet),
doTripletsP S1 L S2 S3 : State, eqState S2 (unionState S3 S1).
intros S1 S2 L H'; elim H'; auto.
intros S3 S4 H'0 H'1; S3; auto.
apply eqStateTrans with (S2 := S3); auto.
red in |- *; split; auto.
intros S3 S4 S5 L0 t H'0 H'1 H'2 H'3.
elim (doTripletUnionEx S3 S4 t); [ intros S6 E | idtac ]; auto.
elim H'3; intros S7 E0.
(unionState S7 S6).
apply eqStateTrans with (S2 := unionState S7 S4); auto.
rewrite E; auto.
apply unionStateAssoc; auto.
Qed.

Theorem doTripletsIncl :
(S1 S2 : State) (L : list triplet),
doTripletsP S1 L S2 inclState S1 S2.
intros S1 S2 L H'.
elim (doTripletsUnionEx S1 S2 L); [ intros S3 E | idtac ]; auto.
apply inclStateEqStateComp with (S1 := S1) (S3 := unionState S3 S1); auto.
Qed.

Theorem doTripletCongruent :
(S1 S2 S3 : State) (L : list triplet),
doTripletsP S1 L S2 doTripletsP (unionState S3 S1) L (unionState S3 S2).
intros S1 S2 S3 L H'; Elimc H'; clear S1 S2 L; auto.
intros S1 S2 S0 L t H' H'0 H'1 H'2.
apply doTripletsRTrans with (S2 := unionState S3 S2); auto.
elim (doTripletCongruentEx S1 S2 S3 t);
[ intros S4 E; Elimc E; intros H'8 H'9 | idtac ];
auto.
apply doTripletsRTrans with (S2 := S4); auto.
apply doTripletsTrans with (S2 := S4) (t := t); auto.
Qed.

Theorem doTripletsMonotoneEx :
(S1 S2 S3 : State) (L : list triplet),
doTripletsP S1 L S3
inclState S1 S2 S4 : State, doTripletsP S2 L S4 inclState S3 S4.
intros S1 S2 S3 L H' H'0.
lapply (doTripletCongruent S1 S3 S2 L); [ intros H'5 | idtac ]; auto.
(unionState S2 S3); split; auto.
apply doTripletsComp with (S1 := unionState S2 S1) (S2 := unionState S2 S3);
auto.
red in |- *; split; auto.
Qed.

Theorem doTripletsConftEx :
(L : list triplet) (S1 S2 S3 : State),
doTripletsP S1 L S2
doTripletsP S1 L S3
S4 : State, doTripletsP S2 L S4 doTripletsP S3 L S4.
intros L S1 S2 S3 H' H'0.
elim (doTripletsUnionEx S1 S2 L); [ intros S4 E | idtac ]; auto.
elim (doTripletsUnionEx S1 S3 L); [ intros S5 E0 | idtac ]; auto.
(unionState S5 S2); split; auto.
apply doTripletsComp with (S1 := unionState S4 S1) (S2 := unionState S4 S3);
auto.
apply doTripletCongruent; auto.
apply eqStateTrans with (S2 := unionState S5 (unionState S4 S1)); auto.
apply eqStateTrans with (S2 := unionState (unionState S5 S4) S1); auto.
apply unionStateAssoc; auto.
apply eqStateTrans with (S2 := unionState (unionState S4 S5) S1); auto.
apply eqStateTrans with (S2 := unionState S4 (unionState S5 S1)); auto.
apply eqStateTrans with (S2 := unionState (unionState S4 S5) S1); auto.
apply eqStateSym; auto.
apply unionStateAssoc; auto.
apply doTripletsComp with (S1 := unionState S5 S1) (S2 := unionState S5 S2);
auto.
apply doTripletCongruent; auto.
Qed.

Theorem doTripletsRealizeStateEval :
(f : rNat bool) (S1 S2 : State) (L : list triplet),
realizeState f S1
doTripletsP S1 L S2
realizeTriplets f L f zero = true realizeState f S2.
intros f S1 S2 L H' H'0; generalize H'; elim H'0; auto.
intros S3 S4 L0 H'1 H'2 H'3 H'4.
apply realizeStateIncl with (S1 := S3); auto; inversion H'1; auto.
intros S3 S4 S5 L0 t H'1 H'2 H'3 H'4 H'5 H'6 H'7.
apply H'4; auto.
apply realizeStateEval with (2 := H'2); auto.
Qed.

Theorem doTripletsTermExAux :
(L : list triplet) (S1 S2 : State),
doTripletsP S1 L S2
t : triplet,
In t L
doTripletsP S1 (rem _ tripletDec t L) S2
( S3 : State,
( S4 : State,
doTripletsP S1 (rem _ tripletDec t L) S3
doTripletP S3 t S4 doTripletsP S4 (rem _ tripletDec t L) S2)).
intros L S1 S2 H'; Elimc H'; clear L S1 S2; auto.
intros S1 S2 S3 L t H' H'0 H'1 H'2 t0 H'3.
case (tripletDec t t0); intros H.
elim (H'2 t);
[ intros H'6
| intros H'6; Elimc H'6; intros S0 E; Elimc E; intros S4 E; Elimc E;
intros H'6 H'7; Elimc H'7; intros H'7 H'8
| idtac ]; auto.
right; S1; S2; split; auto; split; auto.
rewrite <- H; auto.
rewrite <- H; auto.
right; S1; S2; split; auto; split; auto.
rewrite <- H; auto.
apply doTripletsRTrans with (S2 := S0); auto.
rewrite <- H; auto.
apply doTripletsComp with (S1 := S4) (S2 := S3); auto.
rewrite <- H; auto.
apply doTripletInvol with (t := t) (S1 := S1) (S2 := S2); auto.
apply doTripletsIncl with (L := rem triplet tripletDec t L); auto.
elim (H'2 t0);
[ intros H'6
| intros H'6; Elimc H'6; intros S0 E; Elimc E; intros S4 E; Elimc E;
intros H'6 H'7; Elimc H'7; intros H'7 H'8
| idtac ]; auto.
left.
apply doTripletsTrans with (S2 := S2) (t := t); auto.
right; S0; S4; split; [ idtac | split ]; auto.
apply doTripletsTrans with (S2 := S2) (t := t); auto.
Qed.

Theorem doTripletsTermEx :
(L : list triplet) (S1 S2 : State),
doTripletsP S1 L S2
eqState S1 S2
( t : triplet,
( S3 : State,
In t L
doTripletP S1 t S3 doTripletsP S3 (rem _ tripletDec t L) S2)).
intros L S1 S2 H'; inversion H'; auto.
right; t; S3; split; try split; auto.
lapply (doTripletsTermExAux L S3 S2);
[ intros H'3; elim (H'3 t);
[ intros H'6
| intros H'6; Elimc H'6; intros S5 E; Elimc E; intros S6 E; Elimc E;
intros H'6 H'7; Elimc H'7; intros H'7 H'8
| idtac ]
| idtac ]; auto.
apply doTripletsRTrans with (S2 := S5); auto.
apply doTripletsComp with (S1 := S6) (S2 := S2); auto.
apply doTripletInvol with (t := t) (S1 := S1) (S2 := S3); auto.
apply doTripletsIncl with (L := rem triplet tripletDec t L); auto.
Qed.

Theorem doTripletsInclList :
(L1 L2 : list triplet) (S1 S2 : State),
incl L1 L2 doTripletsP S1 L1 S2 doTripletsP S1 L2 S2.
intros L1 L2 S1 S2 H' H'0; generalize L2 H'; elim H'0; clear H'0 H' L2; auto.
intros S3 S4 S5 L0 t H' H'0 H'1 H'2 L2 H'3.
apply doTripletsTrans with (S2 := S4) (t := t); auto with datatypes.
Qed.