Skip to content

Commit

Permalink
[Imo2024P5] move solution comment into snip section
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha committed Nov 17, 2024
1 parent 59841bf commit d0a2df5
Showing 1 changed file with 12 additions and 11 deletions.
23 changes: 12 additions & 11 deletions Compfiles/Imo2024P5.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,19 +36,8 @@ game is over.
Determine the minimum value of $n$ for which Turbo has a strategy that guarantees reaching
the last row on the $n$th attempt or earlier, regardless of the locations of the monsters.
We follow the solution from the
[official solutions](https://www.imo2024.uk/s/IMO2024-solutions-updated.pdf). To show that $n$
is at least $3$, it is possible that the first cell Turbo encounters in the second row on his
first attempt contains a monster, and also possible that the first cell Turbo encounters in the
third row on his second attempt contains a monster. To show that $3$ attempts suffice, the first
attempt can be used to locate the monster in the second row; if this is not at either side of
the board, two more attempts suffice to pass behind that monster and from there go along its
column to the last row, while if it is at one side of the board, the second attempt follows a
zigzag path such that if it encounters a monster the third attempt can avoid all monsters.
-/


namespace Imo2024P5

/-! ### Definitions for setting up the problem -/
Expand Down Expand Up @@ -107,6 +96,18 @@ def Strategy.ForcesWinIn (s : Strategy N) (k : ℕ) : Prop :=

snip begin

/-
We follow the solution from the
[official solutions](https://www.imo2024.uk/s/IMO2024-solutions-updated.pdf). To show that $n$
is at least $3$, it is possible that the first cell Turbo encounters in the second row on his
first attempt contains a monster, and also possible that the first cell Turbo encounters in the
third row on his second attempt contains a monster. To show that $3$ attempts suffice, the first
attempt can be used to locate the monster in the second row; if this is not at either side of
the board, two more attempts suffice to pass behind that monster and from there go along its
column to the last row, while if it is at one side of the board, the second attempt follows a
zigzag path such that if it encounters a monster the third attempt can avoid all monsters.
-/

/-! ### API definitions and lemmas about `Cell` -/

/-- Reflecting a cell of the board (swapping left and right sides of the board). -/
Expand Down

0 comments on commit d0a2df5

Please sign in to comment.