English
If the function f does not depend on the right input (the second argument) in its outputs, 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 `f` returns the same output and next state for every value of it's first argument, then
`xs : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
-/
@[simp]
theorem mapAccumr₂_unused_input_left (f : α → β → σ → σ × γ) (f' : β → σ → σ × γ) (h : ∀ a b s, f a b s = f' b s) :
mapAccumr₂ f xs ys s = mapAccumr f' ys s := by
induction xs, ys using Vector.revInductionOn₂ generalizing s with
| nil => rfl
| snoc xs ys x y ih => simp [h x y s, ih]
