(**************************************************************************)
(*                Le damier de Cachan                                     *)
(*                  Coq V6.3.1                                            *)
(**************************************************************************)

(*            An exercice by Gilles Dowek                                 *)
(*            modified by Christine Paulin                                *)
(*            english version Benjamin Werner                             *)


(* We consider a minimal go-ban of size 3x3. On each intersection is a    *)
(* two-colored stone (one side white, one side black). At each step,      *)
(* one can either return a whole line or a whole column.                  *)
(* The aim is to study the positions which can be reached from a given    *)
(* inital state.                                                          *)


Implicit Arguments On.

(* I- Triples
        One defines the notion of triples of objects of a common
        type M. The go-ban will be represented as a triple of triples
        of booleans, standing for the stone on the corresponding 
        intersection.
        A three-valued type (A,B and C) allows to index the positions
        inside a triple.
*)

Section Polymorphic_Triple.

	Variable M : Set.

	Inductive triple : Set := ...

	Definition triple_x : M -> triple := [m](Triple m m m).

	Inductive pos : Set := A : pos | B : pos | C : pos.

        (* projection function accessing an element in a triple   *)
	Definition proj_triple : pos -> triple -> M := ...


	Variable f : M -> M.

        (* triple_map applies f to the 3 elements of the triple *)
	Definition triple_map : triple -> triple := ...

        (* triple_map_select applies f to the selected element of the triple *)
	Definition triple_map_select : pos -> triple -> triple := ...

End Polymorphic_Triple.

(* Note the modification of the types of the defined objects after the
closing of the section.  *)

(* II- Colors
        The possible colors of stones are modelized as a two-valued type
        (e.g. White and Black)
*)

Inductive color : Set := ...

Definition turn_color : color -> color := ...

(* We can test the defined function *)
Eval Compute in (turn_color White).

(* III- The board (ban) *)

Definition board := ...

Definition white_board : board := ...

Definition start : board 
	:= (Triple (Triple White White Black)
		   (Triple Black White White)
		   (Triple Black Black Black)).

Definition target : board 
	:= (Triple 
		(Triple Black Black White)
		(Triple White Black Black)
		(Triple Black Black Black)).

Definition proj_board : pos -> pos -> board -> color := ...

Definition flip_line : pos -> board -> board := ...

Definition flip_col : pos -> board -> board := ...

(* Test those new functions *)
Eval Compute in (flip_line A (flip_col B white_board)).

(* IV- Legal moves *)

Inductive move [b1:board] : board -> Prop := ...

(* Note one could use the following variant, without new inductive
definition : *)
(*
Definition move2 : board -> board -> Prop := 
	[b1,b2](EX p : pos | b2=(flip_line p b1)) \/ 
		(EX p : pos | b2=(flip_col p b1)).

Lemma move2_line : (b1:board)(p:pos)(move2 b1 (flip_line p b1)).
Intros; Left; Exists p; Trivial.
Save.
*)


(* To talk about reachable positions, we define the
reflexive-transitive closure of move:  *)

Inductive moves [b1:board]: board -> Prop := ...

Lemma move_moves : (b1,b2:board)(move b1 b2) -> (moves b1 b2).

(* That moves is actually transitive is proven by induction over the
predicate moves.                    *)
Lemma moves_trans 
	: (b1,b2,b3:board)(moves b1 b2)->(moves b2 b3)->(moves b1 b3).

(* We register these 2 lemma so that Auto can automatically use them. *)
Hints Resolve move_moves moves_trans.

(* We can show that the target board is accessible from start simply
by exhibiting the necessary moves. The rest is taken care of by the
reduction machinery. *)
Lemma acessible : (moves start target).

(* Now we want to show that the white board cannot be reached from      *)
(* start. Thatfore, we have to exhibit an invariant                     *)

Require Bool.

(* diff_color is true when its two arguments are not hte same color *)
Definition diff_color : color -> color -> bool := ...

(* the invariant is the parity of the number of white (resp. black)
stones in corners. We can simplify it as the parity of changes of
color between two horizontaly adjacent corners: *)

Definition odd_board := ...
                     
Eval Compute in (odd_board start).

Eval Compute in (odd_board target).

Eval Compute in (odd_board white_board).

Lemma odd_invariant_move : 
          (b1,b2:board)(move b1 b2) -> (odd_board b1) = (odd_board b2).

Hints Resolve odd_invariant_move.

Lemma odd_invariant_moves : 
              (b1,b2:board)(moves b1 b2) -> (odd_board b1) = (odd_board b2).

Hints Resolve odd_invariant_moves.

Lemma not_accessible : ~(moves start white_board).