Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2017P3

module

public import Mathlib.Algebra.Order.Archimedean.Real.Hom
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# International Mathematical Olympiad 2017, Problem 3

A hunter and an invisible rabbit play a game in the Euclidean plane.
The rabbit's starting point, A₀, and the hunter's starting point, B₀,
are the same. After n − 1 rounds of the game, the rabbit is at point
A_{n−1} and the hunter is at point B_{n−1}. In the n-th round of the game,
three things occur in order:

(i) The rabbit moves invisibly to a point Aₙ such that the distance
    between A_{n−1} and Aₙ is exactly 1.
(ii) A tracking device reports a point Pₙ to the hunter. The only
    guarantee provided by the tracking device to the hunter is that the
    distance between Pₙ and Aₙ is at most 1.
(iii) The hunter moves visibly to a point Bₙ such that the distance
    between B_{n−1} and Bₙ is exactly 1.

Is it always possible, no matter how the rabbit moves, and no matter what
points are reported by the tracking device, for the hunter to choose her
moves so that after 10⁹ rounds she can ensure that the distance between
her and the rabbit is at most 100?

-/

namespace Imo2017P3

open InnerProductSpace

/-- Points of the Euclidean plane. -/
abbrev Pt := EuclideanSpace ℝ (Fin 2)

/-- The number of rounds in the game. -/
def totalRounds : ℕ := 10 ^ 9

/-- A hunter strategy: given the list of points reported by the tracking
device in rounds `1, ..., n` (in chronological order), choose the hunter's
position `Bₙ`. The hunter's move may depend only on the reported points,
not on the rabbit's actual positions. -/
abbrev Strategy := List Pt → Pt

/-- A strategy is valid if the hunter starts at the common starting point
`0` and moves by exactly `1` in every round, whatever is reported. -/
def ValidStrategy (σ : Strategy) : Prop :=
  σ [] = 0 ∧ ∀ (L : List Pt) (q : Pt), dist (σ L) (σ (L ++ [q])) = 1

/-- The reports made in rounds `1, ..., n`, as a list in chronological order. -/
def reportList (p : ℕ → Pt) : ℕ → List Pt
  | 0 => []
  | (n + 1) => reportList p n ++ [p (n + 1)]

/-- The hunter's position after round `n` when using strategy `σ` against
the reported points `p 1, ..., p n`. -/
def hunterPos (σ : Strategy) (p : ℕ → Pt) (n : ℕ) : Pt := σ (reportList p n)

/-- A rabbit path is valid if it starts at the common starting point `0`
and moves by exactly `1` in every round. -/
def ValidRabbit (A : ℕ → Pt) : Prop :=
  A 0 = 0 ∧ ∀ n, dist (A n) (A (n + 1)) = 1

/-- The reported points are valid for a rabbit path if each report is
within distance `1` of the rabbit's actual position. -/
def ValidReports (A p : ℕ → Pt) : Prop :=
  ∀ n, 1 ≤ n → dist (p n) (A n) ≤ 1

/-- The answer to the question "can the hunter always ensure that the distance
between her and the rabbit becomes at most 100?" is no. -/
/- determine -/ abbrev does_exist : Bool := sorry

theorem imo2017_p3 :
    if does_exist then
      ∃ σ : Strategy, ValidStrategy σ ∧
        ∀ A p : ℕ → Pt, ValidRabbit A → ValidReports A p →
          dist (A totalRounds) (hunterPos σ p totalRounds) ≤ 100
    else
      ¬ ∃ σ : Strategy, ValidStrategy σ ∧
        ∀ A p : ℕ → Pt, ValidRabbit A → ValidReports A p →
          dist (A totalRounds) (hunterPos σ p totalRounds) ≤ 100 := sorry

end Imo2017P3

File author(s): Kimi K3

This problem has a complete formalized solution.