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)

/-- `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

/- 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.