import Mathlib.Data.Real.Basic import Mathlib.Algebra.Order.Positive.Field import Mathlib.Tactic /-! # USA Mathematical Olympiad 2023, Problem 4 Positive integers a and N are fixed, and N positive integers are written on a blackboard. Alice and Bob play the following game. On Alice's turn, she must replace some integer n on the board with n + a, and on Bob's turn he must replace some even integer n on the board with n/2. Alice goes first and they alternate turns. If Bob has no valid moves on his turn the game ends. After analyzing the N integers on the board, Bob realizes that, regardless of what moves Alices makes, he will be able to force the game to end eventually. Show that, in fact, no matter what either player does, for these values of a and N and these particular N integers, the game is guaranteed to end, regardless of either player's moves. -/ namespace Usa2023P4 abbrev Blackboard (n : ℕ) : Type := Fin n → ℕ+ structure AliceMoveResult {n : ℕ} (a : ℕ+) (b0 : Blackboard n) where b : Blackboard n i : Fin n h1 : b0 i + a = b i h2 : ∀ j, j ≠ i → b0 j = b j abbrev AliceStrategy (n : ℕ) (a : ℕ+) := (b0 : Blackboard n) → AliceMoveResult a b0 abbrev NoValidMoves {n : ℕ} (b : Blackboard n) : Prop := ∀ i, Odd (b i).val inductive BobMoveResult {n : ℕ} (b0 : Blackboard n) where | halve : (b : Blackboard n) → (i : Fin n) → (b0 i = b i * 2) → (∀ j, j ≠ i → b0 j = b j) → BobMoveResult b0 | no_moves : NoValidMoves b0 → BobMoveResult b0 abbrev BobStrategy (n : ℕ) := (b0 : Blackboard n) → BobMoveResult b0 inductive Gamestate' (n : ℕ) where | active : Blackboard n → Gamestate' n | done : Gamestate' n /-- Alice and Bob each make a single move, in sequence. -/ def takeTurn {n : ℕ} (a : ℕ+) (as : AliceStrategy n a) (bs : BobStrategy n) : Gamestate' n → Gamestate' n | .done => .done | .active b => match bs (as b).b with | .halve b .. => .active b | .no_moves _ => .done def is_done {n : ℕ} : Gamestate' n → Prop | .done => True | _ => False theorem usa2023_p4 (a : ℕ+) (N : ℕ) (hN : 0 < N) (b0 : Blackboard N) (h1 : ∃ bs : BobStrategy N, ∀ as : AliceStrategy N a, ∃ k, is_done ((takeTurn a as bs)^[k] (.active b0))) : ∀ bs : BobStrategy N, ∀ as : AliceStrategy N a, ∃ k, is_done ((takeTurn a as bs)^[k] (.active b0)) := sorry

This problem does not yet have a complete solution.