English
Corecursion defines a corecursive constructor for a coinductive computation type.
Русский
Курсорная рекурсия задаёт ядровой рекурсивный конструктор для коиндуктивного типа вычислений.
LaTeX
$$$\\mathrm{corec} : (\\beta \\to \\alpha \\oplus \\beta) \\to \\beta \\to \\mathrm{Computation}\\,\\alpha$$$
Lean4
/-- `corec f b` is the corecursor for `Computation α` as a coinductive type.
If `f b = inl a` then `corec f b = pure a`, and if `f b = inl b'` then
`corec f b = think (corec f b')`. -/
def corec (f : β → α ⊕ β) (b : β) : Computation α :=
by
refine ⟨Stream'.corec' (Corec.f f) (Sum.inr b), fun n a' h => ?_⟩
rw [Stream'.corec'_eq]
change Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).2 n = some a'
revert h; generalize Sum.inr b = o
induction n generalizing o with
| zero =>
change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
rcases o with _ | b <;> intro h
· exact h
unfold Corec.f at *; split <;> simp_all
| 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
