English
If R relates two M-objects and h shows that dest respects equivalence under R, then R-compatibility propagates to equality: two related trees are equal whenever their immediate roots align and their subtrees are related recursively.
Русский
Если отношение R связывает две структуры M и для которых h демонстрирует совместимость разрушения с эквивалентностью, тогда пара связанных деревьев равна друг другу при условии согласования корней и рекурсивной связи подпутей.
LaTeX
$$$\forall {n} {P} {R} \ (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 → ∃ a f f₁ f₂, M.dest P x = ⟨a, splitFun f f₁⟩ ∧ M.dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ i, R (f₁ i) (f₂ i))
(x y) (r : R x y) : x = y := by
obtain ⟨a₁, f₁⟩ := x
obtain ⟨a₂, f₂⟩ := y
dsimp [mp] at *
have : a₁ = a₂ :=
by
refine PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
rw [e₁', e₂']
exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
subst this
congr with (i p)
induction p with
( obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
cases h'.symm.trans e₁'
cases h'.symm.trans e₂')
| root x a f h' i c => exact congr_fun (congr_fun e₃ i) c
| child x a f h' i c p IH => exact IH _ _ (h'' _)
