Induction principles

Stream: Is there code for X?

[Bolton Bailey]

Do we have something like

lemma list_induction (P : List α → Prop) :
    (∀ (l : List α), P l) ↔ ( P [] ∧ (∀ (a : α) (l : List α), P l → P (a :: l))) := by
  sorry

[Bolton Bailey]

I feel like I was told once that when an inductive datatype is declared, a lemma like this is automatically generated.

[Junyan Xu]

#check List.rec
/- List.rec.{u_1, u} {α : Type u} {motive : List α → Sort u_1} (nil : motive [])
  (cons : (head : α) → (tail : List α) → motive tail → motive (head :: tail)) (t : List α) : motive t -/
lemma list_induction {α} (P : List α → Prop) :
    (∀ (l : List α), P l) ↔ ( P [] ∧ (∀ (a : α) (l : List α), P l → P (a :: l))) :=
  ⟨fun h ↦ ⟨h _, fun _ _ _ ↦ h _⟩, fun h ↦ List.rec h.1 h.2⟩