English
Given a Partrec₂ predicate p, one can form a partial recursive function computing rfind over p.
Русский
Заданной Partrec₂ предикат p можно построить частичную рекурсивную функцию, находящую rfind.
LaTeX
$$$\forall p:\alpha\toℕ\to^.Bool\; (Partrec₂(p) )\Rightarrow Partrec(\lambda a. Nat.rfind (p(a))).$$
Lean4
theorem rfind {p : α → ℕ →. Bool} (hp : Partrec₂ p) : Partrec fun a => Nat.rfind (p a) :=
(Nat.Partrec.rfind <| hp.map ((Primrec.dom_bool fun b => cond b 0 1).comp Primrec.snd).to₂.to_comp).of_eq fun n =>
by
rcases e : decode (α := α) n with - | a <;> simp [e, Nat.rfind_zero_none, map_id']
congr; funext n
simp only [map_map]
refine map_id' (fun b => ?_) _
cases b <;> rfl
