module
public import Mathlib.Algebra.GroupWithZero.Nat
public import Mathlib.Data.Finset.Option
public import Mathlib.Data.Fintype.Perm
public import Mathlib.Data.Fintype.Pigeonhole
public section
/-!
# USA Mathematical Olympiad 2016, Problem 6
Integers n and k are given, with n ≥ k ≥ 2. You play the following game against
an evil wizard. The wizard has 2n cards; for each i = 1, ..., n, there are two
cards labeled i. Initially, the wizard places all cards face down in a row, in
unknown order. You may repeatedly make moves of the following form: you point to
any k of the cards. The wizard then turns those cards face up. If any two of the
cards match, the game is over and you win. Otherwise, you must look away, while
the wizard arbitrarily permutes the k chosen cards and then turns them back
face-down. Then, it is your turn again.
We say this game is winnable if there exist some positive integer m and some
strategy that is guaranteed to win in at most m moves, no matter how the wizard
responds. For which values of n and k is the game winnable?
-/
namespace Usa2016P6
open Finset
/-! ## The game model -/
/-- An arrangement of the `2n` cards: the label shown at each position. -/
abbrev Arrangement (n : ℕ) := Fin (2 * n) → Fin n
/-- An arrangement is valid when each of the `n` labels appears exactly twice. -/
def Arrangement.Valid {n : ℕ} (a : Arrangement n) : Prop :=
∀ ℓ : Fin n, (univ.filter fun i ↦ a i = ℓ).card = 2
/-- An observation made by the player: the set of queried positions, together
with the labels that were revealed (`none` outside the queried set). -/
abbrev Observation (n : ℕ) := Finset (Fin (2 * n)) × (Fin (2 * n) → Option (Fin n))
/-- A player strategy: from the list of past observations, choose the next set
of positions to query. -/
abbrev Strategy (n : ℕ) := List (Observation n) → Finset (Fin (2 * n))
/-- A strategy is valid for the parameter `k` if it always queries exactly `k`
cards. -/
def Strategy.Valid {n : ℕ} (σ : Strategy n) (k : ℕ) : Prop :=
∀ h, (σ h).card = k
/-- The revealed labels, hidden (`none`) outside the queried set. -/
def reveal {n : ℕ} (a : Arrangement n) (Q : Finset (Fin (2 * n))) :
Fin (2 * n) → Option (Fin n) :=
fun i ↦ if i ∈ Q then some (a i) else none
/-- A wizard: an initial arrangement of the cards, and a way to permute the
queried cards after each unsuccessful query. -/
structure Wizard (n : ℕ) where
init : Arrangement n
perm : List (Observation n) → Finset (Fin (2 * n)) → Equiv.Perm (Fin (2 * n))
/-- A wizard plays legitimately if the initial arrangement has two cards of each
label and each permutation only moves the currently queried cards. -/
def Wizard.Valid {n : ℕ} (W : Wizard n) : Prop :=
W.init.Valid ∧ ∀ h Q i, i ∉ Q → W.perm h Q i = i
/-- The state of play: the current arrangement, the past observations, and
whether the player has already won. -/
structure PlayState (n : ℕ) where
arr : Arrangement n
hist : List (Observation n)
won : Bool
/-- One round of the game. -/
def step {n : ℕ} (σ : Strategy n) (W : Wizard n) (s : PlayState n) : PlayState n :=
if s.won then s
else
let Q := σ s.hist
if (Q.image s.arr).card = Q.card then
{ arr := s.arr ∘ W.perm s.hist Q
, hist := s.hist ++ [(Q, reveal s.arr Q)]
, won := false }
else { s with won := true }
/-- The state after `m` rounds of play. -/
def play {n : ℕ} (σ : Strategy n) (W : Wizard n) : ℕ → PlayState n
| 0 => { arr := W.init, hist := [], won := false }
| m + 1 => step σ W (play σ W m)
/-- The game is winnable if some valid strategy guarantees a win within `m`
moves against every legitimate wizard. -/
def Winnable (n k : ℕ) : Prop :=
∃ m ≥ 1, ∃ σ : Strategy n, σ.Valid k ∧ ∀ W : Wizard n, W.Valid → (play σ W m).won
/- determine -/ abbrev answer : ℕ → ℕ → Prop := sorry
theorem usa2016_p6 (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) : Winnable n k ↔ answer n k := sorry
end Usa2016P6
This problem has a complete formalized solution.