mapAccumr_bisim_tail — Mathlib

English

Tail-bisimilarity principle: if a relation holds for the tail case, the tails of mapAccumr coincide.

Русский

Утверждение о бисимуляции хвоста: для хвостового случая отношение сохраняется, хвостовые значения совпадают.

LaTeX

$$$\forall xs, (\exists R, R s_1 s_2 \land \forall a, R s q \to R (f a s).1 (f' a q).1 \land (f a s).2 = (f' a q).2) \Rightarrow \dots$$$

Lean4

theorem mapAccumr_bisim_tail {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂}
    (h : ∃ R : σ₁ → σ₂ → Prop, R s₁ s₂ ∧ ∀ {s q} a, R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) :
    (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd :=
  by
  rcases h with ⟨R, h₀, hR⟩
  exact (mapAccumr_bisim R h₀ hR).2

Похожие утверждения