English
When combining two different accumulator-generating operations on two vectors, applying mapAccumr to the first with the second’s result is equivalent to a single mapAccumr with a jointly defined update that threads through both vectors.
Русский
При объединении двух различных аккумуляторных операций на двух векторах применение mapAccumr к первому с результатом второго эквивалентно одному вызову mapAccumr с общим обновлением, учитывающим оба вектора.
LaTeX
$$$\text{mapAccumr } f_1 (\text{mapAccumr₂ } f_2 xs ys s_2).snd s_1 = \text{let } m := \text{mapAccumr₂ } (\lambda x y s. (\text{fst}(f_1(s.fst,x)), \text{fst}(f_2(y,s.snd)))) xs ys (s_1,s_2) \text{ in } (m.fst.fst, m.snd)$$$
Lean4
@[simp]
theorem mapAccumr₂_mapAccumr_left (f₁ : γ → β → σ₁ → σ₁ × ζ) (f₂ : α → σ₂ → σ₂ × γ) :
(mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).snd ys s₁) =
let m :=
(mapAccumr₂
(fun x y s =>
let r₂ := f₂ x s.snd
let r₁ := f₁ r₂.snd y s.fst
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂))
(m.fst.fst, m.snd) :=
by induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
