English
If the accumulation function f does not depend on the left input (the first argument) in its outputs, then mapAccumr₂ f xs ys s = map₂ f' xs ys where f' ignores the left argument.
Русский
Если функция f не зависит от левого входа в своих выходах, то mapAccumr₂ f xs ys s равняется map₂ f' xs ys, где f' игнорирует левый аргумент.
LaTeX
$$$$ \operatorname{mapAccumr_2} f\; xs\; ys\; s = \operatorname{map}_2 f'\; xs\; ys \quad \text{whenever } f(a, s) = f'(a, s) $$$$
Lean4
/-- If `f` takes a pair of states, but always returns the same value for both elements of the
pair, then we can simplify to just a single element of state.
-/
@[simp]
theorem mapAccumr_redundant_pair (f : α → (σ × σ) → (σ × σ) × β)
(h : ∀ x s, (f x (s, s)).fst.fst = (f x (s, s)).fst.snd) :
(mapAccumr f xs (s, s)).snd = (mapAccumr (fun x (s : σ) => (f x (s, s) |>.fst.fst, f x (s, s) |>.snd)) xs s).snd :=
mapAccumr_bisim_tail <| by
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
simp_all
