English
If the accumulation function f does not depend on the right argument in its output and next state, i.e., f a b s = f a b' s for all b,b', then mapAccumr₂ f xs ys s = mapAccumr f xs s.
Русский
Если функция накопления f не зависит от второго аргумента в выходе и следующем состоянии, то mapAccumr₂ f xs ys s равняется mapAccumr f xs s.
LaTeX
$$$$ \operatorname{mapAccumr_2} f\; xs\; ys\; s \\= \operatorname{mapAccumr} f'\; xs\; s \quad \text{where } f(a,b,s) = f'(a,s)$$$$
Lean4
/-- If an accumulation function `f`, produces the same output bits regardless of accumulation state,
then the state is redundant and can be optimized out.
-/
@[simp]
theorem mapAccumr₂_eq_map₂_of_unused_state (f : α → β → σ → σ × γ) (f' : α → β → γ) (s : σ)
(h : ∀ a b s, (f a b s).snd = f' a b) : (mapAccumr₂ f xs ys s).snd = (map₂ (fun x y => (f x y s).snd) xs ys) :=
mapAccumr₂_eq_map₂ (fun _ => true) rfl (fun _ _ _ _ => rfl) (fun a b s s' _ _ => by rw [h, h])
