English
If f is a Nat.Primrec' function on Nat vectors, then f is Primrec in the standard sense.
Русский
Если f — функция Nat.Primrec' на векторах натур, то она примитивно-рекурсивна в обычном смысле.
LaTeX
$$$$ \\forall n, \\forall f:\\mathrm{List.Vector}\\ \\mathbb{N}\\ n \\to \\mathbb{N},\\ \\mathrm{Nat.Primrec'}(f) \\Rightarrow \\operatorname{Primrec}(f). $$$$
Lean4
theorem to_prim {n f} (pf : @Nat.Primrec' n f) : Primrec f := by
induction pf with
| zero => exact .const 0
| succ => exact _root_.Primrec.succ.comp .vector_head
| get i => exact Primrec.vector_get.comp .id (.const i)
| comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
| @prec n f g _ _ hf hg =>
exact
.nat_rec' .vector_head (hf.comp Primrec.vector_tail)
(hg.comp <|
Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
Primrec.vector_cons.comp (Primrec.snd.comp .snd) <| (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
