English
Applying mapAccumr to a vector with update f₂ and then mapping with f₁ on the resulting second component is equivalent to a single mapAccumr with a composed update that first applies f₂ and then f₁ on the respective parts.
Русский
Применение mapAccumr к вектору с обновлением f₂, затем отображение с помощью f₁ на полученном втором компоненте эквивалентно одному вызову mapAccumr с составленным обновлением, которое сначала применяет f₂, затем f₁ к соответствующим частям.
LaTeX
$$$\\text{mapAccumr } f_1\\ (\\text{mapAccumr } f_2\\ x s_2).snd\\ s_1 = \\text{let } m := \\text{mapAccumr} \\Big( \\lambda x\\ s,\\; (\\text{fst},\\text{snd}) \\Big)\\ x (s_1,s_2)\\ in (m.fst.fst, m.snd)$$$
Lean4
@[simp]
theorem mapAccumr_mapAccumr :
mapAccumr f₁ (mapAccumr f₂ xs s₂).snd s₁ =
let m :=
(mapAccumr
(fun x s =>
let r₂ := f₂ x s.snd
let r₁ := f₁ r₂.snd s.fst
((r₁.fst, r₂.fst), r₁.snd))
xs (s₁, s₂))
(m.fst.fst, m.snd) :=
by induction xs using Vector.revInductionOn generalizing s₁ s₂ <;> simp_all
