English
For any σ, the function f: α → σ → σ × β, the accumulator s, and the list as, we have a canonical rewrite: mapAccumr f as s = foldr (λ a s, let r := f a s.1 in (r.1, r.2 :: s.2)) (s, []) as.
Русский
Для любой σ и функции f: α → σ → σ × β, выполняемая над списком as с аккумулятором s, выполняется равенство: mapAccumr f as s = foldr ... as.
LaTeX
$$$\\mathrm{mapAccumr}\\ f\\ as\\ s = \\mathrm{foldr}\\ (\\lambda a\, s',\\ \\text{let } r := f\\ a\\ s'.1 \\text{ in } (r.1, r.2 :: s'.2))\\ (s, [])\\ as.$$$
Lean4
theorem mapAccumr_eq_foldr {σ : Type*} (f : α → σ → σ × β) :
∀ (as : List α) (s : σ),
mapAccumr f as s =
List.foldr
(fun a s =>
let r := f a s.1
(r.1, r.2 :: s.2))
(s, []) as
| [], _ => rfl
| a :: as, s => by simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]
