(**************************************************************************)
(*                Le damier de Cachan 2                                   *)
(*                  Coq V7.0                                              *)
(**************************************************************************)
(* Méthode systématique de preuve d'atteignabilité pour le jeu du damier  *)
Set Implicit Arguments.

(* Nécessite d'avoir compiler le fichier damier.v 
   par la commande coqc damier, on peut aussi faire Load damier *)
Require damier.

(* I-Invariant
   Un invariant est une fonction sur les damiers qui est préservée par les 
   jeux 
*)

Definition invariant 
	:= [M:Set][f:board->M](b1,b2:board)(moves b1 b2)->(f b1)=(f b2).

Lemma invariant_move : (M:Set)(f:board->M)
	((b1,b2:board)(move b1 b2)->(f b1)=(f b2))
	->(invariant f).
....
Hints Resolve invariant_move.

Lemma invariant_not_moves : (M:Set)(f:board->M)(invariant f)
	->(b1,b2:board)~((f b1)=(f b2))->~(moves b1 b2).
...
Save.


(* II-Fonctions involutives                                           *)
(* On établit que les fonctions turn_line et turn_color sont des *)
(* involutions, pour cela on prouve que les fonctions triple_map et  *)
(* triple_map_select preservent les involutions                      *)

Definition involution := [M:Set][f:M->M](x:M)(f (f x))=x.

Lemma triple_map_inv 
 : (M:Set)(f:M->M)(involution f)->(involution (triple_map f)).
Red; Intros.
Case x; Simpl.
Intros; Repeat Rewrite H; Trivial.
Save.

Lemma triple_map_select_inv 
 : (M:Set)(f:M->M)(p:pos)(involution f)->(involution (triple_map_select f p)).
Red; Intros.
Case x; Case p; Simpl; Intros; Rewrite H; Trivial.
Save.

Lemma turn_color_inv : (involution turn_color).
Red.
Destruct x; Trivial.
Save.

Hints Resolve triple_map_inv triple_map_select_inv turn_color_inv.

Lemma turn_line_inv : (p:pos)(involution (turn_line p)).
Unfold turn_line board; Auto.
Save.

Lemma turn_col_inv : (p:pos)(involution (turn_col p)).
Unfold turn_col board; Auto.
Save.

(* III - Symétrie des relations move et moves *)

Lemma move_sym : (b1,b2:board)(move b1 b2)->(move b2 b1).
Destruct 1; Intros.
Pattern 2 b1; Replace b1 with (turn_line p (turn_line p b1)); Auto.
Apply (turn_line_inv p).
Pattern 2 b1; Replace b1 with (turn_col p (turn_col p b1)); Auto.
Apply (turn_col_inv p).
Save.
Hints Immediate move_sym.

Lemma moves_sym : (b1,b2:board)(moves b1 b2)->(moves b2 b1).
Induction 1; Intros; EAuto.
Save.
Hints Immediate moves_sym.


(* Une fonction de normalisation pour les damiers, on retourne ligne 
   et colonne de manière à n'avoir que des blancs sur la première ligne et 
   colonne *)

Definition force_white_


Definition force_white : board -> board := 
 [b]Cases b of

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

Lemma force_white_moves : (b:board)(moves b (force_white b)).

Hints Resolve force_white_moves.

(* On en déduit aisément que 2 damiers qui ont la même forme normale sont 
   dans la même orbite
*)
Lemma force_eq_moves 
	: (b1,b2:board)(force_white b1)=(force_white b2)->(moves b1 b2).


(* Réciproquement on veut établir que 2 damiers dans la même orbite ont 
   même forme normale. La preuve peut se faire par énumération des cas
*)
Lemma move_force_eq 
	: (b1,b2:board)(move b1 b2)->(force_white b1)=(force_white b2). 


Lemma moves_force_eq 
	: (b1,b2:board)(moves b1 b2)->(force_white b1)=(force_white b2). 


(* On a établi l'équivalence entre la relation moves et l'égalité des *)
(* formes normales. Pour décider de la relation moves, il suffit de   *)
(* décider de l'égalité de deux damiers *)

(* Decidabilité de l'égalité *)

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

Lemma dec_eq_triple : (M:Set)(dec_eq M)->(dec_eq (triple M)).
Red; Intros M eqdM (x1,x2,x3) (y1,y2,y3).
Case (eqdM x1 y1); Intro H.
Case (eqdM x2 y2); Intro H1.
Case (eqdM x3 y3); Intro H3.
Left; Rewrite H; Rewrite H1; Rewrite H3; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Defined.

(* Une tactique automatique construit la preuve de la décidabilité de *)
(* l'égalité sur les types construits sans paramètres                 *)

Require EqDecide.
Lemma dec_eq_color : (dec_eq color).
Red; Decide Equality.
Defined.

Lemma dec_eq_board : (dec_eq board).
Unfold board; Apply dec_eq_triple; Apply dec_eq_triple; Exact dec_eq_color.
Defined.

(* 
   Pour décider si deux damiers sont dans la même orbite, il suffit de 
   décider de l'égalité des formes normales
*)

Lemma moves_dec : (b1,b2:board){(moves b1 b2)}+{~(moves b1 b2)}.


Definition moves_dec_fun : board -> board -> bool := 
	[b1,b2](if (moves_dec b1 b2) then [_]true else [_]false).

Lemma moves_proof : (b1,b2:board)(moves_dec_fun b1 b2)=true -> (moves b1 b2).

Lemma not_moves_proof 
	: (b1,b2:board)(moves_dec_fun b1 b2)=false -> ~(moves b1 b2).

Lemma accessible_auto : (moves start target).

Lemma not_accessible_auto : ~(moves start white_board).