English
Bisimulation principle with a richer relation structure using lifted MvQPF components to relate destinations and derive equality.
Русский
Бисимуляционный принцип с более сложной структурой отношения, используя поднятые компоненты MvQPF для связи dest и вывода равенства.
LaTeX
$$$\\forall Q u v,\\; (\\forall x, Q x \\to \\exists a f' f_0 f_1, \\Cofix.dest (u x) = q.abs \\langle a, q.P.appendContents f' f_0\\rangle \\land \\Cofix.dest (v x) = q.abs \\langle a, q.P.appendContents f' f_1\\rangle \\land \\forall i, \\exists x', Q x' \\\\land f_0 i = u x' \\\\land f_1 i = v x') \\Rightarrow \\forall x, Q x \\to u x = v x$$$
Lean4
/-- Bisimulation principle the values `⟨a,f⟩` of the polynomial functor representing
`Cofix F α` as well as an invariant `Q : β → Prop` and a state `β` generating the
left-hand side and right-hand side of the equality through functions `u v : β → Cofix F α` -/
theorem bisim' {α : TypeVec n} {β : Type*} (Q : β → Prop) (u v : β → Cofix F α)
(h :
∀ x,
Q x →
∃ a f' f₀ f₁,
Cofix.dest (u x) = q.abs ⟨a, q.P.appendContents f' f₀⟩ ∧
Cofix.dest (v x) = q.abs ⟨a, q.P.appendContents f' 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 : Cofix F α => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
Cofix.bisim R
(fun x y ⟨x', Qx', xeq, yeq⟩ =>
by
rcases h x' Qx' with ⟨a, f', f₀, f₁, ux'eq, vx'eq, h'⟩
rw [liftR_iff]
refine ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, ?_⟩
intro i; cases i
· apply h'
· intro j
apply Eq.refl)
_ _ ⟨x, Qx, rfl, rfl⟩
