list_findIdx — Mathlib

English

A suitable primitive recursive encoding yields Primrec for the findIdx operation.

Русский

Подходящее примитивно вычислимое кодирование даёт примитивную рекурсию для findIdx.

LaTeX

$$$\\mathrm{Primrec}\\left( a \\mapsto (f(a)).\\mathrm{findIdx}(p(a)) \\right)$$$

Lean4

theorem list_findIdx {f : α → List β} {p : α → β → Bool} (hf : Primrec f) (hp : Primrec₂ p) :
    Primrec fun a => (f a).findIdx (p a) :=
  (list_foldr hf (const 0) <| to₂ <| cond (hp.comp fst <| fst.comp snd) (const 0) (succ.comp <| snd.comp snd)).of_eq
    fun a => by dsimp; induction f a <;> simp [List.findIdx_cons, *]

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