English
Equivalent restatement: under a constant first projection, mapAccumr₂ f xs ys s coincides with mapAccumr g ys s for a suitable g, i.e., the left input is ignored.
Русский
Эквивалентное переизложение: при фиксированном первом компоненте, mapAccumr₂ f xs ys s совпадает с mapAccumr g ys s, то есть первый вход проигнорирован.
LaTeX
$$$$ mapAccumr_2 f\; xs\; ys\; s = mapAccumr g\; ys\; s \quad \text{where } g(b, s) = (f\,\cdot\, b\, s).snd $$$$
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 s, (f a s).snd = f' a) :
(mapAccumr f xs s).snd = (map f' xs) :=
by
rw [mapAccumr_eq_map (fun _ => true) rfl (fun _ _ _ => rfl) (fun a s s' _ _ => by rw [h, h])]
simp_all
