(******************** ****************************)
(*                Cachan-board                                      *)
(*                  Coq V8.1                                           *)
(********************** **************************)

(** * Cachan board *)

(** On a 3x3 board, there are black/white token.
   tokens are turned down (black<->white) by row or column.
   One studies the reachable positions
*)

Set Implicit Arguments.

(** ** Triples
      Write a type for a triple of arbitrary objects in a type M. 
      A board will be represented by a triple of triple of colors
      A position has 3 possible values (A,B,C) 
      each position corresponds to a place in the triple
*)

Section Polymorphic_Triple.

Variable M : Type.

Inductive triple : Type := Triple : M -> M -> M -> triple.

Notation "[ x | y | z ]" := (Triple x y z).

Definition triple_x (m : M) : triple := [ m | m | m ].

Variable f : M -> M.

Definition triple_map (t: triple) : triple :=
 match t with (Triple a  b  c) => [(f a) | (f b) | (f c)]
 end.

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

Definition triple_map_select (p : pos) (t:triple) : triple :=
 match t with (Triple a b c) => 
  match p with A => [(f a) | b | c]
	     | B => [a | (f b) | c]
	     | C => [a | b | (f c)]
		end
              end.

(* Projection of a triple according to a position *)
Definition proj_triple (p: pos) (t: triple) : M :=
  match t with (Triple a b c) => 
    match p with A => a | B => b | C => c end
  end.
(* Check proj_triple triple_map *)
End Polymorphic_Triple.
Notation "[ x | y | z ]" := (Triple x y z).

(* Print the type of defined objects after closing the section *)

(** ** Color : type with two values White and Black *)

Inductive color : Type := White : color | Black : color.

Definition turn_color (c: color) : color := 
  match c with White => Black | Black => White end.

(* Test the defined function *)
Eval compute in (turn_color White).

(** ** Board *)

Definition board := triple (triple color).

Definition turn_row (p: pos) : board -> board := 
  triple_map_select (triple_map turn_color) p.

Definition turn_col (p: pos) : board -> board := 
  triple_map (triple_map_select turn_color p).

Definition proj_board (x y: pos) (b:board) : color :=
	proj_triple y (proj_triple x b).

(* Test *)

Definition white_board : board 
	:= triple_x (triple_x White).

Eval compute in (turn_row A (turn_col B white_board)).

Definition start : board 
	:= [ [White | White | Black] |
	     [Black | White | White] |
	     [Black | Black | Black] ].

Definition target : board 
	:= [ [Black | Black | White] |
	     [White | Black | Black] |
	     [Black | Black | Black] ].

(** More on inductive definitions *)
Definition is_white : color -> Prop := 
  fun c => match c with White => True | Black => False end.

Definition T : color -> Type := 
  fun c => match c with White => bool | Black => nat end.

Definition f (x:color) : T x := 
   match x with White => true | Black => 2 end.

Lemma black_not_white : ~ (Black = White).
(* discriminate. *)
intro H.
change (is_white Black).
rewrite H.
simpl.
trivial.
(* discriminate *)
Save.

Definition pr1 M (t:triple M) : M := let (x,y,z) := t in x.

Lemma inj1 : forall M (x1 x2 x3 y1 y2 y3:M),
   [x1 | x2 | x3] = [y1 | y2 | y3] -> x1 = y1.
(* intros; injection H *)
intros; change (pr1 [x1 | x2 | x3] = pr1 [y1 | y2 | y3]).
rewrite H.
simpl.
reflexivity.
Save.

(** ** Possible moves *)
Definition move1 (b1 b2: board) : Prop := 
    (exists p : pos, b2=turn_row p b1) 
\/  (exists p : pos, b2=turn_col p b1).

Lemma move1_row : forall (b1:board)(p:pos),
      move1 b1 (turn_row p b1).
Admitted.

(** Inductive equivalent definition *)

Inductive move (b1:board) : board -> Prop :=
  move_row : forall (p:pos), move b1 (turn_row p b1)
| move_col  : forall (p:pos), move b1 (turn_col p b1).


Inductive moves (b1:board): board -> Prop := 
  moves_init : moves b1 b1
| moves_step : forall (b2 b3:board),
   moves b1 b2 -> move b2 b3 -> moves b1 b3.

Hint Constructors move moves. 

Lemma move_moves : forall (b1 b2:board), move b1 b2 -> moves b1 b2.
(* eauto. *)
intros.
apply moves_step with b1.
trivial.
trivial. 
Save.
Hint Resolve move_moves.

(** Target is reachable from start *)
Lemma reachable : moves start target.
apply moves_step with (turn_row A start); auto.
replace target with (turn_row B (turn_row A start)); auto.
Save.

(** transitivity *)

Lemma moves_trans : forall (b1 b2 b3:board), 
   moves b1 b2 -> moves b2 b3 -> moves b1 b3.
(* Check moves_ind *)
induction 2.
trivial.
eauto.
Save.
Hint Resolve moves_trans.




(** White_board cannot be accessed from start *)

(*
Lemma not_reachable : ~ moves start white_board.
intro.
induction H.
*)

Require Export Bool.

(** Function which decides if two colors are different *)
Definition diff_color (c1 c2 : color) : bool :=
  match c1,c2 with 
                    Black,White => true
                  | White,Black => true
                  | _ ,_        => false
  end.

(** [odd_board b] is true when there is an odd number of white tokens 
     at the 4 corners of the board *)

Definition odd_board (b:board) : bool := 
      xorb (diff_color (proj_board A A b) (proj_board A C b))
                     (diff_color (proj_board C A b) (proj_board C C b)).
                     
Eval compute in (odd_board start).

Eval compute in (odd_board target).

Eval compute in (odd_board white_board).

Lemma odd_invariant_move : forall (b1 b2:board), 
      move b1 b2 -> odd_board b1 = odd_board b2.
(** look at all possible cases *)
destruct 1.
destruct b1 as ((x1,x2,x3),(y1,y2,y3),(z1,z2,z3)); 
destruct p; simpl; case x1; case x3; case z1; case z3;
simpl;intros;try contradiction; auto.
destruct b1 as ((x1,x2,x3),(y1,y2,y3),(z1,z2,z3)); 
destruct p; simpl; case x1; case x3; case z1; case z3;
simpl;intros;try contradiction; auto.
Save.

Hint Resolve odd_invariant_move.

Lemma odd_invariant_moves : 
    forall (b1 b2:board), moves b1 b2 -> odd_board b1 = odd_board b2.
induction 1;intros;trivial.
transitivity (odd_board b2);auto.
Save.

Hint Resolve odd_invariant_moves.

Lemma not_reachable : ~ moves start white_board.
intro.
assert (~ odd_board start=odd_board white_board).
compute.
discriminate.
auto.
Save.

(** The opposite is true 
    if odd_board b1 = odd_board b2 then moves b1 b2 
*)