twoStepInduction

Mathlib.Data.List.Induction

URI: https://scilib.ai/kg/mathlib#List.twoStepInduction

Lean4

/-- A recursion principle for lists which separates the singleton case.
-/
@[elab_as_elim]
def twoStepInduction {motive : (l : List α) → Sort*} (nil : motive []) (singleton : ∀ x, motive [x])
    (cons_cons : ∀ x y xs, motive xs → (∀ y, motive (y :: xs)) → motive (x :: y :: xs)) (l : List α) : motive l :=
  match l with
  | [] => nil
  | [x] => singleton x
  | x :: y :: xs =>
    cons_cons x y xs (twoStepInduction nil singleton cons_cons xs)
      (fun y => twoStepInduction nil singleton cons_cons (y :: xs))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru