English
A generic bisimulation principle for mapAccumr: if a relation holds for the initial states and is preserved under one-step application, then the final states are related and outputs match.
Русский
Обобщённое правило бисимуляции для mapAccumr: если отношение сохраняется после одного шага, то конечные состояния связаны и выводы совпадают.
LaTeX
$$$\forall xs,ys,\, R\; \Rightarrow\; ...$$$
Lean4
theorem mapAccumr_bisim {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁ → σ₂ → Prop)
(h₀ : R s₁ s₂) (hR : ∀ {s q} a, R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) :
R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd :=
by
induction xs using Vector.revInductionOn generalizing s₁ s₂
next => exact ⟨h₀, rfl⟩
next xs x ih =>
rcases (hR x h₀) with ⟨hR, _⟩
simp only [mapAccumr_snoc, ih hR, true_and]
congr 1
