English
Final bisimulation result for mapAccumr across two vectors.
Русский
Итог бисимуляции для mapAccumr по двум векторам.
LaTeX
$$$\forall xs,ys,\; \text{bisimicial conclusion for mapAccumr}$$$
Lean4
theorem mapAccumr₂_bisim {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂}
(R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂)
(hR : ∀ {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) :
R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2 :=
by
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
next => exact ⟨h₀, rfl⟩
next xs ys x y ih =>
rcases (hR x y h₀) with ⟨hR, _⟩
simp only [mapAccumr₂_snoc, ih hR, true_and]
congr 1
