module
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring
public section
/-!
# USA Mathematical Olympiad 2014, Problem 4
Let k be a positive integer. Two players A and B play a game on an infinite
grid of regular hexagons. Initially all the grid cells are empty. Then the
players alternately take turns with A moving first. In her move, A may choose
two adjacent hexagons in the grid which are empty and place a counter in both
of them. In his move, B may choose any counter on the board and remove it.
If at any time there are k consecutive grid cells in a line all of which
contain a counter, A wins. Find the minimum value of k for which A cannot
win in a finite number of moves, or prove that no such minimum value exists.
-/
namespace Usa2014P4
/-- A cell of the hexagonal grid, given in axial coordinates. -/
abbrev Cell := ℤ × ℤ
/-- The six unit steps between adjacent cells of the grid. -/
def offsets : Finset Cell := {(1, 0), (-1, 0), (0, 1), (0, -1), (1, -1), (-1, 1)}
/-- Two cells are adjacent when their difference is one of the six unit steps. -/
def Adj (c d : Cell) : Prop := (d.1 - c.1, d.2 - c.2) ∈ offsets
instance (c d : Cell) : Decidable (Adj c d) := by
unfold Adj
infer_instance
/-- The three (undirected) line directions of the grid. -/
def Dirs : Finset Cell := {(1, 0), (0, 1), (1, -1)}
/-- The cell reached from `p` by making `i` steps in direction `d`. -/
def step (p : Cell) (d : Cell) (i : ℕ) : Cell := (p.1 + (i : ℤ) * d.1, p.2 + (i : ℤ) * d.2)
/-- `A` has won on the board `s`: some line of `k` consecutive cells all carry
a counter. -/
def Winning (k : ℕ) (s : Finset Cell) : Prop :=
∃ d ∈ Dirs, ∃ p : Cell, ∀ i : ℕ, i < k → step p d i ∈ s
/-- A move of player `A`: place counters on two empty adjacent cells. -/
def AMove (s s' : Finset Cell) : Prop :=
∃ c₁ c₂ : Cell, c₁ ≠ c₂ ∧ Adj c₁ c₂ ∧ c₁ ∉ s ∧ c₂ ∉ s ∧ s' = insert c₁ (insert c₂ s)
/-- A move of player `B`: remove one counter from the board. -/
def BMove (s t : Finset Cell) : Prop := ∃ c ∈ s, t = s.erase c
/-- `AForce k s` means that from the board `s`, with `A` to move, `A` can force
a win in finitely many moves regardless of how `B` plays. Since the witness is
an inductive tree covering all of `B`'s responses, every play following the
strategy ends in a win after finitely many moves. -/
inductive AForce (k : ℕ) : Finset Cell → Prop
| of_win {s s'} : AMove s s' → Winning k s' → AForce k s
| of_step {s s'} : AMove s s' → (∀ t, BMove s' t → AForce k t) → AForce k s
/-- `A` can win the game with parameter `k` in finitely many moves. -/
def ACanWin (k : ℕ) : Prop := AForce k ∅
/- determine -/ abbrev solution : ℕ := sorry
theorem usa2014_p4 : IsLeast {k : ℕ | 0 < k ∧ ¬ ACanWin k} solution := sorry
end Usa2014P4
This problem has a complete formalized solution.