English
For any f: β → α ⊕ β and b: β, destruct (corec f b) = rmap (corec f) (f b).
Русский
Для любого f: β → α ⊕ β и b: β, выполняется равенство destruct (corec f b) = rmap (corec f) (f b).
LaTeX
$$$\mathrm{destruct}(\mathrm{corec}(f)(b)) = \mathrm{rmap}(\mathrm{corec}(f))(f(b)).$$$
Lean4
@[simp]
theorem corec_eq (f : β → α ⊕ β) (b : β) : destruct (corec f b) = rmap (corec f) (f b) :=
by
dsimp [corec, destruct]
rw [show Stream'.corec' (Corec.f f) (Sum.inr b) 0 = Sum.rec Option.some (fun _ ↦ none) (f b)
by
dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
match (f b) with
| Sum.inl x => rfl
| Sum.inr x => rfl]
rcases h : f b with a | b'; · rfl
dsimp [Corec.f, destruct]
apply congr_arg; apply Subtype.eq
dsimp [corec, tail]
rw [Stream'.corec'_eq, Stream'.tail_cons]
dsimp [Corec.f]; rw [h]
