English
Let l be a list, f a function, and b a base value. For every i with i less than the length of scanr f b l, the i-th element of scanr f b l equals foldr f b (l.drop i).
Русский
Пусть l — список, f — функция, b — базовое значение. Для каждого i, такого что i меньше длины scanr f b l, i-й элемент scanr f b l равен foldr f b (l.drop i).
LaTeX
$$$ \\forall (l : List \\alpha) (f : \\alpha \\rightarrow \\beta \\rightarrow \\beta) (b : \\beta) (i : \\mathbb{N}), i < (scanr f b l).length \\Rightarrow (scanr f b l)[i] = foldr f b (l.drop i). $$$
Lean4
theorem getElem_scanr {i : ℕ} (h : i < (scanr f b l).length) : (scanr f b l)[i] = foldr f b (l.drop i) := by
induction l generalizing i with
| nil => simp
| cons head tail ih =>
obtain rfl | h' := eq_or_ne i 0
· simp
· obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h'
simp [@ih m (by simp_all [length_scanr])]
