English
If f: α → Nat → σ and g: α → List σ → Option σ with g computable and a hypothesis H ensuring a strong recursion property, then f is computable.
Русский
Если f : α → Nat → σ и g : α → List σ → Option σ с вычислимостью и условием H, гарантирующим строгую рекурсию, то f вычислима.
LaTeX
$$$\mathrm{Nat.Partrec}\; f \Rightarrow \mathrm{Computable}_2\; f$ (упрощено) + продолжение конструкции,
\mathrm{Partrec}\; f$$$
Lean4
theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Computable₂ g)
(H : ∀ a n, g a ((List.range n).map (f a)) = Option.some (f a n)) : Computable₂ f :=
suffices Computable₂ fun a n => (List.range n).map (f a) from
option_some_iff.1 <| (list_getElem?.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq fun a => by simp
option_some_iff.1 <|
(nat_rec snd (const (Option.some []))
(to₂ <|
option_bind (snd.comp snd) <|
to₂ <|
option_map (hg.comp (fst.comp <| fst.comp fst) snd) (to₂ <| list_concat.comp (snd.comp fst) snd))).of_eq
fun a => by
induction a.2 with
| zero => rfl
| succ n IH => simp [IH, H, List.range_succ]
