Require Import Utf8.
Require Import List.

Inductive color: Set := black: color | white: color.

Definition is_white (c: color) := match c with black => False | white => True end.

Theorem not_black_n_white: ~(white=black).
intro.
apply eq_ind with (x:=white) (P:=is_white)(y:=black).
simpl ; split.
apply H.
Qed.

Definition invert (c: color) := match c with
    | black => white
    | white => black
end.

Lemma simple_invert: forall c: color, ~(invert c = c).
intro.
destruct c ; simpl ; intro ;
apply not_black_n_white ; rewrite H ; reflexivity.
Qed.

Lemma double_invert: forall c: color, invert (invert c) = c.
destruct c ; simpl ; reflexivity.
Qed.

Definition listc := (list color).

Fixpoint cc (u:color) (l: listc) {struct l} :=
match l with
    | nil => u
    | v::l' => match u with
        | black => cc v l'
        | white => cc (invert v) l'
        end
end.

Lemma cc_invert: forall l: listc, forall c: color, cc (invert c) l = invert (cc c l).
induction l ; intro.
simpl ; reflexivity.
simpl ; destruct c ;simpl ; rewrite IHl.
reflexivity.
rewrite double_invert.
reflexivity.
Qed.


(* rend un noir lorsqu'il y a un nombre pair de blancs *)
Fixpoint  parity (l: listc) :=
match l with
    | nil => black
    | u::l' => match u with
        | white => invert (parity l')
        | black =>  parity l'
        end
end.

(* les deux fonctions sont equivalentes *)
Theorem cc_parity: forall l: listc, forall c: color, cc c l =  parity (c::l).
induction l ; intro.
simpl.
destruct c ; reflexivity.
simpl cc ; destruct c.
rewrite IHl.
simpl ; reflexivity.
rewrite cc_invert.
rewrite IHl.
simpl.
reflexivity.
Qed.






(*
Variations ou extensions possibles
A TERMINER
ça serait bien de prouver directement cc_even sans la fonction parity
on pourrait aussi compter le nombre de blancs et dire que ce nombre est pair
*)


(*
(* nombre pair de blancs ? *)

Fixpoint even (l: listc) :=
match l with
    | nil =>True
    | u::l' => u=white/\~(even l') \/ u=black/\even l'
end.

Lemma parity_even: forall l: listc, (parity l)=black <-> even l.
induction l ; simpl ; split ; intro. split.
reflexivity.
destruct a ; [right | left] ; split.
reflexivity.
apply IHl ; apply H.
reflexivity.
intro.
destruct IHl.
rewrite H2 in H.
apply simple_invert with (c:=black) ; apply H.
apply H0.
destruct H ; destruct H ; rewrite H ; simpl.
destruct IHl as [H1 H2].
destruct parity.
destruct H0 ; apply H1 ; reflexivity.
simpl ; reflexivity.
destruct IHl as [H1 H2].
rewrite H2 ; [reflexivity|apply H0].
Qed.

Theorem cc_even: forall l: listc, forall c: color, (cc c l)=black <-> even (c::l).
intros.
rewrite cc_parity.
apply parity_even.
Qed.
*)