# Puzzle: The Devil's Chessboard

The devil wants your and your friend's soul! He has offered to play a game.
The devil has an 8 by 8 chessboard, on which each square lies a coin which lies either heads up or tails up. He will bring you in to see the board, and then point to a particular square. You will not be able to communicate these data to your friend. After seeing the board and where the devil pointed, you must flip exactly one coin on the board.
You will be released and your friend will be brought in to see the modified board. Your friend must then point to exactly the square where the devil pointed earlier. If your friend points to the right square, you will both be freed. But if your friend is wrong, the devil will steal your souls!
Can you and your friend come up with a strategy to keep your souls that is guaranteed to succeed no matter what the initial configuration of the board, and no matter where the devil points? Or is it impossible to guarantee success in this devilish game?

Require Import Arith Decidable.
Require Fin.

Local Open Scope list.

Theorem dec_eq_fin : {k} (n m : Fin.t k), {n = m} + {n m}.
Proof.
apply Fin.rect2; try (intros k n).
- auto.
- right. unfold not. intros. inversion H.
- right. unfold not. intros. inversion H.
- intros m IH. inversion IH.
+ left. rewrite H. reflexivity.
+ right. unfold not. intros.
apply Fin.FS_inj in H0. apply (H H0).
Defined.

Theorem dec_eq_fin´ : {k} (n m : Fin.t k), decidable (n = m).
Proof. unfold decidable.
apply Fin.rect2; try (intros k n).
- auto.
- right. unfold not. intros. inversion H.
- right. unfold not. intros. inversion H.
- intros m IH. inversion IH.
+ left. rewrite H. reflexivity.
+ right. unfold not. intros.
apply Fin.FS_inj in H0. apply (H H0).
Defined.

Inductive Coin : Set :=
| Tails : Coin.

Definition flip x := match x with
end.

A board configuration, BoardConfig, maps each square on the chessboard to whether the coin on that square is heads or tails. The natural number k indicates the number of squares on the chessboard. We will formulate the problem generically in the number of squares on the chessboard.

Definition BoardConfig (k : nat) := Fin.t kCoin.

The Strategy that you and your friend come up with. You decide which coin to flip based on the board's configuration and where the devil pointed, while your friend must guess where the devil pointed solely based on the board configuration which your friend sees.

Record Strategy (k : nat) :=
{ you_flip : BoardConfig kFin.t kFin.t k
; friend_points : BoardConfig kFin.t k
}.

Definition flipBoard {k : nat}
(config : BoardConfig k) (flipi i : Fin.t k) :=
let x := config i in
if dec_eq_fin flipi i
then flip x
else x.

youWin k is the proposition that, playing the game on a chessboard with k squares, you and your friend have a strategy that is guaranteed to save your souls.

Definition youWin (k : nat) :=
(strategy : Strategy k),
(config : BoardConfig k) (devilPoint : Fin.t k),
let newConfig := flipBoard config (you_flip _ strategy config devilPoint)
in friend_points _ strategy newConfig = devilPoint.

Puzzle is our formal problem statement: can you find a strategy such that you and your friend are guaranteed to win on an 8 by 8 chessboard, or otherwise, can you prove that the devil will steal your souls no matter what?

Definition Puzzle := youWin (8 × 8) not (youWin (8 × 8)).

Theorem PuzzleSolution : Puzzle.
Proof.
Abort.

Looking for more of a challenge? Prove, for each possible size of chessboard, whether you and your friend have any chance at freedom.

Theorem GeneralizedSolution : (k : nat), youWin k not (youWin k).
Proof.
Abort.

As an example, we will show that you and your friend can save your souls, in a rather trivial manner, if the chessboard has only a single square.

Lemma fin1is0 : (n : Fin.t 1), Fin.F1 = n.
Proof.
apply (Fin.rectS (fun k xif beq_nat k 0 then Fin.F1 = x else True));
intros;
destruct (beq_nat n 0);
constructor.
Defined.

Example youWin1 : youWin 1.
Proof.
unfold youWin.
({| you_flip := fun _ _ Fin.F1 ; friend_points := fun _ @Fin.F1 0 |}).
intros. simpl. apply fin1is0.
Qed.