English
For any α, β, σ, φ and f : α → β → σ → σ × φ, the relation mapAccumr₂ f as bs s equals folding over as.zip bs with a corresponding updater: mapAccumr₂ f as bs s = foldr (λ ab s, let r := f ab.1 ab.2 s.1 in (r.1, r.2 :: s.2)) (s, []) (as.zip bs).
Русский
Для f: α → β → σ → σ × φ существует эквивалентность между mapAccumr₂ и foldr через пару ab из списка as и bs.
LaTeX
$$$\\mathrm{mapAccumr_2}\\ f\\ as\\ bs\\ s = \\mathrm{foldr}\\ (\\lambda ab\\, s',\\ let\\ r := f\\ ab.1\\ ab.2\\ s'.1\\ in\\ (r.1, r.2 :: s'.2))\\ (s, [])\\ (as.zip\\ bs).$$$
Lean4
theorem mapAccumr₂_eq_foldr {σ φ : Type*} (f : α → β → σ → σ × φ) :
∀ (as : List α) (bs : List β) (s : σ),
mapAccumr₂ f as bs s =
foldr
(fun ab s =>
let r := f ab.1 ab.2 s.1
(r.1, r.2 :: s.2))
(s, []) (as.zip bs)
| [], [], _ => rfl
| _ :: _, [], _ => rfl
| [], _ :: _, _ => rfl
| a :: as, b :: bs, s => by
simp only [mapAccumr₂, mapAccumr₂_eq_foldr f as]
rfl
