English
If f is Partrec' on (n+1) and you lift it to an option-coded result via rfindOpt, then the resulting function on n is Partrec'.
Русский
Если f — Partrec' на (n+1) и его результат кодируется через rfindOpt как опцион, то полученная функция на n есть Partrec'.
LaTeX
$$$$\forall {n} {f : \mathrm{List.Vector} \mathbb{N} (n+1) \to \mathbb{N}}, \; \mathrm{Nat.Partrec'}(f) \Rightarrow \mathrm{Nat.Partrec'}(\lambda v. \mathrm{Nat}.rfindOpt(\lambda a. \mathrm{ofNat}(\mathrm{Option}\, \mathbb{N})(f(a ::ᵥ v)))).$$$$
Lean4
theorem rfindOpt {n} {f : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n + 1) f) :
@Partrec' n fun v => Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v)) :=
((rfind <|
(of_prim (Primrec.nat_sub.comp (_root_.Primrec.const 1) Primrec.vector_head)).comp₁
(fun n => Part.some (1 - n)) hf).bind
((prim Nat.Primrec'.pred).comp₁ Nat.pred hf)).of_eq
fun v =>
Part.ext fun b =>
by
simp only [Nat.rfindOpt, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff, Part.mem_some_iff,
Option.mem_def, Part.mem_coe]
refine exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
· congr
funext n
cases f (n ::ᵥ v) <;> simp <;> rfl
· have := Nat.rfind_spec h
simp only [Part.coe_some, Part.mem_some_iff] at this
revert this; rcases f (a ::ᵥ v) with - | c <;> intro this
· cases this
rw [← Option.some_inj, eq_comm]
rfl
