English
corec f b yields a Seq α by repeatedly applying f to generate elements; the head is produced when f(b) = some (a, s), and the rest is corec f s; if f(b) = none, the sequence is nil.
Русский
corec f b порождает Seq α, повторно применяя f для получения элементов; голова получается, если f(b) = some (a, s), остаток — corec f s; если f(b) = none, последовательность равна nil.
LaTeX
$$$\\text{corec}(f)(b) = \\begin{cases} \\mathrm{nil}, & f(b) = \\mathrm{none}, \\\\ \\mathrm{cons}(a, \\text{corec}(f)(s)), & f(b) = \\mathrm{some}(a, s). \\end{cases}$$$
Lean4
/-- Corecursor for `Seq α` as a coinductive type. Iterates `f` to produce new elements
of the sequence until `none` is obtained. -/
def corec (f : β → Option (α × β)) (b : β) : Seq α :=
by
refine ⟨Stream'.corec' (Corec.f f) (some b), fun {n} h => ?_⟩
rw [Stream'.corec'_eq]
change Stream'.corec' (Corec.f f) (Corec.f f (some b)).2 n = none
revert h; generalize some b = o
induction n generalizing o with
| zero =>
change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
rcases o with - | b <;> intro h
· rfl
dsimp [Corec.f] at h
dsimp [Corec.f]
revert h; rcases h₁ : f b with - | s <;> intro h
· rfl
· obtain ⟨a, b'⟩ := s
contradiction
| succ n IH =>
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
exact IH (Corec.f f o).2
