Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1974P4

module

public import Mathlib.Tactic
public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Data.Finset.Card
public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Finset.Powerset
public import Mathlib.Data.Finset.Prod
public import Mathlib.Order.Interval.Finset.Nat

public section


/-!
# International Mathematical Olympiad 1974, Problem 4

Consider decompositions of an 8 × 8 chessboard into p non-overlapping
rectangles, subject to the following conditions:

(i) Each rectangle has as many white squares as black squares.
(ii) If aᵢ is the number of white squares in the i-th rectangle, then
     a₁ < a₂ < ... < aₚ.

Find the maximum value of p for which such a decomposition is possible.
For this value of p, determine all possible sequences a₁, a₂, ..., aₚ.
-/

namespace Imo1974P4

/-- A rectangle on the chessboard, given by the coordinates `(r, c)` of its
top-left unit square, its height `h` (number of rows) and its width `w`
(number of columns). -/
structure Rect where
  r : ℕ
  c : ℕ
  h : ℕ
  w : ℕ
deriving DecidableEq

/-- The unit squares making up a rectangle. -/
def Rect.cells (R : Rect) : Finset (ℕ × ℕ) :=
  Finset.Icc (R.r, R.c) (R.r + (R.h - 1), R.c + (R.w - 1))

/-- The white squares of the chessboard are those whose coordinates have
even sum. -/
def isWhite (x : ℕ × ℕ) : Prop :=
  (x.1 + x.2) % 2 = 0

instance : DecidablePred isWhite :=
  fun x ↦ inferInstanceAs (Decidable ((x.1 + x.2) % 2 = 0))

/-- The number of white squares of a rectangle. -/
def Rect.whiteCount (R : Rect) : ℕ :=
  (R.cells.filter isWhite).card

/-- The number of black squares of a rectangle. -/
def Rect.blackCount (R : Rect) : ℕ :=
  (R.cells.filter fun x ↦ ¬ isWhite x).card

/-- The 8 × 8 chessboard. -/
def board : Finset (ℕ × ℕ) :=
  Finset.Icc (0, 0) (7, 7)

/-- A valid decomposition of the chessboard: a finite set of nonempty
rectangles contained in the board, pairwise disjoint, covering the whole
board, each having as many white squares as black squares (condition (i)),
and such that no two rectangles have the same number of white squares
(condition (ii)). -/
def ValidDecomp (T : Finset Rect) : Prop :=
  (∀ R ∈ T, 1 ≤ R.h ∧ 1 ≤ R.w ∧ R.r + R.h ≤ 8 ∧ R.c + R.w ≤ 8) ∧
  (∀ R₁ ∈ T, ∀ R₂ ∈ T, R₁ ≠ R₂ → R₁.cells ∩ R₂.cells = ∅) ∧
  T.biUnion Rect.cells = board ∧
  (∀ R ∈ T, R.whiteCount = R.blackCount) ∧
  (T.image Rect.whiteCount).card = T.card

instance (T : Finset Rect) : Decidable (ValidDecomp T) := by
  unfold ValidDecomp
  infer_instance

/- determine -/ abbrev solutions : Finset (Finset ℕ) := sorry

/-- The maximum possible number of white squares. -/
/- determine -/ abbrev maxCount : ℕ := sorry

theorem imo1974_p4 :
    (∀ T : Finset Rect, ValidDecomp T → T.card ≤ maxCount ∧
      (T.card = maxCount → T.image Rect.whiteCount ∈ solutions)) ∧
    ∀ s ∈ solutions, ∃ T : Finset Rect, ValidDecomp T ∧ T.card = maxCount ∧
      T.image Rect.whiteCount = s := sorry

end Imo1974P4

File author(s): Kimi K3

This problem has a complete formalized solution.