English
Let f: α → β → σ → σ × γ be given and S, h0, closure, out as in the previous invariant setting. Then the outputs of mapAccumr₂ are exactly the same as those produced by map₂ with the second component of f: (mapAccumr₂ f xs ys s0).snd = map₂ (f · · s0 |>.snd) xs ys.
Русский
Пусть дана функция f: α → β → σ → σ × γ и множества S, s0 ∈ S, а также условия замыкания и совместимости выходов, как в предыдущем случае инвариантности. Тогда выход второй компоненты mapAccumr₂ совпадает с map₂, где второй компонент функции f(аб, s0): (mapAccumr₂ f xs ys s0).snd = map₂ (f · · s0 |>.snd) xs ys.
LaTeX
$$$$ (\\operatorname{mapAccumr_2} f\\; xs\\; ys\\; s_0).snd \\\\;=\; \\operatorname{map}_2\\bigl(\\lambda x\\, y, (f x y s_0).snd\\bigr) xs ys $$$$
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 b s, s ∈ S → (f a b s).1 ∈ S) (out : ∀ a b s s', s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) :
(mapAccumr₂ f xs ys s₀).snd = map₂ (f · · s₀ |>.snd) xs ys :=
by
rw [Vector.map₂_eq_mapAccumr₂]
apply mapAccumr₂_bisim_tail
use fun s _ => s ∈ S, h₀
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩
