Set Implicit Arguments.

Require Import tp2.

Definition invariant (M : Set)(f : board -> M) := ???

Lemma invariant_move : forall (M:Set)(f:board->M),
???	->(invariant f).
Proof.
???
Qed.

Lemma invariant_not_moves : forall (M:Set)(f:board->M), 
  (invariant f) -> forall (b1 b2:board), ~((f b1)=(f b2))->~(moves b1 b2).
Proof.
intros M f If b1 b2 nf mb12.
???
Qed.

Definition involution (M : Set) (f : M -> M) := ???.

Lemma triple_map_inv : forall (M:Set)(f:M->M), ???
Proof.
???
Qed.

Lemma triple_map_select_inv : forall (M : Set)(f : M -> M)(p : pos),
???
Proof.
???
Qed.

Lemma turn_color_inv : ???
Proof.
???
Qed.

Lemma turn_line_inv : forall (p:pos), (involution (turn_line p)).
Proof.
intros p x; unfold turn_line.
???
Qed.

Lemma turn_col_inv : ??
Proof.
???
Qed.


Lemma move_sym : ???.
Proof.
intros b1 b2 mb12.
case mb12; intros p.
pattern b1 at 2. 
replace b1 with (turn_line p (turn_line p b1)).
???
Qed.

Lemma moves_sym : ???
Proof.
intros b1 b2 Ib12; induction Ib12.
???
Qed.


(* Une fonction de normalisation pour les damiers, on retourne lignes 
   et colonnes de maniere à n'avoir que des blancs sur la premiere ligne
   et la premiere colonne *)

Definition force_white_line (p : pos)(b : board) : board := 
  match (proj_board p A b) with
    ???
  end.

Definition force_white_col (p : pos)(b : board) : board := 
???
.

Lemma force_white_line_moves 
	: forall (p:pos)(b:board), (moves b (force_white_line p b)).
Proof.
unfold force_white_line; intros p b.
case (proj_board p A b).
???
Qed.



Lemma force_white_col_moves 
	: forall (p:pos)(b:board), (moves b (force_white_col p b)).
Proof.
???
Qed.

Definition force_white (b : board) : board := ???


(* Preuve que la fonction de mise en forme normale 
   préserve les deplacements *)

Lemma force_white_moves : forall (b:board), ??
intros; unfold force_white.
???
Qed.

Lemma force_eq_moves : forall (b1 b2:board), 
  (force_white b1) = (force_white b2)- > (moves b1 b2).
intros b1 b2 E.
apply moves_trans with (force_white b1).
apply force_white_moves.
rewrite E.
apply moves_sym.
apply force_white_moves.
Qed.


Lemma move_force_eq : forall (b1 b2:board), 
  (move b1 b2)->(force_white b1)=(force_white b2). 
intros b1 b2 mb12.

case b1; intros l1 l2 l3; case l1; intros x1 y1 z1; case l2; intros x2 y2 z2; 
case l3; intros x3 y3 z3; simpl.

case b2; intros u1 u2 u3; case u1; intros a1 a2 a3; case u2; intros c1 c2 c3; 
case u3; intros d1 d2 d3.
(*
case x1; case x2; case x3; case a1; case a2; case a3; case c1; case c2; case c3; case d1; case d2; case d3;
case y1; case y2; case y3; case z1; case z2; case z3; trivial.
*)
Admitted.


Lemma moves_force_eq :???

intros b1 b2 h.
apply invariant_move; trivial.
apply move_force_eq.
Qed.


Definition dec_eq (M : Set) := forall (x y:M), {x=y}+{~x=y}.

Lemma dec_eq_triple : forall (M:Set), (dec_eq M)->(dec_eq (triple M)).
intros M eqdM u v.
case u; intros x1 x2 x3; case v; intros y1 y2 y3.
???
Defined.


Lemma dec_eq_color : ??
Proof.
unfold dec_eq; decide equality.
Defined.

Lemma dec_eq_board : (dec_eq board).
Proof.
unfold board.
???
Defined.

Lemma moves_dec : forall (b1 b2:board), {(moves b1 b2)}+{~(moves b1 b2)}.
intros; case (dec_eq_board (force_white b1) (force_white b2)).
???
Defined.

Definition moves_dec_fun (b1 b2 : board) : bool :=
	if (moves_dec b1 b2) then true else false.

Lemma moves_proof : forall (b1 b2:board), ?? = ?? -> ???
Proof.
unfold moves_dec_fun; intros b1 b2.
???
Defined.

Lemma not_moves_proof :  forall (b1 b2:board), ?? = ?? -> ???
Proof.
???
Qed.

Lemma accessible_auto : (moves start target).
apply moves_proof. 
reflexivity.
Qed.

Lemma not_accessible_auto : ~(moves start white_board).
apply not_moves_proof.
reflexivity.
Qed.