Strong induction for List

Stream: lean4

[Jeremy Salwen]

For proofs about nat, I can use induction n using Nat.strong_induction_on to strengthen my induction hypothesis to be about all smaller numbers.

For a proof about lists, I would like to do a similar thing. I could imagine strengthening it to all suffixes, all prefixes, all substrings, etc, or ultimately all Lists with smaller sizeOf. I couldn't figure out how to do this.

[Mario Carneiro]

use termination_by _ l => l.length, it subsumes most of those

[James Gallicchio]

It would be nice to have a List.induction_by_length_on for use in tactic-mode.

[James Gallicchio]

I don't think it would be too hard to define using well-founded recursion like Mario suggested

[Jeremy Salwen]

Hmm ok I will try to implement it by copying Nat.strong_induction_on

[Jeremy Salwen]

Ok I think I did it! I wasn't able to prove it outside of tactics mode, but here it is:

 @[elab_as_elim]
 lemma List.induction_by_length_on {p : List α → Prop} (l : List α) (h : ∀ l, (∀ l₂, List.length l₂ < List.length l → p l₂) → p l) :
    p l := by
  generalize heq: length l = len
  induction len using Nat.strong_induction_on generalizing l with
  | h n ih =>
    subst heq
    exact h l (fun l₂ hlt => (ih (length l₂) hlt l₂ rfl))

I'm not sure if elab_as_elim is important.

[James Gallicchio]

elab_as_elim i .. think ? changes the way p is inferred in the definition. I believe it is right to put it there, but someone should correct me

[Mario Carneiro]

@[elab_as_elim]
lemma List.induction_by_length_on {p : List α → Prop} (l : List α)
    (IH : ∀ l, (∀ l₂, List.length l₂ < List.length l → p l₂) → p l) : p l :=
  IH l fun l₂ _ => List.induction_by_length_on l₂ IH
termination_by _ => l.length

is how you do it using termination_by