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

Require damier_ex.

(* 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).
Red; Induction 2; Intros; Trivial.
Transitivity (f b0); Auto.
Save.
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).
Red; EAuto.
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_line : pos -> board -> board := 
	[p,b]Cases (proj_board p A b) of White => b 
					|Black => (turn_line p b)
	     end.

Lemma force_white_line_moves 
	: (p:pos)(b:board)(moves b (force_white_line p b)).
Unfold force_white_line; Intros.
Case (proj_board p A b); Auto.
Save.

Definition force_white_col : pos -> board -> board := 
	[p,b]Cases (proj_board A p b) of White => b 
					|Black => (turn_col p b)
	     end.

Lemma force_white_col_moves : (p:pos)(b:board)(moves b (force_white_col p b)).
Unfold force_white_col; Intros.
Case (proj_board A p b); Auto.
Save.

Definition force_white : board -> board := 
[b](force_white_line B
	(force_white_line C 
	(force_white_col A 
	(force_white_col B 
	(force_white_col C b))))).

Hints Resolve force_white_line_moves force_white_col_moves.

(* 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)).
Intros; Unfold force_white.
Apply moves_trans with (force_white_col C b); Auto.
Apply moves_trans with (force_white_col B (force_white_col C b)); Auto.
Apply moves_trans with (force_white_col A (force_white_col B 
	   			(force_white_col C b))); Auto.
Apply moves_trans with (force_white_line C (force_white_col A 
			(force_white_col B (force_white_col C b)))); Auto.
Save.
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).
Intros; Apply moves_trans with (force_white b1); Auto.
Rewrite H; Auto.
Save.

(* Réciproquement on veut établir que 2 damiers dans la même orbite ont 
   même forme normale.
*)
Lemma move_force_eq 
	: (b1,b2:board)(move b1 b2)->(force_white b1)=(force_white b2). 
Destruct 1.

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.

(* $3 * 2^9$ cas, prend 23 s en natif : *)
Time (Destruct p; Case x1; Case y1; Case z1; Case x2; Case y2; Case z2; 
	Case x3; Case y3; Case z3; Compute; Trivial).

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.

Time (Destruct p; Case x1; Case y1; Case z1; Case x2; Case y2; Case z2; 
	Case x3; Case y3; Case z3; Compute; Trivial).
Save.

Lemma moves_force_eq 
	: (b1,b2:board)(moves b1 b2)->(force_white b1)=(force_white b2). 
Change (invariant force_white).
Apply invariant_move.
Exact move_force_eq.
Save.

(* 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)}.
Intros; Case (dec_eq_board (force_white b1) (force_white b2)).
Left; Apply force_eq_moves; Auto.
Right; Apply invariant_not_moves with f:=force_white; Trivial.
Exact moves_force_eq.
Defined.


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).
Unfold moves_dec_fun; Intros b1 b2.
Case (moves_dec b1 b2); Simpl; [Trivial | Intros; Discriminate].
Save.

Lemma not_moves_proof 
	: (b1,b2:board)(moves_dec_fun b1 b2)=false -> ~(moves b1 b2).
Unfold moves_dec_fun; Intros b1 b2.
Case (moves_dec b1 b2); Simpl; [Intros; Discriminate | Trivial].
Save.

Lemma accessible_auto : (moves start target).
Apply moves_proof; Reflexivity.
Save.

Lemma not_accessible_auto : ~(moves start white_board).
Apply not_moves_proof; Reflexivity.
Save.