List length induction

Stream: Is there code for X?

[David E. Narváez]

Where is the principle of length induction? (Or well-foundedness of List.length so one can use WellFounded.induction.)

[Kenny Lau]

Could you please include the theorem with sorry as the proof? (#mwe)

[Floris van Doorn]

Not as a single lemma, but it's not hard to do this manually:

example {α} (P : List α → Prop) {l : List α} : P l := by
  generalize h : l.length = n
  induction n generalizing l with
  | zero =>
    simp at h
    subst h
    sorry
  | succ n ih =>
    cases l with
    | nil => simp at h
    | cons head tail =>
      simp at h
      subst h
      sorry

[David E. Narváez]

Kenny Lau said:

Could you please include the theorem with sorry as the proof? (#mwe)

namespace List

lemma length_wf {α : Type} : WellFounded (λ (x y : List α) ↦ x.length < y.length) := by
  suffices acc_len : ∀ (n : ℕ) (l : List α), l.length ≤ n → Acc (λ (x y : List α) ↦ x.length < y.length) l by
    constructor
    intro l
    apply acc_len l.length
    simp
  intro n
  induction n with
  | zero =>
    simp
    constructor
    intros y yltx
    simp at yltx
  | succ m ih =>
    intros l
    cases l with
    | nil =>
      simp
      constructor
      intros y yltx
      simp at yltx
    | cons h t =>
      simp
      intros tlen
      constructor
      intros y ylen
      simp [Nat.lt_add_one_iff] at ylen
      apply ih
      trans t.length <;> assumption

end List

To later be used as

induction P using WellFounded.induction List.length_wf

though arguably there should be something defined as

def List.length_induction = WellFounded.induction List.length_wf

[Kenny Lau]

@David E. Narváez

namespace List

theorem length_wf {α : Type} : WellFounded (λ (x y : List α) ↦ x.length < y.length) :=
  InvImage.wf _ Nat.lt_wfRel.2

[Kenny Lau]

David E. Narváez said:

induction P using WellFounded.induction List.length_wf

but this is an #xy problem, you wanted to use WellFounded.induction List.length_wf in the first place, so it would be better to write down just the induction theorem instead of taking a path (i.e. using WellFounded) that you think is the right path

[David E. Narváez]

I think more importantly I would like to know where in Mathlib can I find the length induction principle so that I do not have to add (any version of) the above code to every project where I need length induction.

[Dexin Zhang]

You can also use Nat.strong_induction_on on l.length

[Kenny Lau]

David E. Narváez said:

I think more importantly I would like to know where in Mathlib can I find the length induction principle so that I do not have to add (any version of) the above code to every project where I need length induction.

I'm saying that you can do "length induction" without separately having that lemma

[Kenny Lau]

or did you mean recursion? induction is about proofs

[David E. Narváez]

I mean I want to be able to write

induction P using List.length_induction

in a proof.

[Kenny Lau]

right, and Floris above is suggesting instead:

generalize h : l.length = n
induction n generalizing l

[Dexin Zhang]

induction can do generalize also

induction h : l.length generalizing l