English
A more constructive bisimilarity principle for Cofix: if Q x holds and there exists a decomposition of u and v with corresponding dest and a compatibility condition, then u x = v x.
Русский
Более конструктивный принцип бисимиляции для Cofix: если Q x выполняется и есть разложение для u и v с соответствующими dest и условием совместимости, то u x = v x.
LaTeX
$$$$\forall {F : Type u \to Type u} [q : QPF F] {\alpha : Type u} (Q : \alpha \to Prop) (u v : \alpha \to QPF.Cofix F), (h : \forall x, Q x \to \exists a f f',\ Cofix.dest (u x) = abs ⟨a, f⟩ ∧ Cofix.dest (v x) = abs ⟨a, f'⟩ ∧ \forall i, \exists x', Q x' ∧ f i = u x' ∧ f' i = v x') : \forall x, Q x \rightarrow u x = v x.$$$$
Lean4
theorem bisim' {α : Type*} (Q : α → Prop) (u v : α → Cofix F)
(h :
∀ x,
Q x →
∃ a f f',
Cofix.dest (u x) = abs ⟨a, f⟩ ∧
Cofix.dest (v x) = abs ⟨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 : 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', ux'eq, vx'eq, h'⟩
rw [liftr_iff]
exact ⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩)
_ _ ⟨x, Qx, rfl, rfl⟩
