English
Let F be a type constructor with a QPF structure. If r is a relation on Cofix F such that r x y implies equality of mapped destinations under the quotient map, then r x y implies x = y. In other words, a bisimulation relation is antisymmetric with respect to the coinductive structure.
Русский
Пусть F — это порождающая конструкция, обладающая структурой QPF. Если r — отношение на Cofix F так, что r x y влечёт равенство отображений dest через Quot.mk r, то r x y влечёт x = y.
LaTeX
$$$\\forall x,y:\\mathrm{Cofix}\,F,\\ r\\,x\\,y \\Rightarrow x = y$$$
Lean4
theorem bisim_rel (r : Cofix F → Cofix F → Prop)
(h : ∀ x y, r x y → Quot.mk r <$> Cofix.dest x = Quot.mk r <$> Cofix.dest y) : ∀ x y, r x y → x = y :=
by
let r' (x y) := x = y ∨ r x y
intro x y rxy
apply Cofix.bisim_aux r'
· intro x
left
rfl
· intro x y r'xy
rcases r'xy with r'xy | r'xy
· rw [r'xy]
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
rw [← Quot.factor_mk_eq _ _ this]
dsimp [r']
rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]
rw [h _ _ r'xy]
right; exact rxy
