module
public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Fintype.Card
public section
/-!
# USA Mathematical Olympiad 2017, Problem 4
Let P₁, P₂, ..., P_{2n} be 2n distinct points on the unit circle x² + y² = 1, other than
(1, 0). Each point is colored either red or blue, with exactly n red points and n blue
points. Let R₁, R₂, ..., Rₙ be any ordering of the red points. Let B₁ be the nearest
blue point to R₁ traveling counterclockwise around the circle starting from R₁. Then let
B₂ be the nearest of the remaining blue points to R₂ traveling counterclockwise around
the circle from R₂, and so on, until we have labeled all of the blue points B₁, ..., Bₙ.
Show that the number of counterclockwise arcs of the form Rᵢ → Bᵢ that contain the point
(1, 0) is independent of the way we chose the ordering R₁, ..., Rₙ of the red points.
-/
namespace Usa2017P4
/-!
## Combinatorial setup
We cut the circle at (1, 0) and record the 2n points in counterclockwise order,
starting right after (1, 0), as the elements of `Fin (2 * n)`. The coloring is given
by `c : Fin (2 * n) → Bool` with `true` for red and `false` for blue. Traveling
counterclockwise from a point `r` one meets the positions `r + 1, r + 2, ...`
cyclically; the counterclockwise arc from `r` to `b` contains (1, 0) exactly when
`b.val < r.val`. The greedy labeling process is modeled by `wraps`, which counts the
arcs through (1, 0) produced when the red points are processed in a given order.
-/
section Geometry
variable {m : ℕ}
/-- Shift `p` forward (counterclockwise) by `d` positions, cyclically. -/
def shift (p : Fin m) (d : ℕ) : Fin m :=
⟨(p.val + d) % m, Nat.mod_lt _ (Nat.lt_of_le_of_lt (Nat.zero_le _) p.isLt)⟩
/-- The cyclic (counterclockwise) distance from `a` to `b`; it is `0` iff `a = b`. -/
def cdist (a b : Fin m) : ℕ := (b.val + m - a.val) % m
/-- `wrap r b` is `1` when the counterclockwise arc from `r` to `b` passes through
the cut point (1, 0), and `0` otherwise. -/
def wrap (r b : Fin m) : ℕ := if b.val < r.val then 1 else 0
end Geometry
section Process
variable {m : ℕ} (c : Fin m → Bool)
/-- The set of blue points that have not been used yet. -/
def avail (used : Finset (Fin m)) : Finset (Fin m) :=
Finset.univ.filter (fun b => c b = false ∧ b ∉ used)
/-- The nearest available blue point to `r`, going counterclockwise from `r`
(if one exists; otherwise, arbitrarily, `r` itself). -/
noncomputable def nb (used : Finset (Fin m)) (r : Fin m) : Fin m :=
if h : (avail c used).Nonempty then
Classical.choose (Finset.exists_min_image (avail c used) (cdist r) h)
else r
/-- The total number of arcs through (1, 0) produced when the red points listed in
`l` are processed in order, starting from the set `used` of already-taken blue
points. -/
noncomputable def wraps : List (Fin m) → Finset (Fin m) → ℕ
| [], _ => 0
| (r :: rs), used => wrap r (nb c used r) + wraps rs (insert (nb c used r) used)
end Process
/-- **USAMO 2017 Problem 4.** With the notation introduced above (points recorded in
counterclockwise order starting from (1, 0), `true` = red), the number of
counterclockwise arcs `Rᵢ → Bᵢ` containing (1, 0) does not depend on the ordering
`R₁, ..., Rₙ` of the red points. -/
theorem usa2017_p4 (n : ℕ) (hn : 0 < n) (c : Fin (2 * n) → Bool)
(hred : (Finset.univ.filter (fun i => c i = true)).card = n)
(l₁ l₂ : List (Fin (2 * n)))
(hnod₁ : l₁.Nodup) (hlen₁ : l₁.length = n) (hred₁ : ∀ r ∈ l₁, c r = true)
(hnod₂ : l₂.Nodup) (hlen₂ : l₂.length = n) (hred₂ : ∀ r ∈ l₂, c r = true) :
wraps c l₁ ∅ = wraps c l₂ ∅ := sorry
end Usa2017P4
This problem has a complete formalized solution.