Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2007P4

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Interval
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2007, Problem 4

An animal with n cells is a connected figure consisting of n equal-sized
square cells (equivalently, a polyomino with n cells). A dinosaur is an
animal with at least 2007 cells. It is said to be primitive if its cells
cannot be partitioned into two or more dinosaurs. Find with proof the
maximum number of cells in a primitive dinosaur.
-/

namespace Usa2007P4

/-- Two cells of the integer lattice are adjacent when they share an edge,
i.e. their Manhattan distance is `1`. -/
def gridAdj (a b : ℤ × ℤ) : Prop := (a.1 - b.1).natAbs + (a.2 - b.2).natAbs = 1

/-- The infinite grid graph on `ℤ × ℤ`: vertices are cells, edges join
edge-adjacent cells. -/
def gridGraph : SimpleGraph (ℤ × ℤ) where
  Adj := gridAdj
  symm := ⟨fun a b h => by
    have e1 : b.1 - a.1 = -(a.1 - b.1) := by ring
    have e2 : b.2 - a.2 = -(a.2 - b.2) := by ring
    show (b.1 - a.1).natAbs + (b.2 - a.2).natAbs = 1
    rw [e1, e2, Int.natAbs_neg, Int.natAbs_neg]
    exact h⟩
  loopless := ⟨fun a h => by simp [gridAdj] at h⟩

/-- An *animal* is a nonempty finite set of cells whose induced subgraph of
the grid graph is connected. -/
structure IsAnimal (s : Finset (ℤ × ℤ)) : Prop where
  nonempty : s.Nonempty
  preconnected : (gridGraph.induce (s : Set (ℤ × ℤ))).Preconnected

/-- A *dinosaur* is an animal with at least `2007` cells. -/
def IsDinosaur (s : Finset (ℤ × ℤ)) : Prop := IsAnimal s ∧ 2007 ≤ s.card

/-- `parts` is a partition of the animal `d` into two or more dinosaurs:
at least two pairwise disjoint dinosaurs whose union is `d`. -/
def IsDinoPartition (d : Finset (ℤ × ℤ)) (parts : Finset (Finset (ℤ × ℤ))) : Prop :=
  2 ≤ parts.card ∧
  (∀ p ∈ parts, IsDinosaur p) ∧
  (∀ p ∈ parts, ∀ q ∈ parts, p ≠ q → Disjoint p q) ∧
  parts.biUnion id = d

/-- A dinosaur is *primitive* if its cells cannot be partitioned into two or
more dinosaurs. -/
def IsPrimitive (d : Finset (ℤ × ℤ)) : Prop :=
  IsDinosaur d ∧ ¬ ∃ parts, IsDinoPartition d parts

/-- The answer to USAMO 2007 Problem 4. -/
/- determine -/ abbrev answer : ℕ := sorry

theorem usa2007_p4 :
    IsGreatest {n : ℕ | ∃ d : Finset (ℤ × ℤ), IsPrimitive d ∧ d.card = n} answer := sorry

end Usa2007P4

File author(s): Kimi K3

This problem has a complete formalized solution.