English
Bisimulation principle for Cofix: if r is a relation on Cofix F and if repeatedly r maps via cofactors, then x = y whenever r x y holds under Liftr constraints.
Русский
Принцип бисимулации для Cofix: если r — отношение на Cofix F и если через dest и Liftr сохраняются свойства, то при r x y выполняется x = y.
LaTeX
$$$$\forall {F : Type u \to Type u} [q : QPF F] (r : Cofix F \to Cofix F \to Prop),\n (\forall x y, r x y \to Eq (q.map (Quot.mk r) x.dest) (q.map (Quot.mk r) y.dest)) \rightarrow \forall (x y : Cofix F), r x y \rightarrow x = y.$$$$
Lean4
theorem bisim (r : Cofix F → Cofix F → Prop) (h : ∀ x y, r x y → Liftr r (Cofix.dest x) (Cofix.dest y)) :
∀ x y, r x y → x = y := by
apply Cofix.bisim_rel
intro x y rxy
rcases (liftr_iff r _ _).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
rw [dxeq, dyeq, ← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
congr 2 with i
apply Quot.sound
apply h'
