module
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.SpecificLimits.Basic
public section
/-!
# International Mathematical Olympiad 2012, Problem 3
The liar's guessing game is a game played between two players A and B. The rules
of the game depend on two fixed positive integers k and n which are known to both
players.
At the start of the game A chooses integers x and N with 1 ≤ x ≤ N. Player A
keeps x secret, and truthfully tells N to player B. Player B now tries to obtain
information about x by asking player A questions as follows: each question consists
of B specifying an arbitrary set S of positive integers (possibly one specified in
some previous question), and asking A whether x belongs to S. Player B may ask as
many questions as he wishes. After each question, player A must immediately answer
it with yes or no, but is allowed to lie as many times as she wants; the only
restriction is that, among any k + 1 consecutive answers, at least one answer must
be truthful.
After B has asked as many questions as he wants, he must specify a set X of at
most n positive integers. If x belongs to X, then B wins; otherwise, he loses.
Prove that:
(a) If n ≥ 2^k, then B can guarantee a win.
(b) For all sufficiently large k, there exists an integer n ≥ (1.99)^k such that
B cannot guarantee a win.
-/
namespace Imo2012P3
/-!
## Game infrastructure
Since `1 ≤ x ≤ N` throughout the game, only the intersection of each question
(and of the final set `X`) with `{1, ..., N}` matters, so we model the candidates
as `Fin N`, questions as `Finset (Fin N)`, and answers as `Bool`
(`true` = "yes", `false` = "no"). Answers are indexed by `ℕ`: the `i`-th answer
is given after player B chooses his `i`-th move based on the previous answers.
-/
/-- A move of player B: either stop and guess a set `X`, or ask whether `x ∈ S`. -/
inductive Move (N : ℕ) where
| guess : Finset (Fin N) → Move N
| ask : Finset (Fin N) → Move N
/-- A strategy for player B: from the list of answers so far (in chronological
order), decide the next move. -/
structure Strategy (N : ℕ) where
move : List Bool → Move N
/-- The answer history after `t` questions, when player A answers according
to `ans`. -/
def hist (ans : ℕ → Bool) : ℕ → List Bool
| 0 => []
| t + 1 => hist ans t ++ [ans t]
/-- The `i`-th answer is truthful for the secret `x`: it matches the truth value
of `x ∈ S`, where `S` is the question B asked at that point. (If B guessed instead
of asking, the answer is vacuously truthful.) -/
def TruthfulAt {N : ℕ} (σ : Strategy N) (x : Fin N) (ans : ℕ → Bool) (i : ℕ) : Prop :=
∀ S : Finset (Fin N), σ.move (hist ans i) = Move.ask S → (x ∈ S ↔ ans i = true)
/-- The play is consistent with the secret `x` up to time `T`: among any `k + 1`
consecutive answers within the first `T`, at least one is truthful. -/
def ConsistentUpTo (k : ℕ) {N : ℕ} (σ : Strategy N) (x : Fin N) (ans : ℕ → Bool)
(T : ℕ) : Prop :=
∀ t : ℕ, t + k + 1 ≤ T → ∃ i : ℕ, t ≤ i ∧ i ≤ t + k ∧ TruthfulAt σ x ans i
/-- Player B's strategy `σ` guarantees a win if
1. against any answer sequence that stays consistent with `x` forever, B eventually
stops and guesses, and
2. whenever B guesses `X` at time `T` and the answers given so far are consistent
with `x`, then `x ∈ X` and `X` has at most `n` elements. -/
def GuaranteesWin (k n : ℕ) {N : ℕ} (σ : Strategy N) : Prop :=
(∀ (x : Fin N) (ans : ℕ → Bool), (∀ T, ConsistentUpTo k σ x ans T) →
∃ T X, σ.move (hist ans T) = Move.guess X) ∧
(∀ (x : Fin N) (ans : ℕ → Bool) (T : ℕ) (X : Finset (Fin N)),
σ.move (hist ans T) = Move.guess X → ConsistentUpTo k σ x ans T →
x ∈ X ∧ X.card ≤ n)
/-- Player B can guarantee a win with parameters `k, n` when player A's bound
is `N`. -/
def BobWins (k n N : ℕ) : Prop :=
∃ σ : Strategy N, GuaranteesWin k n σ
theorem imo2012_p3_part_a {k n : ℕ} (hk : 1 ≤ k) (hn : 2 ^ k ≤ n) (N : ℕ) :
BobWins k n N := sorry
theorem imo2012_p3_part_b :
∃ k₀ : ℕ, ∀ k ≥ k₀, ∃ n : ℕ, (1.99 : ℝ) ^ k ≤ (n : ℝ) ∧
¬ BobWins k n (n + 1) := sorry
end Imo2012P3
This problem has a complete formalized solution.