English
A strengthened variant of bisimulation, parameterized by a predicate Q on an index domain and a construction u,v : α → M P, establishing equivalence provided a certain structured witness exists for every x with Q x.
Русский
Усиленная версия бисимуляции, параметризованная предикатом Q на множество индексов и отображениями u,v : α → M P, устанавливающая эквивалентность при наличии соответствующего структурированного свидетеля для каждого x с Q x.
LaTeX
$$$\forall Q,u,v:\, (\forall x, Q x → ∃ a f f', M.dest (u x) = ⟨a,f⟩ ∧ M.dest (v x) = ⟨a,f'⟩ ∧ ∀ i, ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') → ∀ x, Q x → u x = v x$$$
Lean4
theorem bisim' {α : Type*} (Q : α → Prop) (u v : α → M P)
(h :
∀ x,
Q x → ∃ a f f', M.dest (u x) = ⟨a, f⟩ ∧ M.dest (v x) = ⟨a, f'⟩ ∧ ∀ i, ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') :
∀ x, Q x → u x = v x := fun x Qx =>
let R := fun w z : M P => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
@M.bisim P R
(fun _ _ ⟨x', Qx', xeq, yeq⟩ =>
let ⟨a, f, f', ux'eq, vx'eq, h'⟩ := h x' Qx'
⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩)
_ _
⟨x, Qx, rfl, rfl⟩
-- for the record, show M_bisim follows from _bisim'
