module
public import Mathlib.Tactic
public section
/-!
# International Mathematical Olympiad 1993, Problem 6
There are n > 1 lamps L₀, L₁, ..., Lₙ₋₁ in a circle. We use L_{n+k} to mean L_k.
A lamp is at all times either on or off. Initially they are all on.
Perform steps s₀, s₁, ... as follows: at step sᵢ, if L_{i-1} is lit, then switch Lᵢ
from on to off or vice versa, otherwise do nothing. Show that:
(a) There is a positive integer M(n) such that after M(n) steps all the lamps are
on again;
(b) If n = 2ᵏ, then we can take M(n) = n² - 1.
(c) If n = 2ᵏ + 1, then we can take M(n) = n² - n + 1.
-/
namespace Imo1993P6
open scoped Fin.NatCast
/-- The state of the system: the on/off states of the lamps (`true` = on), together
with the position of the lamp that may be switched at the next step. Positions are
taken modulo `n`, i.e. in `Fin n`. -/
abbrev State (n : ℕ) := (Fin n → Bool) × Fin n
/-- One step of the process, performed at the current position `s.2`: if lamp
`s.2 - 1` is on then lamp `s.2` is switched, otherwise nothing happens to the lamps;
in any case the position advances by one (modulo `n`). -/
def step {n : ℕ} [NeZero n] (s : State n) : State n :=
(Function.update s.1 s.2 (if s.1 (s.2 - 1) then !s.1 s.2 else s.1 s.2), s.2 + 1)
/-- The initial state: all lamps on, and the next step happens at lamp `0`. -/
abbrev initial (n : ℕ) [NeZero n] : State n := (fun _ => true, 0)
/-- The lamp states after `t` steps of the process. -/
abbrev lampsAfter (n : ℕ) [NeZero n] (t : ℕ) : Fin n → Bool :=
(step^[t] (initial n)).1
theorem imo1993_p6_a (n : ℕ) [NeZero n] (hn : 1 < n) :
∃ M : ℕ, 0 < M ∧ ∀ i : Fin n, lampsAfter n M i = true := sorry
theorem imo1993_p6_b (n k : ℕ) [NeZero n] (hn : n = 2 ^ k) (hk : 0 < k) :
∀ i : Fin n, lampsAfter n (n ^ 2 - 1) i = true := sorry
theorem imo1993_p6_c (n k : ℕ) [NeZero n] (hn : n = 2 ^ k + 1) (hk : 0 < k) :
∀ i : Fin n, lampsAfter n (n ^ 2 - n + 1) i = true := sorry
end Imo1993P6
This problem has a complete formalized solution.