# Solution: The Devil's Chessboard

With an 8 by 8 chessboard, you and your friend can escape! Number each square from 0 to 63, and then consider each number as a bit vector corresponding to its binary representation.
When your friend looks at the board, he will xor the bit vectors for every square on which a coin is heads. He will then point to the square whose bit vector corresponds to the result of this operation. Let f be the function which takes a board configuration and returns the bit vector of the square according to this operation.
The fact that the warden can point to any square means that you must be able to take any board configuration x to a board configuration y with a given bit vector result f(y) = w. You can do this by computing f(x) and then flipping the coin on the square f(x) xor w.
We see that this strategy generalizes to the case where the number of squares is 2 ^ n for any natural number n. Matt McCutchen sent me a very concise and clever argument as to why it is impossible when the number of squares k is not of this form:
"Let x be a square on the board, and let S(x) be the set of board configurations for which the friend points to x. Then S(x) must contain at least 2^k / k configurations, because each initial configuration must be able to reach at least one configuration in S(x) with one flip, but each configuration in S(x) can only be reached from k initial configurations. If k is not a power of two, then the configurations do not divide evenly and there's no way to have enough of them for every square."
I have yet to formalize these arguments to solve the puzzle in Coq. Rather, this Coq file shows that we can, in principle, brute-force the solution by trying every possible solution and seeing if it works. It makes for a good argument that, just as we care about efficiency of programs, we may also care about efficiency of proofs!

Require Lib.Iso Lib.Finite.
Require Import Lib.Omniscient.

Require Import Arith Decidable FunctionalExtensionality.

Require Import problem.

Thanks to http://homes.cs.washington.edu/~jrw12/dep-destruct.html for the following lemma.

Lemma fin_case :
n (P : Fin.t (S n) → Type),
(P Fin.F1) →
( x, P (Fin.FS x)) →
( x, P x).
Proof.
intros.
refine (match x as in Fin.t
return pf : = S n,
eq_rect Fin.t (S n) pf = x
P x with
| Fin.F1 __
| Fin.FS _ __
end eq_refl _).
- intros.
inversion pf.
subst.
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
auto.
- intros.
inversion pf.
subst.
rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
auto.
- rewrite <- Eqdep_dec.eq_rect_eq_dec by apply eq_nat_dec.
reflexivity.
Defined.

Lemma fin0empty : Fin.t 0 → False.
Proof.
intros. inversion H.
Defined.

Theorem finiteFin : (n : nat), finite (Fin.t n).
Proof.
induction n; unfold finite; intros.
- left. apply Fin.case0.
- unfold finite in IHn.
assert ( x : Fin.t n, decidable (P (Fin.FS x))).
induction x; apply f.
pose proof (IHn _ H); destruct H0;
pose proof (f Fin.F1); destruct H1;
try match goal with
| [ H: not _ |- _ ] ⇒ right; unfold not; intro ; apply H in ; assumption
end.
left. apply fin_case; assumption.
right. unfold not. intro . apply H0.
intros. apply ( (Fin.FS x)).
Defined.

Require Import Program.

Ltac simplWithEq :=
simpl; unfold eq_rect_r; rewrite <-? Eqdep.EqdepTheory.eq_rect_eq.

Lemma fin_case_F1 { n : nat } { P : Fin.t (S n) → Type }
(P0 : P Fin.F1) (PS : x : Fin.t n, P (Fin.FS x))
: fin_case n P P0 PS Fin.F1 = P0.
Proof.
simplWithEq. reflexivity.
Defined.

Lemma fin_case_FS { n : nat } { P : Fin.t (S n) → Type }
(P0 : P Fin.F1) (PS : x : Fin.t n, P (Fin.FS x))
(k : Fin.t n)
: fin_case n P P0 PS (Fin.FS k) = PS k.
Proof.
simplWithEq. reflexivity.
Defined.

Theorem coinFin2 : Iso.T Coin (True + True).
Proof.
apply Iso.Build_T with
(AtoB := fun xmatch x with
| Tailsinr I end )
(BtoA := fun xmatch x with
| inr ITails
end);
intro x; destruct x; try reflexivity;
try (destruct t; reflexivity).
Defined.

Theorem boardConfigIso (k : nat) : Iso.T (BoardConfig k) (Fin.t kTrue + True).
Proof.
unfold BoardConfig.
apply Iso.FuncCong.
apply Iso.Refl.
apply coinFin2.
Defined.

Fixpoint settimes (A : Set) (n : nat) : Set := match n with
| 0 ⇒ False
| S ⇒ (A + settimes A )%type
end.

Theorem finIso (k : nat) : Iso.T (Fin.t k) (settimes True k).
Proof.
induction k.
refine (
{| Iso.AtoB := fin0empty
; Iso.BtoA := False_rect (Fin.t 0)
|}); intros.
inversion a.
inversion b.
refine (
{| Iso.AtoB := fin_case k (fun _ settimes True (S k))
(inl I)
(fun inr (Iso.AtoB _ _ IHk ))
; Iso.BtoA := fun x match x with
| inl I Fin.F1
| inr y Fin.FS (Iso.BtoA _ _ IHk y)
end
|}); intros; simpl.
dependent destruction a; simplWithEq. reflexivity.
rewrite (Iso.AtoBack _ _ IHk). reflexivity.
destruct b. destruct t. simplWithEq. reflexivity.
simplWithEq. rewrite (Iso.BtoBack _ _ IHk). reflexivity.
Defined.

Lemma finSetTimes (k : nat) {A : Set} (f : Finite.T A)
: Finite.T (settimes A k).
Proof.
induction k.
apply Finite.F0.
apply Finite.FPlus.
apply f.
fold settimes.
apply IHk.
Defined.

Definition FFin (k : nat) : Finite.T (Fin.t k) :=
(Finite.FIso (finSetTimes k Finite.F1) (Iso.Sym (finIso k))).

Ltac proveFinite := match goal with
| [ |- Finite.T (?a × ?b) ] ⇒ apply Finite.FTimes
| [ |- Finite.T (?a → ?b) ] ⇒ apply Finite.func
| [ |- Finite.T (Fin.t _) ] ⇒ apply FFin
| [ |- Finite.T Coin ] ⇒ apply (Finite.FIso (Finite.FPlus Finite.F1 Finite.F1)); apply Iso.Sym; apply coinFin2
end.

Theorem finiteStrategy (k : nat) : Finite.T (Strategy k).
Proof.
apply (@Finite.FIso ((BoardConfig kFin.t kFin.t k) × (BoardConfig kFin.t k))).
repeat ((try unfold BoardConfig); proveFinite).

apply Iso.Build_T with
(AtoB := fun x ⇒ {| you_flip := fst x; friend_points := snd x |})
(BtoA := fun y(you_flip k y, friend_points k y)); intros; simpl.
destruct a. reflexivity.
destruct b. reflexivity.
Defined.

Theorem GeneralizedSolution : (k : nat), youWin k not (youWin k).
Proof.
intro k.
unfold Puzzle. unfold youWin. apply omniFinite. apply finiteStrategy.
intro strategy. apply finiteFinite.
eapply (Finite.FIso _ (Iso.Sym (boardConfigIso k))).
intro config.
apply finiteFinite. proveFinite.
intro flippedSquare.
unfold decidable.
apply dec_eq_fin´.
Grab Existential Variables.
proveFinite. proveFinite. apply (Finite.FPlus Finite.F1 Finite.F1).
Defined.

Definition PuzzleSolution : Puzzle := GeneralizedSolution (8 × 8).