list_findIdx₁ — Mathlib

English

For any predicate p and list l, the function a ↦ l.findIdx (p a) is primitive recursive.

Русский

Для любого предиката p и списка l функция a ↦ l.findIdx(p a) примитивно рекурсивна.

LaTeX

$$$\\forall p:\\alpha\\to\\beta\\to\\mathsf{Bool},\\ Primrec_2 p\\;\\to\\; \\forall l:\\mathrm{List}\,\\beta,\\ Primrec (\\lambda a. \\mathrm{List.findIdx}(p\\,a)\\,l)$$$

Lean4

theorem list_findIdx₁ {p : α → β → Bool} (hp : Primrec₂ p) : ∀ l : List β, Primrec fun a => l.findIdx (p a)
  | [] => const 0
  | a :: l =>
    (cond (hp.comp .id (const a)) (const 0) (succ.comp (list_findIdx₁ hp l))).of_eq fun n => by simp [List.findIdx_cons]

Похожие утверждения