Mathlib.Data.List.TakeWhile

List.dropWhile_get_zero_not theorem

(l : List α) (hl : 0 < (l.dropWhile p).length) : ¬p ((l.dropWhile p).get ⟨0, hl⟩)

Full source

theorem dropWhile_get_zero_not (l : List α) (hl : 0 < (l.dropWhile p).length) :
    ¬p ((l.dropWhile p).get ⟨0, hl⟩) := by
  induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]

First Element of `dropWhile` Fails Predicate

Informal description

For any list `l` of type `α` and a predicate `p`, if the length of `l.dropWhile p` is positive, then the first element of `l.dropWhile p` does not satisfy the predicate `p`. In other words, if `dropWhile p l` is non-empty, then `p` does not hold for its first element.

List.dropWhile_eq_nil_iff theorem

: dropWhile p l = [] ↔ ∀ x ∈ l, p x

Full source

@[simp]
theorem dropWhile_eq_nil_iff : dropWhiledropWhile p l = [] ↔ ∀ x ∈ l, p x := by
  induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

Empty `dropWhile` Condition: $\text{dropWhile } p \, l = [] \leftrightarrow \forall x \in l, p(x)$

Informal description

For any predicate $p$ and list $l$, the `dropWhile p l` operation results in an empty list if and only if every element $x$ in $l$ satisfies the predicate $p$. In other words, $\text{dropWhile } p \, l = [] \leftrightarrow \forall x \in l, p(x)$.

List.takeWhile_eq_self_iff theorem

: takeWhile p l = l ↔ ∀ x ∈ l, p x

Full source

@[simp]
theorem takeWhile_eq_self_iff : takeWhiletakeWhile p l = l ↔ ∀ x ∈ l, p x := by
  induction l with
  | nil => simp
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

`takeWhile` Preserves List if and only if All Elements Satisfy Predicate

Informal description

For any predicate $p$ and list $l$, the operation $\text{takeWhile } p \, l$ results in the original list $l$ if and only if every element $x$ in $l$ satisfies the predicate $p$. In other words, $\text{takeWhile } p \, l = l \leftrightarrow \forall x \in l, p(x)$.

List.takeWhile_eq_nil_iff theorem

: takeWhile p l = [] ↔ ∀ hl : 0 < l.length, ¬p (l.get ⟨0, hl⟩)

Full source

@[simp]
theorem takeWhile_eq_nil_iff : takeWhiletakeWhile p l = [] ↔ ∀ hl : 0 < l.length, ¬p (l.get ⟨0, hl⟩) := by
  induction l with
  | nil =>
    simp only [takeWhile_nil, Bool.not_eq_true, true_iff]
    intro h
    simp at h
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

Empty `takeWhile` Condition: $\text{takeWhile } p \, l = [] \leftrightarrow \forall h_l, \neg p(l[0])$

Informal description

For any predicate $p$ and list $l$, the `takeWhile p l` operation results in an empty list if and only if for every positive length index $0 < \text{length}(l)$, the predicate $p$ does not hold for the first element of $l$. In other words, $\text{takeWhile } p \, l = []$ if and only if for all $h_l : 0 < \text{length}(l)$, we have $\neg p(l[0])$ (where $l[0]$ denotes the first element of $l$).

List.mem_takeWhile_imp theorem

{x : α} (hx : x ∈ takeWhile p l) : p x

Full source

theorem mem_takeWhile_imp {x : α} (hx : x ∈ takeWhile p l) : p x := by
  induction l with simp [takeWhile] at hx
  | cons hd tl IH =>
    cases hp : p hd
    · simp [hp] at hx
    · rw [hp, mem_cons] at hx
      rcases hx with (rfl | hx)
      · exact hp
      · exact IH hx

Elements in `takeWhile` Satisfy the Predicate

Informal description

For any element $x$ in the list obtained by `takeWhile p l`, the predicate $p$ holds for $x$.

List.takeWhile_takeWhile theorem

(p q : α → Bool) (l : List α) : takeWhile p (takeWhile q l) = takeWhile (fun a => p a ∧ q a) l

Full source

theorem takeWhile_takeWhile (p q : α → Bool) (l : List α) :
    takeWhile p (takeWhile q l) = takeWhile (fun a => p a ∧ q a) l := by
  induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

Composition of `takeWhile` Operations via Conjunction

Informal description

