module
public import Mathlib.Data.Fintype.Card
public import Mathlib.Data.Fintype.Prod
public import Mathlib.Data.Set.Operations
public import Mathlib.Order.Bounds.Defs
public section
/-!
# International Mathematical Olympiad 2018, Problem 4
A site is any point (x, y) in the plane for which x, y ∈ {1, . . . , 20}.
Initially, each of the 400 sites is unoccupied. Amy and Ben take turns
placing stones on unoccupied sites, with Amy going first; Amy has the
additional restriction that no two of her stones may be at a distance
equal to √5. They stop once either player cannot move. Find the greatest
K such that Amy can ensure that she places at least K stones.
## Formalization notes
* We use 0-indexed coordinates, so a site is an element of
`Fin 20 × Fin 20`.
* Two sites are at distance `√5` exactly when they are a knight's move
apart: their coordinate differences are 1 and 2 in some order
(`KnightAdj`).
* `CanEnsure K fuel red blue` says that from the position with red
stones on `red`, blue stones on `blue`, and Amy to move, Amy can
ensure that she places at least `K` stones in total. The `fuel`
parameter bounds the number of rounds left to play; every round
occupies two new sites, so `CanEnsure K 400 ∅ ∅` (with fuel exceeding
any possible length of play) is the exact game-theoretic meaning of
"Amy can ensure at least `K` stones", abbreviated `AmyEnsures K`.
The answer is `K = 100`.
-/
namespace Imo2018P4
/-- A site on the board: the 0-indexed version of `{1, ..., 20}²`. -/
abbrev Site : Type := Fin 20 × Fin 20
/-- Two sites are at distance `√5` iff they are a knight's move apart,
i.e. their coordinate differences are `(±1, ±2)` or `(±2, ±1)`. -/
def KnightAdj (a b : Site) : Prop :=
(a.1.val + 1 = b.1.val ∧ a.2.val + 2 = b.2.val) ∨
(a.1.val + 2 = b.1.val ∧ a.2.val + 1 = b.2.val) ∨
(a.1.val + 1 = b.1.val ∧ b.2.val + 2 = a.2.val) ∨
(a.1.val + 2 = b.1.val ∧ b.2.val + 1 = a.2.val) ∨
(b.1.val + 1 = a.1.val ∧ a.2.val + 2 = b.2.val) ∨
(b.1.val + 2 = a.1.val ∧ a.2.val + 1 = b.2.val) ∨
(b.1.val + 1 = a.1.val ∧ b.2.val + 2 = a.2.val) ∨
(b.1.val + 2 = a.1.val ∧ b.2.val + 1 = a.2.val)
instance (a b : Site) : Decidable (KnightAdj a b) := by
unfold KnightAdj; infer_instance
/-- The sites on which Amy may place a stone: the unoccupied sites at
distance different from `√5` from every red stone. -/
def amyMoves (red blue : Finset Site) : Finset Site :=
(Finset.univ \ (red ∪ blue)).filter fun a => ∀ r ∈ red, ¬ KnightAdj a r
/-- The sites on which Ben may place a stone: all unoccupied sites. -/
def benMoves (red blue : Finset Site) : Finset Site :=
Finset.univ \ (red ∪ blue)
/-- With `fuel` rounds left to play, Amy can ensure from the position
`(red, blue)` (with Amy to move) that she places at least `K` stones in
total. (An inductive predicate so that definitions and proofs do not
have to unfold a recursion on the `fuel` parameter.) -/
inductive CanEnsure (K : ℕ) : ℕ → Finset Site → Finset Site → Prop
/-- If Amy already has `K` stones, she is done. -/
| zero {red blue : Finset Site} (h : K ≤ red.card) : CanEnsure K 0 red blue
/-- If Amy has no legal move, the game stops; she needs to already
have `K` stones. -/
| of_no_move {fuel : ℕ} {red blue : Finset Site} (hm : amyMoves red blue = ∅)
(h : K ≤ red.card) : CanEnsure K (fuel + 1) red blue
/-- Amy plays `a`; if Ben cannot reply the game stops and she needs
`K` stones; otherwise she must still ensure `K` stones after every
reply of Ben. -/
| of_move {fuel : ℕ} {red blue : Finset Site} {a : Site} (ha : a ∈ amyMoves red blue)
(hend : benMoves (insert a red) blue = ∅ → K ≤ (insert a red).card)
(hcont : ∀ b ∈ benMoves (insert a red) blue,
CanEnsure K fuel (insert a red) (insert b blue)) :
CanEnsure K (fuel + 1) red blue
/-- Amy can ensure that she places at least `K` stones. (400 rounds of
fuel exceeds any possible length of play, since every round occupies two
new sites of the 400.) -/
def AmyEnsures (K : ℕ) : Prop := CanEnsure K 400 ∅ ∅
/- determine -/ abbrev answer : ℕ := sorry
theorem imo2018_p4 : IsGreatest {K | AmyEnsures K} answer := sorry
end Imo2018P4
This problem has a complete formalized solution.