theorems about dropWhile

Stream: lean4

[Damiano Testa]

Dear All,

for my own benefit, I proved some trivialities about docs4#List.dropWhile -- you can find them below.

If anyone thinks that they may be useful, let me know and I can PR them somewhere!

Thanks!

import Std.Data.List.Basic

theorem List.dropWhile_of_true {a : α} {L : List α} {c : α → Bool} (ca : c a = true) :
    (a::L).dropWhile c = L.dropWhile c := by simp [ca]

theorem List.dropWhile_of_false {a : α} {L : List α} {c : α → Bool} (ca : c a = false) :
    (a::L).dropWhile c = a :: L := by simp [ca]

theorem List.length_dropWhile {L : List α} {c : α → Bool} : (L.dropWhile c).length ≤ L.length := by
  cases L with
    | nil => simp
    | cons a as => if h : c a
      then
        rw [List.dropWhile_of_true h];
        exact Nat.le_trans List.length_dropWhile (Nat.le_succ _)
      else rw [List.dropWhile_of_false]; simp; simp [h]

[Eric Wieser]

Do we want to be making non-meta feature PRs to mathlib4 yet?

[Damiano Testa]

It was not my intention to push for these lemmas to be PRed: I simply "needed" these lemmas, saw that docs4#List.length_drop exists and wondered whether then also some dropWhile lemmas were to be expected!

It is certainly of no priority for me!

[Eric Rodriguez]

I guess we'd have to reverse-synchronise them, which seems irritating. We could put them in non-synced files for the time being.

[Eric Rodriguez]

e.g. these could be in Data/List/DropWhile4.lean where the 4 symbolises that these are mathlib4-only files. we could, after the port is done, then merge everything into the correct files

[Damiano Testa]

The reason for me "needing" these lemmas was to remove a partial in a definition that I had. Now that I have convinced Lean that partial is superfluous, I can live with having a partial! :upside_down:

[Ruben Van de Velde]

Or in this case, PR them to std4 directly? :)

[Damiano Testa]

I am happy to make a PR to std4, but also to wait and possibly not PR these lemmas at all! :smile:

[Damiano Testa]

I also just noticed that with mathlib, the proof is easier, although I had to fight a decidable typeclass:

import Mathlib.Data.List.Infix

theorem List.length_dropWhile {L : List α} {c : α → Bool} : (L.dropWhile c).length ≤ L.length := by
  convert List.isSuffix.length_le (@List.dropWhile_suffix α L (c ·) _)
  simp only [Bool.decide_coe]

[Mario Carneiro]

Eric Wieser said:

Do we want to be making non-meta feature PRs to mathlib4 yet?

Yes, certainly. There are no restrictions on new material in mathlib4 besides compatibility with mathlib, and I absolutely do not want to send a message that mathlib4 is "frozen" at all!

[Eric Wieser]

Should we have a compromise like "all mathlib4-new material in existing files should go at the bottom of the file", so as not to interfere with forward-ports?

[James Gallicchio]

would it also be fine to make changes to anything where the lean3 mathlib file is frozen?

[Eric Wieser]

Are there any such files?

[Damiano Testa]

While I agree with the spirit, now that I am at a computer that actually has Lean4, instead of using the online editor, I can see that the lemma that I had was completely trivial, given what is in mathlib4:

theorem List.length_dropWhile {L : List α} {c : α → Bool} : (L.dropWhile c).length ≤ L.length :=
  List.isSuffix.length_le (List.dropWhile_suffix (c ·))

If you think that it is worth to PR it, I can do it, but maybe it is too trivial, even from the point of view of formalization! :smile: