English
Every primitive recursive function is Partrec.
Русский
Каждая примитивно-рекурсивная функция является частично-рекурсивной.
LaTeX
$$$\text{Nat.Primrec } f \;\Rightarrow\; \text{Nat.Partrec } f$$$
Lean4
theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Partrec f := by
induction hf with
| zero => exact zero
| succ => exact succ
| left => exact left
| right => exact right
| pair _ _ pf pg =>
refine (pf.pair pg).of_eq_tot fun n => ?_
simp [Seq.seq]
| comp _ _ pf pg => refine (pf.comp pg).of_eq_tot fun n => (by simp)
| prec _ _ pf pg =>
refine (pf.prec pg).of_eq_tot fun n => ?_
simp only [unpaired, PFun.coe_val, bind_eq_bind]
induction n.unpair.2 with
| zero => simp
| succ m IH =>
simp only [mem_bind_iff, mem_some_iff]
exact ⟨_, IH, rfl⟩
