English
For f : β → Option(α × β) and b : β, destruct(corec f b) equals omap(corec f)(f b); i.e., the initial step is determined by f b via omap.
Русский
Для f : β → Option(α × β) и b : β, destruct(corec f b) равно omap(corec f)(f b); т.е. начальный шаг задаётся через f b через omap.
LaTeX
$$$\\text{destruct}(\\text{corec}(f)(b)) = \\mathrm{omap}(\\text{corec}(f))(f(b)).$$$
Lean4
@[simp]
theorem corec_eq (f : β → Option (α × β)) (b : β) : destruct (corec f b) = omap (corec f) (f b) :=
by
dsimp [corec, destruct, get]
rw [show Stream'.corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1 from rfl]
dsimp [Corec.f]
rcases h : f b with - | s; · rfl
obtain ⟨a, b'⟩ := s; dsimp [Corec.f]
apply congr_arg fun b' => some (a, b')
apply Subtype.eq
dsimp [corec, tail]
rw [Stream'.corec'_eq, Stream'.tail_cons]
dsimp [Corec.f]; rw [h]
