English
Under suitable primrec f and p, the function a ↦ (f a).findIdx (p a) is primitive recursive.
Русский
При подходящих примитивных f и p отображение a ↦ (f a).findIdx (p a) примитивно вычислимо.
LaTeX
$$$\\mathrm{Primrec}\\left( a \\mapsto (f(a)).\\mathrm{findIdx}\\left( p(a) \\right) \\right)$$$
Lean4
/-- Filtering a list for elements that satisfy a decidable predicate is primitive recursive. -/
theorem listFilter (hf : PrimrecPred p) : Primrec fun L ↦ List.filter (p ·) L :=
by
rw [← List.filterMap_eq_filter]
apply listFilterMap .id
simp only [Primrec₂, Option.guard, decide_eq_true_eq]
exact ite (hf.comp snd) (option_some_iff.mpr snd) (const none)
