English
If f ignores the right input and yields a constant first component, then mapAccumr₂ f xs ys s reduces to map₂ with a suitable right-argument mapping.
Русский
Если f игнорирует правый вход и даёт константную первую компоненту, то mapAccumr₂ f xs ys s сводится к map₂ с соответствующим отображением второго аргумента.
LaTeX
$$$$ \operatorname{mapAccumr_2} f xs ys s = \operatorname{map}_2 f' xs ys \quad \text{when } f a b s = f'(b, s) $$$$
Lean4
/-- If `f` returns the same output and next state for every value of it's second argument, then
`ys : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
-/
@[simp]
theorem mapAccumr₂_unused_input_right (f : α → β → σ → σ × γ) (f' : α → σ → σ × γ) (h : ∀ a b s, f a b s = f' a s) :
mapAccumr₂ f xs ys s = mapAccumr f' xs 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]
