List.dropWhile head false

Stream: Is there code for X?

[Martin Dvořák]

I would like a lemma for one of the following examples:

import Mathlib.Data.List.Basic

variable {α : Type} {l : List α} {P : α → Bool}

example (nonempty : l.dropWhile P ≠ []) :
  decide (P ((l.dropWhile P).head nonempty)) = false :=
by
  sorry

example (pos_length : 0 < (l.dropWhile P).length) :
  decide (P ((l.dropWhile P).get ⟨0, pos_length⟩)) = false :=
by
  sorry

[Martin Dvořák]

I think it should go to Mathlib:

import Mathlib.Data.List.Basic

variable {α : Type} {l : List α} {P : α → Bool}

lemma List.decide_dropWhile_head (hl : l.dropWhile P ≠ []) :
  decide (P ((l.dropWhile P).head hl)) = false :=
by
  induction l with
  | nil => simp at hl
  | cons d _ ih => by_cases P d <;> simp_all [List.dropWhile]

[Eric Wieser]

I don't think mathlib should have any lemmas about decide; decide P = false should be stated as ¬P

[Timo Carlin-Burns]

P here is actually a Bool, so maybe just P = false?

[Martin Dvořák]

My bad!

import Mathlib.Data.List.Basic

variable {α : Type} {l : List α} {P : α → Bool}

lemma List.decide_dropWhile_head (hl : l.dropWhile P ≠ []) :
  P ((l.dropWhile P).head hl) = false :=
by
  induction l with
  | nil => simp at hl
  | cons d _ ih => by_cases P d <;> simp_all [List.dropWhile]

[Timo Carlin-Burns]

docs#List.dropWhile_nthLe_zero_not looks like almost exactly what you're proving. That theorem uses the ¬P = true spelling

[Eric Wieser]

A lot of these lemmas will be a mess because in lean 3 dropWhile took a function to Prop not bool

[Martin Dvořák]

Timo Carlin-Burns said:

docs#List.dropWhile_nthLe_zero_not looks like almost exactly what you're proving. That theorem uses the ¬P = true spelling

Isn't List.nthLe deprecated?

[Eric Wieser]

Yes, but a lot of this stuff was ported without much thought, and hasn't yet received a cleanup pass.