Contributing a strong induction for lists

Stream: new members

[Will Crichton]

I implemented a strong induction principle for lists that works over all suffixes. The signature is:

def List.IsStrictSuffix {α} (l1 l2 : List α) := ∃ t ≠ [], t ++ l1 = l2

def List.suffix_induction {α} {p : List α → Prop}
  (l : List α)
  (nil : p nil)
  (cons : ∀ head tail, (∀ l', l'.IsStrictSuffix (head :: tail) → p l') → p (head :: tail))
  : p l

Full source link.

Would it be useful to submit this as a contribution to Mathlib? I was hoping something like this was in Mathlib, but there wasn't, so I implemented it myself.

[Joachim Breitner]

Is this principle more useful than using strong induction on list lengths? It seems that if you can prove IsStrictSuffix you can prove that one list is smaller than the other one easily.

[Joachim Breitner]

Also, it may not be needed to have a separate nil and cons case, and a single case might be nicer.

[Will Crichton]

I'm actually not sure how to prove the induction principle for list lengths. That was my first intuition, but you end up needing to show that l1.length < l2.length -> sizeOf l1 < sizeOf l2 and that is not true. Maybe I did something wrong in the proof.

[Will Crichton]

But yes more generally, I think Mathlib should have some strong induction principle for lists. This is just the one I could figure out :-)

[Joachim Breitner]

Try termination_by l.length before your decreasing_by

[Joachim Breitner]

Also, there isn’t really anything special about List.length here, so a single induction principle for any α → Nat should suffice:

def Nat.strongIndutionMeasureOn {α} {motive : α → Sort _} (f : α → Nat)
   (x : α) (step : (x : α) → ((y : α) → f y < f x → motive y) → motive x) : motive x :=
  step x (fun y _ => Nat.strongIndutionMeasureOn f y step)
termination_by f x

example (x : List Nat) : x = x := by
  induction x using Nat.strongIndutionMeasureOn (f := List.length)
  case step x ih =>
    -- 1 goal
    -- x: List Nat
    -- ih: ∀ (y : List Nat), y.length < x.length → y = y
    -- ⊢ x = x
    sorry

[llllvvuu]

Joachim Breitner said:

Is this principle more useful than using strong induction on list lengths?

Maybe if there is a use case where the statement is indeed true only for suffixes and not arbitrary lists, then one would need to create this hypothesis, e.g.:

import Batteries.Data.List.Lemmas
import Mathlib.Tactic.Cases

example (x : List Nat) : x = x := by
  generalize hy : x = y
  replace hy : y <:+ x := hy ▸ x.suffix_refl

  -- induction y using Nat.strongInductionMeasureOn List.length with | _ y ih => ?_
  induction' hn : y.length using Nat.strongInductionOn with n ih generalizing y
  induction y using (measure List.length).wf.induction with | _ y ih => ?_
  sorry

But I guess this can't be solved by an induction principle.

[llllvvuu]

Joachim Breitner said:

Also, it may not be needed to have a separate nil and cons case, and a single case might be nicer.

I guess if one wanted to mimic the multiset API one could rename List.strongRec and List.suffix_induction to List.strongInduction and List.caseStrongInductionOn respectively, and also add List.strongInductionOn (funny thing: this is spelled differently in docs#Nat.caseStrongInductionOn, docs#Multiset.case_strongInductionOn, and docs#Finset.case_strong_induction_on). Though I agree the non-case variant is often better / there are very few usages of the case variants in mathlib.

[Marcus Rossel]

Side note: I've asked the same question before here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.20strong.20induction

[llllvvuu]

(deleted)

[llllvvuu]

I was just about to propose it in Batteries anyway thinking it did something that the Nat version didn't, but then I realized I got confused, so I closed it. Maybe it could still be of interest in Mathlib for the sake of completeness / showing up in search results (interestingly, docs#Finset.strongInductionOn does actually get used a few times), if not useful in Batteries.

But I did put in a proposal to add Joachim Breitner's α → Nat idea from above.