English
If a function f on vectors is Partrec, then its encodable version encoded via Partrec' exists; i.e., Partrec f implies Partrec' f.
Русский
Если функция f на векторах является Partrec, то её кодируемая версия существует; то есть Partrec f ⇒ Partrec' f.
LaTeX
$$$$\forall {n}{f : \mathrm{PFun} (\mathrm{List.Vector} \mathbb{N} n) \mathbb{N}}, \; \mathrm{Partrec}(f) \Rightarrow \mathrm{Nat.Partrec'}(f).$$$$
Lean4
theorem of_part : ∀ {n f}, _root_.Partrec f → @Partrec' n f :=
@(suffices ∀ f, Nat.Partrec f → @Partrec' 1 fun v => f v.head from fun {n f} hf =>
by
let g := fun n₁ => (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
exact
(comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by dsimp only [g]; simp [encodek, Part.map_id']
fun f hf => by
obtain ⟨c, rfl⟩ := exists_code.1 hf
simpa [eval_eq_rfindOpt] using
rfindOpt <|
of_prim <|
Primrec.encode_iff.2 <|
primrec_evaln.comp <|
(Primrec.vector_head.pair (_root_.Primrec.const c)).pair <| Primrec.vector_head.comp Primrec.vector_tail)
