English
Let l be a list, n a natural number, and m a natural index with m < length(l). Then the m-th element of l.rotate n equals the element of l at position (m + n) mod length(l).
Русский
Пусть l — список, n — естественное число, а m — индекс с условием m < длина(l). Тогда m-й элемент l.rotate n равен элементу l на позиции (m + n) mod длина(l).
LaTeX
$$$\\forall l\\in\\mathrm{List}\\alpha,\\forall n\\in\\mathbb{N},\\forall m\\in\\mathbb{N},\\ (m < |l|) \\Rightarrow (l.rotate n)[m] = l[(m + n) \\% |l|]$$$
Lean4
theorem getElem?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) : (l.rotate n)[m]? = l[(m + n) % l.length]? :=
by
rw [rotate_eq_drop_append_take_mod]
rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm
· rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]
rw [length_drop, Nat.lt_sub_iff_add_lt] at hm
rw [mod_eq_of_lt hm, Nat.add_comm]
· have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
· congr 1
rw [length_drop] at hm
have hm' := Nat.sub_le_iff_le_add'.1 hm
have : n % length l + m - length l < length l :=
by
rw [Nat.sub_lt_iff_lt_add hm']
exact Nat.add_lt_add hlt hml
conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
cutsat
· rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]
