Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2004P3

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 2004, Problem 3

Define a "hook" to be a figure made up of six unit squares as shown below
in the picture (a 3 × 3 square with the centre square, the middle square
of one side, and a corner square adjacent to that middle square removed),
or any of the figures obtained by applying rotations and reflections to
this figure.

Which m × n rectangles can be tiled by hooks?
-/

namespace Imo2004P3

/-- The cells of an `m × n` rectangle, as a finite subset of `ℤ × ℤ`. -/
def rect (m n : ℕ) : Finset (ℤ × ℤ) :=
  ((Finset.range m) ×ˢ (Finset.range n)).image fun p => ((p.1 : ℤ), (p.2 : ℤ))

/-- The eight orientations of the hook (rotations and reflections of the
figure in the problem statement). Each orientation is a `3 × 3` square with
three cells removed: the centre cell, the middle cell of one side, and a
corner cell adjacent to that middle cell. -/
def hookShapes : Finset (Finset (ℤ × ℤ)) :=
  { {(0, 0), (0, 1), (0, 2), (1, 0), (1, 2), (2, 0)},
    {(0, 0), (0, 1), (0, 2), (1, 0), (1, 2), (2, 2)},
    {(0, 0), (0, 1), (0, 2), (1, 0), (2, 0), (2, 1)},
    {(0, 0), (0, 1), (1, 0), (2, 0), (2, 1), (2, 2)},
    {(0, 0), (1, 0), (1, 2), (2, 0), (2, 1), (2, 2)},
    {(0, 2), (1, 0), (1, 2), (2, 0), (2, 1), (2, 2)},
    {(0, 1), (0, 2), (1, 2), (2, 0), (2, 1), (2, 2)},
    {(0, 0), (0, 1), (0, 2), (1, 2), (2, 1), (2, 2)} }

/-- A hook is a translate of one of the eight orientations. -/
def IsHook (s : Finset (ℤ × ℤ)) : Prop := ∃ σ ∈ hookShapes, ∃ t, s = σ.image (· + t)

/-- The six orientations of the two-hook "tiles" (pairs of interlocking
hooks): the `3 × 4` rectangle, the `4 × 3` rectangle, and the four
orientations of the zigzag shape. -/
def tileShapes : Finset (Finset (ℤ × ℤ)) :=
  { {(0, 0), (0, 1), (0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (1, 3), (2, 0), (2, 1), (2, 2), (2, 3)},
    {(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (2, 2), (3, 0), (3, 1), (3, 2)},
    {(0, 1), (0, 2), (0, 3), (1, 1), (1, 2), (1, 3), (2, 0), (2, 1), (2, 2), (3, 0), (3, 1), (3, 2)},
    {(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2), (2, 1), (2, 2), (2, 3), (3, 1), (3, 2), (3, 3)},
    {(0, 0), (0, 1), (1, 0), (1, 1), (1, 2), (1, 3), (2, 0), (2, 1), (2, 2), (2, 3), (3, 2), (3, 3)},
    {(0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (1, 3), (2, 0), (2, 1), (2, 2), (2, 3), (3, 0), (3, 1)} }

/-- A tile is a translate of one of the six tile shapes. -/
def IsTile (s : Finset (ℤ × ℤ)) : Prop := ∃ τ ∈ tileShapes, ∃ t, s = τ.image (· + t)

/-- `R` can be tiled by hooks: there is a finite family of pairwise
disjoint hooks whose union is `R`. -/
def Tileable (R : Finset (ℤ × ℤ)) : Prop :=
  ∃ 𝒯 : Finset (Finset (ℤ × ℤ)), (∀ H ∈ 𝒯, IsHook H) ∧
    (∀ H₁ ∈ 𝒯, ∀ H₂ ∈ 𝒯, H₁ ≠ H₂ → Disjoint H₁ H₂) ∧ R = 𝒯.biUnion id

/-- The predicate characterising the rectangles that can be tiled by hooks. -/
def GoodRect (m n : ℕ) : Prop :=
  m ≠ 1 ∧ m ≠ 2 ∧ m ≠ 5 ∧ n ≠ 1 ∧ n ≠ 2 ∧ n ≠ 5 ∧ (3 ∣ m ∨ 3 ∣ n) ∧ (4 ∣ m ∨ 4 ∣ n)

/-- The answer: exactly the rectangles with `{1, 2, 5} ∩ {m, n} = ∅`,
`3 ∣ mn` (i.e. `3 ∣ m` or `3 ∣ n`) and `4 ∣ mn` (i.e. `4 ∣ m` or `4 ∣ n`). -/
/- determine -/ abbrev answer : Set (ℕ × ℕ) := sorry

theorem imo2004_p3 (m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
    Tileable (rect m n) ↔ (m, n) ∈ answer := sorry

end Imo2004P3

File author(s): Kimi K3

This problem has a complete formalized solution.