(**************************************************************************)
(* 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 flip over 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 := Triple : M -> M -> M -> triple.
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 :=
[p,t]Cases t of (Triple a b c) =>
Cases p of A => a | B => b | C => c end
end.
Variable f : M -> M.
Definition triple_map : triple -> triple :=
[t]Cases t of (Triple a b c) => (Triple (f a) (f b) (f c))
end.
Definition triple_map_select : pos -> triple -> triple :=
[p,t]Cases t of (Triple a b c) =>
Cases p of A => (Triple (f a) b c)
| B => (Triple a (f b) c)
| C => (Triple a b (f c))
end
end.
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.
Turning a stone is boolean negation
*)
Inductive color : Set := White : color | Black : color.
Definition turn_color : color -> color :=
[c]Cases c of White => Black | Black => White end.
(* We can test the defined function *)
Eval Compute in (turn_color White).
(* III- The board (ban) *)
Definition board := (triple (triple color)).
(* Note that the first argument of triple is synthesized, since
implicit arguments are turned on. *)
Definition flip_line : pos -> board -> board :=
[p](triple_map_select (triple_map turn_color) p).
Definition flip_col : pos -> board -> board :=
[p](triple_map (triple_map_select turn_color p)).
Definition proj_board : pos -> pos -> board -> color :=
[x,y,b](proj_triple y (proj_triple x b)).
(* Test *)
Definition white_board : board
:= (triple_x (triple_x White)).
Eval Compute in (flip_line A (flip_col B white_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)).
(* IV- Legal moves *)
Inductive move [b1:board] : board -> Prop :=
move_line : (p:pos)(move b1 (flip_line p b1))
| move_col : (p:pos)(move b1 (flip_col p b1)).
(* 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 :=
moves_init : (moves b1 b1)
| moves_step : (b2,b3:board)(moves b1 b2) -> (move b2 b3) -> (moves b1 b3).
Hints Resolve move_line move_col moves_init moves_step.
Lemma move_moves : (b1,b2:board)(move b1 b2) -> (moves b1 b2).
Intros; Apply moves_step with b1; Trivial.
Save.
(* 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).
Induction 2; EAuto.
Save.
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).
Apply moves_step with (flip_line A start); Auto.
Replace target with (flip_line B (flip_line A start)); Auto.
Save.
(* Now we want to show that the white board cannot be reached from *)
(* start. Thatfore, we have to exhibit an invariant *)
Require Bool.
Definition diff_color : color -> color -> bool :=
[c1,c2:color]
Cases c1 c2 of Black White => true
| White Black => true
| _ _ => false
end.
(* the invariant is the parity of the number of white (resp. white)
stones in corners. We can simplify it as the parity of changes of
color between two horizontaly adjacent corners: *)
Definition odd_board :=
[b:board](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 :
(b1,b2:board)(move b1 b2) -> (odd_board b1) = (odd_board b2).
(* One checks all possible states for the four corner stones (16) *)
(* and all possible moves (6) ! *)
(*
Unfold odd_board;Destruct 1;
Case b1; Intros l1 l2 l3; Case l1; Intros x1 x2 x3;
Case l2; Intros y1 y2 y3; Case l3; Intros z1 z2 z3;
Destruct p; Simpl; Case x1; Case x3; Case z1; Case z3;
Simpl;Intros;Contradiction Orelse Auto.
Save.
Hints Resolve odd_invariant_move.
Lemma odd_invariant_moves :
(b1,b2:board)(moves b1 b2) -> (odd_board b1) = (odd_board b2).
Induction 1;Intros;Trivial.
Transitivity (odd_board b0);Auto.
Save.
Hints Resolve odd_invariant_moves.
Lemma not_accessible : ~(moves start white_board).
Red;Intro.
Cut (~(odd_board start)=(odd_board white_board));Auto.
Compute.
Discriminate.
Save.
*)