module
public import Mathlib.Tactic
public import Mathlib.Algebra.IsPrimePow
public import Mathlib.Data.Finset.NatDivisors
public import Mathlib.NumberTheory.Divisors
public section
/-!
# International Mathematical Olympiad 1990, Problem 5
Given an initial integer n₀ > 1, two players A and B choose integers n₁, n₂, n₃, ...
alternately according to the following rules:
Knowing n₂ₖ, A chooses any integer n₂ₖ₊₁ such that n₂ₖ ≤ n₂ₖ₊₁ ≤ n₂ₖ².
Knowing n₂ₖ₊₁, B chooses any integer n₂ₖ₊₂ such that n₂ₖ₊₁/n₂ₖ₊₂ = p^r for some prime p
and integer r ≥ 1.
Player A wins the game by choosing the number 1990; player B wins by choosing the number 1.
For which n₀ does
(a) A have a winning strategy?
(b) B have a winning strategy?
(c) neither player have a winning strategy?
## Formalization notes
The proof follows a solution sketch after kalva.
-/
namespace Imo1990P5
/-- A legal move of player A: from the number `n` just chosen by B (or the initial
number `n₀`), A may choose any `m` with `n ≤ m ≤ n ^ 2` (A wins by choosing 1990). -/
@[reducible] def AMove (n m : ℕ) : Prop := n ≤ m ∧ m ≤ n ^ 2
/-- A legal move of player B: from the number `m` just chosen by A, B may choose any
`m'` such that `m / m'` is a prime power `p ^ r` with `r ≥ 1` (B wins by choosing 1). -/
@[reducible] def BMove (m m' : ℕ) : Prop := ∃ p r : ℕ, p.Prime ∧ 0 < r ∧ m = m' * p ^ r
/-- `AWins n`: it is A's turn and the current number is `n` (the initial position has
`n = n₀`), and A has a winning strategy. A either wins immediately by choosing 1990
(a legal move from `n`), or chooses a legal move `m` from which B cannot win
(B wins by choosing 1) and such that every legal answer of B is again a winning
position for A. -/
inductive AWins : ℕ → Prop
| win (n : ℕ) (h : AMove n 1990) : AWins n
| move (n m : ℕ) (h₁ : AMove n m) (h₂ : ¬ BMove m 1)
(h₃ : ∀ m', BMove m m' → AWins m') : AWins n
/-- `BWins m`: it is B's turn and the current number is `m`, and B has a winning
strategy. B either wins immediately by choosing 1, or chooses a legal move `m' ≠ 1`
from which A cannot win (A wins by choosing 1990) and such that every legal answer
of A is again a winning position for B. -/
inductive BWins : ℕ → Prop
| one (m : ℕ) (h : BMove m 1) : BWins m
| move (m m' : ℕ) (h : BMove m m') (h₁ : m' ≠ 1)
(h₂ : ∀ m'', AMove m' m'' → m'' ≠ 1990)
(h₃ : ∀ m'', AMove m' m'' → BWins m'') : BWins m
/-- `BWinsStart n`: B has a winning strategy from the initial position with `n₀ = n`
(it is A's turn): whatever legal first move `m` A makes, it is not 1990 and B wins
from `m`. -/
def BWinsStart (n : ℕ) : Prop := ∀ m, AMove n m → m ≠ 1990 ∧ BWins m
/- determine -/ abbrev aWinsSet : Set ℕ := sorry
/- determine -/ abbrev bWinsSet : Finset ℕ := sorry
/- determine -/ abbrev drawSet : Finset ℕ := sorry
theorem imo1990_p5 (n : ℕ) (hn : 2 ≤ n) :
(AWins n ↔ n ∈ aWinsSet) ∧ (BWinsStart n ↔ n ∈ bWinsSet) ∧
((¬ AWins n ∧ ¬ BWinsStart n) ↔ n ∈ drawSet) := sorry
end Imo1990P5
This problem has a complete formalized solution.