list_getElem? — Mathlib

English

There is a primitive recursive function for List.getElem? with respect to a bound on length.

Русский

Существует примитивно вычислимая функция List.getElem? по ограничению на длину.

LaTeX

$$$\\mathrm{Primrec}_2((\\cdot[\\cdot]? : List α → \\mathbb{N} → \\mathrm{Option} α))$$$

Lean4

theorem list_getElem? : Primrec₂ ((·[·]? : List α → ℕ → Option α)) :=
  let F (l : List α) (n : ℕ) :=
    l.foldl (fun (s : ℕ ⊕ α) (a : α) => Sum.casesOn s (@Nat.casesOn (fun _ => ℕ ⊕ α) · (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n)
  have hF : Primrec₂ F :=
    (list_foldl fst (sumInl.comp snd)
        ((sumCasesOn fst (nat_casesOn snd (sumInr.comp <| snd.comp fst) (sumInl.comp snd).to₂).to₂
                (sumInr.comp snd).to₂).comp
            snd).to₂).to₂
  have : @Primrec _ (Option α) _ _ fun p : List α × ℕ => Sum.casesOn (F p.1 p.2) (fun _ => none) some :=
    sumCasesOn hF (const none).to₂ (option_some.comp snd).to₂
  this.to₂.of_eq fun l n => by
    dsimp; symm
    induction l generalizing n with
    | nil => rfl
    | cons a l IH =>
      rcases n with - | n
      · dsimp [F]
        clear IH
        induction l <;> simp_all
      · simpa using IH ..

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