English
Enhancement of bisimulation: if R relates x,y and h shows their destinations are equivalent under the quotient, then x=y, by transporting through the quotient structure and using the equivalence relation recursively.
Русский
Усложнение бисимиляции: если R связывает x,y и h показывает, что их разрушения эквивалентны по фактору, то x=y, через транспортировку по фактору и рекурсивное использование эквивалентности.
LaTeX
$$$\forall {n} {P} (R : P.M α → P.M α → Prop),\ (h : ∀ (x y), R x y → (id ::: Quot.mk R) <$$> M.dest _ x = (id ::: Quot.mk R) <$$> M.dest _ y) (x y) (r : R x y) : x = y$$$
Lean4
theorem bisim' {α : TypeVec n} (R : P.M α → P.M α → Prop)
(h : ∀ x y, R x y → (id ::: Quot.mk R) <$$> M.dest _ x = (id ::: Quot.mk R) <$$> M.dest _ y) (x y) (r : R x y) :
x = y := by
have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_
· solve_by_elim [Relation.EqvGen.rel]
· apply Relation.EqvGen.is_equivalence
· clear r x y
introv Hr
have : ∀ x y, R x y → Relation.EqvGen R x y := @Relation.EqvGen.rel _ R
induction Hr
· rw [← Quot.factor_mk_eq R (Relation.EqvGen R) this]
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
all_goals simp_all
