the mutilated chessboard problem

mutilated.lean

/-
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad

The mutilated chessboard problem.

Consider an eight-by-eight chessboard and a set of dominos with the property that each domino
can cover exactly two adjacent chessboard squares. Remove the bottom left and top right corners.
The *mutilated chessboard problem* asks whether it is possible to cover the remaining squares
with nonoverlapping dominos. A simple observation shows that the answer is no: every domino
covers exactly one black square and one white square, and the two corners that have been removed
have the same color---say, white---so there are more white squares to be covered than black squares.
-/
import data.finset data.zmod.basic data.nat.parity tactic.norm_num tactic.omega
open finset nat

/- definitions -/

def chessboard := zmod 8 × zmod 8

instance : fintype chessboard := by unfold chessboard; apply_instance
instance : decidable_eq chessboard := by unfold chessboard; apply_instance

def mutilated : finset chessboard := univ \ {(0, 0), (7, 7)}

def right (u : chessboard) := (u.1 + 1, u.2)
def left  (u : chessboard) := (u.1 - 1, u.2)
def up    (u : chessboard) := (u.1, u.2 + 1)
def down  (u : chessboard) := (u.1, u.2 - 1)

@[derive decidable_eq]
inductive domino
| horizontal : chessboard → domino
| vertical   : chessboard → domino

open domino

def squares : domino → finset chessboard
| (horizontal u) := {u, right u}
| (vertical u)   := {u, up u}

def white (p : chessboard) : Prop := even (p.1.val + p.2.val)

instance : decidable_pred white := by intro; unfold white; apply_instance

abbreviation white_squares : finset chessboard := filter white finset.univ
abbreviation black_squares := univ \ white_squares

/- straightforward facts -/

private lemma aux₀ (n : nat) : even (n % 8) ↔ even n :=
by change even (n % 8) ↔ _; simp [even_iff, mod_mod_of_dvd _ (dec_trivial : 2 ∣ 8)]

private lemma aux₁ : (1 : zmod 8).val = 1 := rfl

private lemma aux₂ : (-1 : zmod 8).val = 7 := rfl

private lemma aux₃ (u : zmod 8) : ¬ (u + 1 = u) :=
begin
  intro h,
  have : u + 0 = u + 1, by simp [h],
  have : (0 : zmod 8) = (1 : zmod 8), from add_left_cancel this,
  have : 0 = 1, from congr_arg fin.val this,
  contradiction
end

local attribute [simp] aux₀ aux₁ aux₂ aux₃ filter_inter filter_insert filter_singleton

@[simp] lemma right_left (u : chessboard) : right (left u) = u :=
by simp [left, right]

@[simp] lemma left_right (u : chessboard) : left (right u) = u :=
by simp only [left, right, add_sub_cancel, prod.mk.eta]

@[simp] lemma right_ne (u : chessboard) : right u ≠ u :=
by cases u; simp [right]

@[simp] lemma up_ne (u : chessboard) : up u ≠ u :=
by cases u; simp [up]

@[simp] lemma white_right {u : chessboard} : white (right u) ↔ ¬ white u :=
by { simp [right, white, zmod.add_val] with parity_simps, by_cases even u.fst.val; simp *, }

@[simp] lemma white_left {u : chessboard} : white (left u) ↔ ¬ white u :=
by { simp [left, white, zmod.add_val] with parity_simps, by_cases even u.fst.val; simp * }

@[simp] lemma white_up {u : chessboard} : white (up u) ↔ ¬ white u :=
by { simp [up, white, zmod.add_val] with parity_simps, by_cases even u.fst.val; simp * }

@[simp] lemma white_down {u : chessboard} : white (down u) ↔ ¬ white u :=
by { simp [down, white, zmod.add_val] with parity_simps, by_cases even u.fst.val; simp * }

@[simp] lemma card_squares (d : domino) : card (squares d) = 2 :=
by cases d; simp [*, squares]

lemma card_squares_inter_white_squares : ∀ d, card (squares d ∩ white_squares) = 1
| (horizontal u) := by repeat { simp [squares]; split_ifs }
| (vertical u)   := by repeat { simp [squares]; split_ifs }

lemma card_squares_inter_black_squares (d : domino) : card (squares d ∩ black_squares) = 1 :=
have squares d ∩ black_squares = squares d \ (squares d ∩ white_squares),
  by { ext x, simp, tauto },
by rw [this, card_sdiff (inter_subset_left _ _), card_squares_inter_white_squares]; simp

/- the main argument -/

lemma card_white_squares : card white_squares = card black_squares :=
have h₁ : image right white_squares = black_squares,
  begin
    ext x, simp [@mem_filter _ white],
    show (∃ y, white y ∧ right y = x) ↔ ¬white x,
      from ⟨λ ⟨y, wy, eq⟩, by simp [eq.symm, wy], λ h, ⟨left x, by simp *⟩⟩,
  end,
have h₂ : ∀ u ∈ white_squares, ∀ v ∈ white_squares, right u = right v → u = v,
  by intros u _ v _ eq; rw [←left_right u, eq, left_right],
by rw [←h₁, card_image_of_inj_on h₂]

lemma card_mutilated_inter_black_squares :
  card (mutilated ∩ black_squares) = card (mutilated ∩ white_squares) + 2 :=
have h₁ : mutilated ∩ black_squares = black_squares,
  begin
    ext x, simp [mutilated],
    refine ⟨λ h, h.1, λ h, ⟨h, λ h', h _⟩ ⟩,
    cases h'; simp [*, white] with parity_simps
  end,
have h₂ : mutilated ∩ white_squares ∪ {(0, 0), (7, 7)} = white_squares,
  begin
    ext x, simp [mutilated], split,
    { rintro (rfl | rfl | ⟨_, h⟩), iterate 2 { simp [white] with parity_simps}, exact h },
    intro h, simp [h], rw [←or_assoc], apply classical.em
  end,
begin
  conv_lhs { rw [h₁, ←card_white_squares, ←h₂] },
  rw [card_disjoint_union],
  { simp, rw [card_insert_of_not_mem]; simp, intro h,
    have := congr_arg fin.val h, contradiction },
  simp [disjoint, white], refl
end

lemma card_bind_squares_inter_white_squares {s : finset domino}
    (h : ∀ u ∈ s, ∀ v ∈ s, u ≠ v → squares u ∩ squares v = ∅) :
  card (s.bind squares ∩ black_squares) = card (s.bind squares ∩ white_squares) :=
begin
repeat { rw [bind_inter, card_bind] },
  simp only [card_squares_inter_white_squares, card_squares_inter_black_squares],
  all_goals { intros, rw [inter_right_comm, ←inter_assoc, h]; tauto }
end

theorem mutilated_checkboard_problem {s : finset domino}
    (h : ∀ u ∈ s, ∀ v ∈ s, u ≠ v → squares u ∩ squares v = ∅) :
  s.bind squares ≠ mutilated :=
begin
  intro h',
  have := card_mutilated_inter_black_squares,
  rw [←h', card_bind_squares_inter_white_squares h] at this,
  have : 0 = 2, from add_left_cancel this,
  contradiction
end