English
If g : α → P α and f : α → M P satisfies M.dest (f x) = P.map f (g x) for all x, then f is the unique corecursive solution, i.e., f = M.corec g.
Русский
Если задано отображение g : α → P α и функция f : α → M P, удовлетворяющая условию dest(f x) = map f (g x) для всех x, то f является единственным решением корекурсии: f = M.corec g.
LaTeX
$$$\text{hyp}: \forall x, M.dest (f x) = P.map f (g x) \Rightarrow f = M.corec g$$$
Lean4
theorem corec_unique (g : α → P α) (f : α → M P) (hyp : ∀ x, M.dest (f x) = P.map f (g x)) : f = M.corec g :=
by
ext x
apply bisim' (fun _ => True) _ _ _ _ trivial
clear x
intro x _
rcases gxeq : g x with ⟨a, f'⟩
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
refine ⟨_, _, _, h₀, h₁, ?_⟩
intro i
exact ⟨f' i, trivial, rfl, rfl⟩
