English
A bisimulation principle using LiftR to relate destination structures and deduce equality of coinductive trees.
Русский
Принцип бисимуляции с использованием LiftR для связиDest структур и вывода равенства коиндективных деревьев.
LaTeX
$$$\\forall r x y, r x y \\to q.map (TypeVec.appendFun TypeVec.id (Quot.mk r)) (Cofix.dest x) = q.map (TypeVec.appendFun TypeVec.id (Quot.mk r)) (Cofix.dest y) \\Rightarrow \\forall x y, r x y \\to x=y$$$
Lean4
/-- Bisimulation principle using `LiftR` to match and relate children of two trees. -/
theorem bisim {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop)
(h : ∀ x y, r x y → LiftR (RelLast α 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 (fun a b => RelLast α r b) (dest x) (dest y)).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
rw [dxeq, dyeq, ← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
rw [← split_dropFun_lastFun f₀, ← split_dropFun_lastFun f₁]
rw [appendFun_comp_splitFun, appendFun_comp_splitFun]
rw [id_comp, id_comp]
congr 2 with (i j); rcases i with - | i
· apply Quot.sound
apply h' _ j
· change f₀ _ j = f₁ _ j
apply h' _ j
