English
A close recurrence description for the (i+1)-th element of scanl, interpreted with option-bounded retrieval.
Русский
Пограничное описание следующего элемента scanl через i-й элемент и i-й элемент l.
LaTeX
$$$$\forall i:\mathbb{N},\ (\operatorname{scanl} f b l)_{i+1} = f\big((\operatorname{scanl} f b l)_i\big)\big(l_i\big) \quad \text{(при соответствующих ограничениях)}.$$$$
Lean4
theorem getElem_succ_scanl {i : ℕ} (h : i + 1 < (scanl f b l).length) :
(scanl f b l)[i + 1] =
f ((scanl f b l)[i]'(Nat.lt_of_succ_lt h)) (l[i]'(Nat.lt_of_succ_lt_succ (h.trans_eq (length_scanl b l)))) :=
by
induction i generalizing b l with
| zero =>
cases l
· simp only [scanl, length, lt_self_iff_false] at h
· simp
| succ i hi =>
cases l
· simp only [scanl, length] at h
exact absurd h (by cutsat)
· simp_rw [scanl_cons]
rw [getElem_append_right]
· simp only [length, Nat.zero_add 1, succ_add_sub_one, hi]; rfl
· simp only [length_singleton]; cutsat
