English
A variant of the strong recursion principle for natural numbers holds under primitive recursive hypotheses.
Русский
Альтернатива принципа сильной рекурсии по натуральным числам сохраняется при примитивно вычислимых предпосылках.
LaTeX
$$$\\text{Primrec}_2\\ f \\Rightarrow \\text{Primrec}_2\\ g \\Rightarrow \\text{Primrec}_2\\ f$$$
Lean4
theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Primrec₂ g)
(H : ∀ a n, g a ((List.range n).map (f a)) = some (f a n)) : Primrec₂ f :=
suffices Primrec₂ fun a n => (List.range n).map (f a) from
Primrec₂.option_some_iff.1 <| (list_getElem?.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq fun a n => by simp
Primrec₂.option_some_iff.1 <|
(nat_rec (const (some []))
(to₂ <|
option_bind (snd.comp snd) <|
to₂ <| option_map (hg.comp (fst.comp fst) snd) (to₂ <| list_concat.comp (snd.comp fst) snd))).of_eq
fun a n => by
induction n with
| zero => rfl
| succ n IH => simp [IH, H, List.range_succ]
