English
A two-parameter coinduction principle: if for all s, a bisimulation-like condition holds relating f s and g s, then f s = g s.
Русский
Двухпараметричный принцип когоиндукции: если для каждого s выполняется бисимиляционное условие, связывающее f s и g s, то f s = g s.
LaTeX
$$$\\text{coinduction2} (s)(f,g)\\;\\; (H) :\\; \\forall s, BisimO (\\lambda s1 s2. \\exists s: Seq\\ α, s1 = f s ∧ s2 = g s) (\\text{destruct}(f\\ s)) (\\text{destruct}(g\\ s)) \\rightarrow f s = g s$$$
Lean4
theorem coinduction2 (s) (f g : Seq α → Seq β)
(H : ∀ s, BisimO (fun s1 s2 : Seq β => ∃ s : Seq α, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))) :
f s = g s := by
refine eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩
intro s1 s2 h; rcases h with ⟨s, h1, h2⟩
rw [h1, h2]; apply H
