English
Let xs be a vector of elements of type α and ys a vector of elements of type β, both of length n. Consider two stateful step functions f1 and f2, sending a pair of elements and a current state to a new state plus an output: f1 : α → β → σ1 → σ1 × γ and f2 : α → β → σ2 → σ2 × γ, with initial states s1 ∈ σ1 and s2 ∈ σ2. Suppose there exists a relation R ⊆ σ1 × σ2 such that R(s1, s2) holds, and for all s, q, a, b, if R(s, q) holds then the first components after applying the steps preserve the relation, i.e., R((f1 a b s).1, (f2 a b q).1) holds, and the outputs agree, i.e., (f1 a b s).2 = (f2 a b q).2. Then the final second components produced by mapAccumr₂ f1 xs ys starting from s1 and by mapAccumr₂ f2 xs ys starting from s2 are equal.
Русский
Пусть xs — вектор элементов α, ys — вектор элементов β длины n. Пусть f1 и f2: α × β × σ → σ × γ — пополняющие переходы с выходом, с начальными состояниями s1 ∈ σ1 и s2 ∈ σ2. Пусть существует отношение R ⊆ σ1 × σ2 такое, что R(s1, s2). Для любых s, q, a, b из соответствующих типов верно: если R(s, q), то R((f1 a b s).1, (f2 a b q).1) и (f1 a b s).2 = (f2 a b q).2. Тогда финальные значения выходов второго компонента у mapAccumr₂ f1 xs ys и у mapAccumr₂ f2 xs ys равны.
LaTeX
$$$\exists R : σ_1 \to σ_2 \to \mathrm{Prop},\; R\, s_1\, s_2 \land \forall {s\, q} \; a\, b,\; R\, s\, q \rightarrow R\big((f_1\ a\ b\ s).1\big)\big((f_2\ a\ b\ q).1\big) \land (f_1\ a\ b\ s).2 = (f_2\ a\ b\ q).2 \Rightarrow (\mathrm{mapAccumr_2}\ f_1\ xs\ ys\ s_1).2 = (\mathrm{mapAccumr_2}\ f_2\ xs\ ys\ s_2).2$$$
Lean4
theorem mapAccumr₂_bisim_tail {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁}
{s₂ : σ₂}
(h :
∃ R : σ₁ → σ₂ → Prop, R s₁ s₂ ∧ ∀ {s q} a b, R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) :
(mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2 :=
by
rcases h with ⟨R, h₀, hR⟩
exact (mapAccumr₂_bisim R h₀ hR).2
