List strong induction

Stream: mathlib4

[Marcus Rossel]

From this topic it seems that the following theorem isn't in Lean/Std/Mathlib yet:

-- Note: The induction hypothesis states "if l₂ is a strict suffix of hd::tl, then p l₂".
theorem List.strongInduction {p : List α → Prop} (l : List α)
    (nil  : p [])
    (cons : ∀ hd tl, (∀ {hd₁ tl₁ l₂}, hd₁::tl₁ ++ l₂ = hd::tl → p l₂) → p (hd::tl)) :
    p l := by
  generalize hl : l.length = len
  induction len using Nat.strongInductionOn generalizing l <;> cases ‹Nat› <;> cases l
  case ind.succ.cons hi _ _ => exact cons _ _ fun h => hi _ (by simp_arith [←hl, ←h]) _ rfl
  all_goals simp_all

Before I open a PR on Github I would like to find out whether this is a theorem worth having. I've used it before, preferring it over Nat.strongInductionOn on the list's length. I wonder though if there's a better way of stating the induction hypothesis. Any feedback would be great :)

[Joachim Breitner]

This way of expressing “strict prefix” feels rather convoluted to me. Does this really lead to nicer proofs than going by induction on the length of the list?

Also have you considered other ways of expressing this that don't juggle so many hd :: things:

theorem List.suffixInduction {p : List α → Prop} (l : List α) (step : ∀ l, (IH : ∀ l', l'.isSuffixOf l → l ≠ l' → p l') :  p l