# Library problem

# Puzzle: The Devil's Chessboard

*exactly one*coin on the board.

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 :=

| Heads : Coin

| Tails : Coin.

Definition flip x := match x with

| Heads ⇒ Tails

| Tails ⇒ Heads

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.

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 k → Fin.t k → Fin.t k

; friend_points : BoardConfig k → Fin.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.

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 x ⇒ if 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.