module
public import Mathlib.Algebra.Order.Field.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Nat.Dist
public import Mathlib.Data.Rat.Star
public import Mathlib.Order.Interval.Set.Infinite
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring
public section
/-!
# USA Mathematical Olympiad 2004, Problem 4
Alice and Bob play a game on a 6 by 6 grid. On his turn, a player chooses
a rational number not yet appearing in the grid and writes it in an empty square
of the grid. Alice goes first and then the players alternate. When all squares
have numbers written in them, in each row, the square with the greatest number in
that row is colored black. Alice wins if he can then draw a line from the top of
the grid to the bottom of the grid that stays in black squares, and Bob wins if
he can't. (If two squares share a vertex, Alice can draw a line from one to the
other that stays in those two squares.) Find, with proof, a winning strategy for
one of the players.
-/
namespace Usa2004P4
/-! ### The board, the pairing of cells, and the endgame -/
/-- A cell of the 6×6 grid: `(row, column)`, both in `Fin 6`.
Row `0` is the top row of the grid and row `5` the bottom row. -/
abbrev Cell : Type := Fin 6 × Fin 6
/-- Two cells are adjacent if their squares share a vertex (Chebyshev distance at most 1). -/
def Adj (x y : Cell) : Prop := Nat.dist x.1.1 y.1.1 ≤ 1 ∧ Nat.dist x.2.1 y.2.1 ≤ 1
/-- A cell is black if it contains the greatest number in its row. -/
def IsBlack (f : Cell → ℚ) (c : Cell) : Prop := ∀ d : Cell, d.1 = c.1 → f d ≤ f c
/-- Alice wins a finished board: there is a chain of black cells, consecutive cells
sharing a vertex, from the top row to the bottom row. -/
def AliceWins (f : Cell → ℚ) : Prop :=
∃ c d : Cell, c.1.1 = 0 ∧ d.1.1 = 5 ∧ IsBlack f c ∧ IsBlack f d ∧
Relation.ReflTransGen (fun x y => Adj x y ∧ IsBlack f x ∧ IsBlack f y) c d
/-- A play of the game: the sequence of 36 moves, each a cell together with the
rational number written in it. Alice makes the moves `0, 2, ..., 34` and Bob the
moves `1, 3, ..., 35`. The legality conditions are that all cells played are
distinct (a player must write in an empty square) and that all numbers played are
distinct (a player must choose a rational not yet appearing in the grid). -/
structure Play where
moves : Fin 36 → Cell × ℚ
cell_inj : Function.Injective fun i => (moves i).1
val_inj : Function.Injective fun i => (moves i).2
/-- The board after the first `n` moves of a play. -/
noncomputable def prefBoard (p : Play) (n : ℕ) : Cell → Option ℚ :=
fun c => if h : ∃ i : Fin 36, (i : ℕ) < n ∧ (p.moves i).1 = c
then some (p.moves h.choose).2
else none
/-- The final board of a play: after 36 moves every cell is filled (see
`prefBoard_finalBoard`), and this is the number written in each cell. -/
noncomputable def finalBoard (p : Play) : Cell → ℚ :=
fun c => (prefBoard p 36 c).getD 0
/-- A play follows Bob's strategy `σ` if each of Bob's moves (the odd-numbered
moves) is the move prescribed by `σ` on the current board. -/
def FollowsStrategy (σ : (Cell → Option ℚ) → Cell × ℚ) (p : Play) : Prop :=
∀ k : Fin 36, Odd (k : ℕ) → p.moves k = σ (prefBoard p k)
/-- **USAMO 2004, Problem 4.** Bob (the second player) has a winning strategy:
whenever the play follows Bob's strategy `σ` of answering a move in the first two
rows by a suitable number in the paired cell (and playing anywhere in rows 3 to 6
otherwise), the final board has no black path from the top row to the bottom row,
so Alice cannot win. -/
theorem usa2004_p4 :
∃ σ : (Cell → Option ℚ) → Cell × ℚ,
∀ p : Play, FollowsStrategy σ p → ¬ AliceWins (finalBoard p) := sorry
end Usa2004P4
This problem has a complete formalized solution.