English
Let S be a subset of the state type σ and let s0 ∈ S. Suppose f: α → σ → σ × β is such that (i) for every a and s ∈ S, the new state (f a s).fst stays in S, and (ii) for all a ∈ α and s, s' ∈ S we have (f a s).snd = (f a s').snd. Then the second component produced by mapAccumr f on xs starting from s0 is exactly the plain map of xs using the second component of f with the initial state s0; i.e. (mapAccumr f xs s0).snd = map (λ a, (f a s0).snd) xs.
Русский
Пусть S ⊆ σ и s0 ∈ S. Пусть f: α → σ → σ × β удовлетворяет: (i) для любого a и s ∈ S новое состояние (f a s).fst принадлежит S; (ii) для любых a, s, s' ∈ S выполнено (f a s).snd = (f a s').snd. Тогда вторая компонента результата mapAccumr f над xs с начальным состоянием s0 совпадает с обычным отображением xs по функции a ↦ (f a s0).snd; то есть (mapAccumr f xs s0).snd = map (λ a, (f a s0).snd) xs.
LaTeX
$$$$ (mapAccumr f xs\, s_0).snd \;=\; \\operatorname{map}\\bigl(a \\mapsto \\operatorname{snd}(f(a, s_0))\\bigr) xs $$$$
Lean4
/-- If there is a set of states that is closed under `f`, and such that `f` produces that same output
for all states in this set, then the state is not actually needed.
Hence, then we can rewrite `mapAccumr` into just `map`.
-/
theorem mapAccumr_eq_map {f : α → σ → σ × β} {s₀ : σ} (S : Set σ) (h₀ : s₀ ∈ S) (closure : ∀ a s, s ∈ S → (f a s).1 ∈ S)
(out : ∀ a s s', s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) : (mapAccumr f xs s₀).snd = map (f · s₀ |>.snd) xs :=
by
rw [Vector.map_eq_mapAccumr]
apply mapAccumr_bisim_tail
use fun s _ => s ∈ S, h₀
exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
