English
Bisimulation principle using map and Quot.mk to match and relate children of two trees; proves equality under a relation.
Русский
Принцип бисимуляции с использованием map и Quot.mk для сопоставления и сопоставления потомков двух деревьев; доказывает равенство при отношении.
LaTeX
$$$\\forall \\alpha, r:\\, Cofix F \\alpha \\to Cofix F \\alpha \\to Prop,\\; (\\forall x y, r x y \\to \\operatorname{Eq}\\left( q.map (\\text{appendFun id (Quot.mk r)}) (Cofix.dest x) \\right) \\left( q.map (\\text{appendFun id (Quot.mk r)}) (Cofix.dest y) \\right) ) \\Rightarrow \\forall x y, r x y \\to x = y$$$
Lean4
/-- Bisimulation principle using `map` and `Quot.mk` to match and relate children of two trees. -/
theorem bisim_rel {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop)
(h : ∀ x y, r x y → appendFun id (Quot.mk r) <$$> Cofix.dest x = appendFun id (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
cases r'xy with
| inl h => rw [h]
| inr 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 [appendFun_comp_id]
rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)), @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
rw [h _ _ r'xy]
right; exact rxy
