English
The function List.lookup : α → List (α × β) → Option β is primitive recursive in its two inputs.
Русский
Функция List.lookup : α → List(α × β) → Option β является примитивно-рекурсивной по двум входам.
LaTeX
$$$ \mathrm{PR}_2\big(\mathrm{List.lookup} : \alpha \times \mathrm{List}(\alpha \times \beta) \to \mathrm{Option}(\beta)\big)$$
Lean4
theorem listLookup [DecidableEq α] : Primrec₂ (List.lookup : α → List (α × β) → Option β) :=
(to₂ <|
list_rec snd (const none) <|
to₂ <|
cond (Primrec.beq.comp (fst.comp fst) (fst.comp <| fst.comp snd))
(option_some.comp <| snd.comp <| fst.comp snd) (snd.comp <| snd.comp snd)).of_eq
fun a ps => by
induction ps with simp [List.lookup, *]
| cons p ps ih => cases ha : a == p.1 <;> simp
