English
List recursion is primitive recursive when the step function is primitive recursive and the base case is primitive recursive.
Русский
Рекурсия по спискам примитивно вычислима, если базовый случай и шаговые функции примитивно вычислимы.
LaTeX
$$$\\mathrm{Primrec}\\left( a \\mapsto \\mathrm{List.recOn}(f(a))(g(a))(\\lambda b\\ l IH. h(a)(b,l,IH)) \\right)$$$
Lean4
theorem list_rec {f : α → List β} {g : α → σ} {h : α → β × List β × σ → σ} (hf : Primrec f) (hg : Primrec g)
(hh : Primrec₂ h) : @Primrec _ σ _ _ fun a => List.recOn (f a) (g a) fun b l IH => h a (b, l, IH) :=
let F (a : α) := (f a).foldr (fun (b : β) (s : List β × σ) => (b :: s.1, h a (b, s))) ([], g a)
have : Primrec F :=
list_foldr hf (pair (const []) hg) <| to₂ <| pair ((list_cons.comp fst (fst.comp snd)).comp snd) hh
(snd.comp this).of_eq fun a =>
by
suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
dsimp [F]
induction f a <;> simp [*]