For any predicates $p, q : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, the operation of taking elements from $l$ while $p$ holds, applied to the result of taking elements from $l$ while $q$ holds, is equal to taking elements from $l$ while both $p$ and $q$ hold simultaneously. In symbols: \[ \text{takeWhile } p (\text{takeWhile } q \, l) = \text{takeWhile } (\lambda a, p a \land q a) \, l \]

List.takeWhile_idem theorem

: takeWhile p (takeWhile p l) = takeWhile p l

Full source

theorem takeWhile_idem : takeWhile p (takeWhile p l) = takeWhile p l := by
  simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]

Idempotence of `takeWhile` Operation

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any list $l : \text{List } \alpha$, applying the `takeWhile p` operation twice is equivalent to applying it once. That is: \[ \text{takeWhile } p (\text{takeWhile } p \, l) = \text{takeWhile } p \, l \]

List.find?_eq_head?_dropWhile_not theorem

: l.find? p = (l.dropWhile (fun x ↦ !(p x))).head?

Full source

lemma find?_eq_head?_dropWhile_not :
    l.find? p = (l.dropWhile (fun x ↦ ! (p x))).head? := by
  induction l
  case nil => simp
  case cons head tail hi =>
    set ph := p head with phh
    rcases ph with rfl | rfl
    · have phh' : ¬(p head = true) := by simp [phh.symm]
      rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
      · exact hi
      · simpa using phh
    · rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
      · simp
      · simpa using phh

Equivalence of find? and head? after dropWhile negation

Informal description

For any list `l` and predicate `p`, the first element of `l` satisfying `p` (if it exists) is equal to the head of the list obtained by dropping elements from `l` while they do not satisfy `p`. In other words, the `find?` operation on `l` with predicate `p` is equivalent to taking the head of the list after dropping all initial elements that fail to satisfy `p`. Formally, this can be written as: $$\text{find? } p\ l = \text{head? } (\text{dropWhile } (\lambda x.\ \neg p\ x)\ l)$$

List.find?_not_eq_head?_dropWhile theorem

: l.find? (fun x ↦ !(p x)) = (l.dropWhile p).head?

Full source

lemma find?_not_eq_head?_dropWhile :
    l.find? (fun x ↦ ! (p x)) = (l.dropWhile p).head? := by
  convert l.find?_eq_head?_dropWhile_not ?_
  simp

Equivalence of Negated Find and Head After DropWhile

Informal description

For any list $l$ and predicate $p$, the first element of $l$ that does not satisfy $p$ (if it exists) is equal to the head of the list obtained by dropping all initial elements of $l$ that satisfy $p$. Formally, this can be written as: $$\text{find? } (\lambda x.\ \neg p\ x)\ l = \text{head? } (\text{dropWhile } p\ l)$$

List.find?_eq_head_dropWhile_not theorem

(h : ∃ x ∈ l, p x) : l.find? p = some ((l.dropWhile (fun x ↦ !(p x))).head (by simpa using h))

Full source

lemma find?_eq_head_dropWhile_not (h : ∃ x ∈ l, p x) :
    l.find? p = some ((l.dropWhile (fun x ↦ ! (p x))).head (by simpa using h)) := by
  rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]

First Satisfying Element Equals Head After Dropping Non-Satisfying Elements

Informal description

Given a list $l$ and a predicate $p$, if there exists an element $x \in l$ such that $p(x)$ holds, then the first such element found by `find?` is equal to the head of the list obtained by dropping all initial elements of $l$ that do not satisfy $p$. Formally, this can be written as: $$\text{find? } p\ l = \text{some } \big(\text{head } (\text{dropWhile } (\lambda x.\ \neg p\ x)\ l)\big)$$

List.find?_not_eq_head_dropWhile theorem

(h : ∃ x ∈ l, ¬p x) : l.find? (fun x ↦ !(p x)) = some ((l.dropWhile p).head (by simpa using h))

Full source

lemma find?_not_eq_head_dropWhile (h : ∃ x ∈ l, ¬p x) :
    l.find? (fun x ↦ ! (p x)) = some ((l.dropWhile p).head (by simpa using h)) := by
  convert l.find?_eq_head_dropWhile_not ?_
  · simp
  · simpa using h

First Non-Satisfying Element Equals Head After Dropping Satisfying Elements

Informal description

Given a list $l$ and a predicate $p$, if there exists an element $x \in l$ such that $\neg p(x)$ holds, then the first such element found by `find?` is equal to the head of the list obtained by dropping all initial elements of $l$ that satisfy $p$. Formally, this can be written as: $$\text{find? } (\lambda x.\ \neg p\ x)\ l = \text{some } \big(\text{head } (\text{dropWhile } p\ l)\big)$$