English
A bisimulation lemma for multivariate functor M describes how dest interacts with a split into components, ensuring a correspondence between the left and right branches.
Русский
Лемма би-симуляции для мультфункторного M описывает взаимодействие dest с разбиением на компоненты, обеспечивая соответствие левой и правой ветвям.
LaTeX
$$$\\forall {n} {P} {α} {a_1} {f_1} {a'} {f'} {f_1'}\\, (e_1: M.dest P ⟨a_1,f_1⟩ = ⟨a', splitFun f' f_1'⟩) \\,\\Rightarrow \\, \\exists g_1'\\ ,\\ e_1'\\,; \\; f' = M.pathDestLeft P e_1' f_1 \\land f_1' = \\lambda x. \\langle g_1'(x), M.pathDestRight P e_1' f_1 x \\rangle$$$
Lean4
theorem bisim_lemma {α : TypeVec n} {a₁ : (mp P).A} {f₁ : (mp P).B a₁ ⟹ α} {a' : P.A} {f' : (P.B a').drop ⟹ α}
{f₁' : (P.B a').last → M P α} (e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩) :
∃ (g₁' : _) (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
f' = M.pathDestLeft P e₁' f₁ ∧ f₁' = fun x : (last P).B a' => ⟨g₁' x, M.pathDestRight P e₁' f₁ x⟩ :=
by
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁
let he₁' := PFunctor.M.dest a₁
rcases e₁' : he₁' with ⟨a₁', g₁'⟩
rw [M.dest_eq_dest' _ e₁'] at e₁
cases e₁; exact ⟨_, e₁', splitFun_inj ef⟩
