Init.Data.List.Nat.Basic

List.tail_dropLast theorem

{l : List α} : tail (dropLast l) = dropLast (tail l)

Full source

theorem tail_dropLast {l : List α} : tail (dropLast l) = dropLast (tail l) := by
  ext1
  simp only [getElem?_tail, getElem?_dropLast, length_tail]
  split <;> split
  · rfl
  · omega
  · omega
  · rfl

Tail and DropLast Commute on Lists

Informal description

For any list $l$ of elements of type $\alpha$, the tail of the list obtained by removing the last element of $l$ is equal to the list obtained by removing the last element of the tail of $l$. In other words: $$\text{tail}(\text{dropLast}(l)) = \text{dropLast}(\text{tail}(l))$$

List.dropLast_reverse theorem

{l : List α} : l.reverse.dropLast = l.tail.reverse

Full source

@[simp] theorem dropLast_reverse {l : List α} : l.reverse.dropLast = l.tail.reverse := by
  apply ext_getElem
  · simp
  · intro i h₁ h₂
    simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail]
    congr
    simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂
    omega

Reversed List Drop-Last Equals Tail Reversed: $(l^{\text{reverse}}).\text{dropLast} = (\text{tail}(l))^{\text{reverse}}$

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by first reversing $l$ and then removing its last element is equal to the list obtained by first removing the first element of $l$ and then reversing the resulting list. In symbols: $$ (l^{\text{reverse}}).\text{dropLast} = (\text{tail}(l))^{\text{reverse}} $$

List.length_filter_pos_iff theorem

{l : List α} {p : α → Bool} : 0 < (filter p l).length ↔ ∃ x ∈ l, p x

Full source

@[simp]
theorem length_filter_pos_iff {l : List α} {p : α → Bool} :
    0 < (filter p l).length ↔ ∃ x ∈ l, p x := by
  simpa [length_eq_countP_add_countP, countP_eq_length_filter] using
    countP_pos_iff (p := p)

Positive Filtered List Length Criterion: $\text{length}(\text{filter}\ p\ l) > 0 \leftrightarrow \exists x \in l, p(x)$

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the length of the filtered list $\text{filter}\ p\ l$ is positive if and only if there exists an element $x \in l$ such that $p(x)$ holds. In other words, $0 < \text{length}(\text{filter}\ p\ l) \leftrightarrow \exists x \in l, p(x)$.

List.length_filter_lt_length_iff_exists theorem

{l} : (filter p l).length < l.length ↔ ∃ x ∈ l, ¬p x

Full source

@[simp]
theorem length_filter_lt_length_iff_exists {l} :
    (filter p l).length < l.length ↔ ∃ x ∈ l, ¬p x := by
  simp [length_eq_countP_add_countP p (l := l), countP_eq_length_filter]

Filtered List Length Decrease Criterion: $\text{length}(\text{filter}\ p\ l) < \text{length}(l) \leftrightarrow \exists x \in l, \neg p(x)$

Informal description

For any list $l$ and predicate $p$, the length of the filtered list $\text{filter}\ p\ l$ is strictly less than the length of $l$ if and only if there exists an element $x \in l$ such that $\neg p(x)$ holds.

List.length_filterMap_pos_iff theorem

 {xs : List α} {f : α → Option β} : 0 < (filterMap f xs).length ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b

Full source

@[simp]
theorem length_filterMap_pos_iff {xs : List α} {f : α → Option β} :
    0 < (filterMap f xs).length ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
    split
    · simp_all [ih]
    · simp_all

Non-Empty Filtered Map Condition: $\text{length}(\text{filterMap}\ f\ xs) > 0 \leftrightarrow \exists x \in xs, \exists b, f x = \text{some}\ b$

Informal description

For any list `xs` of elements of type `α` and any function `f : α → Option β`, the length of the filtered and mapped list `filterMap f xs` is positive if and only if there exists an element `x ∈ xs` and a value `b : β` such that `f x = some b`.

List.length_filterMap_lt_length_iff_exists theorem

{xs : List α} {f : α → Option β} : (filterMap f xs).length < xs.length ↔ ∃ (x : α) (_ : x ∈ xs), f x = none

Full source

@[simp]
theorem length_filterMap_lt_length_iff_exists {xs : List α} {f : α → Option β} :
    (filterMap f xs).length < xs.length ↔ ∃ (x : α) (_ : x ∈ xs), f x = none := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
    split
    · simp_all only [exists_prop, length_cons, true_or, iff_true]
      have := length_filterMap_le f xs
      omega
    · simp_all

Length Decrease Criterion for Filter-Mapped Lists: $|\text{filterMap}\ f\ xs| < |xs| \leftrightarrow \exists x \in xs, f x = \text{none}$

Informal description

For any list `xs` of elements of type `α` and any function `f : α → Option β`, the length of the filtered and mapped list `filterMap f xs` is strictly less than the length of `xs` if and only if there exists an element `x ∈ xs` such that `f x = none`.

List.getElem_eq_getElem_reverse theorem

{l : List α} {i} (h : i < l.length) : l[i] = l.reverse[l.length - 1 - i]'(by simpa using Nat.sub_one_sub_lt_of_lt h)

Full source

theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
    l[i] = l.reverse[l.length - 1 - i]'(by simpa using Nat.sub_one_sub_lt_of_lt h) := by
  rw [getElem_reverse]
  congr
  omega

Index Correspondence Between List and Its Reverse: $l[i] = l^{\text{reverse}}[|l| - 1 - i]$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number index $i$ such that $i < \text{length}(l)$, the element at position $i$ in $l$ is equal to the element at position $\text{length}(l) - 1 - i$ in the reversed list $l^{\text{reverse}}$. That is, $$ l[i] = l^{\text{reverse}}[|l| - 1 - i] $$ where $|l|$ denotes the length of $l$.

List.length_leftpad theorem

{n : Nat} {a : α} {l : List α} : (leftpad n a l).length = max n l.length

Full source

/-- The length of the List returned by `List.leftpad n a l` is equal
  to the larger of `n` and `l.length` -/
-- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
-- so the left hand side simplifies directly to `n - l.length + l.length`.
theorem length_leftpad {n : Nat} {a : α} {l : List α} :
    (leftpad n a l).length = max n l.length := by
  simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]

Length of Left-Padded List Equals Maximum of Target Length and Original Length

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the length of the list obtained by left-padding $l$ with $a$ to reach length $n$ is equal to the maximum of $n$ and the length of $l$, i.e., $$\mathrm{length}(\mathrm{leftpad}\,n\,a\,l) = \max(n, \mathrm{length}(l)).$$

List.leftpad_length abbrev

Full source

@[deprecated length_leftpad (since := "2025-02-24")]
abbrev leftpad_length := @length_leftpad

Length of Left-Padded List Equals Maximum of Target Length and Original Length

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the length of the left-padded list $\mathrm{leftpad}\,n\,a\,l$ is equal to the maximum of $n$ and the length of $l$, i.e., $$\mathrm{length}(\mathrm{leftpad}\,n\,a\,l) = \max(n, \mathrm{length}(l)).$$

List.length_rightpad theorem

{n : Nat} {a : α} {l : List α} : (rightpad n a l).length = max n l.length

Full source

theorem length_rightpad {n : Nat} {a : α} {l : List α} :
    (rightpad n a l).length = max n l.length := by
  simp [rightpad]
  omega

Length of Right-Padded List Equals Maximum of Target Length and Original Length

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the length of the right-padded list $\mathrm{rightpad}\,n\,a\,l$ is equal to the maximum of $n$ and the length of $l$, i.e., $$\mathrm{length}(\mathrm{rightpad}\,n\,a\,l) = \max(n, \mathrm{length}(l)).$$

List.mem_eraseIdx_iff_getElem theorem

{x : α} : ∀ {l} {k}, x ∈ eraseIdx l k ↔ ∃ i h, i ≠ k ∧ l[i]'h = x

Full source

theorem mem_eraseIdx_iff_getElem {x : α} :
    ∀ {l} {k}, x ∈ eraseIdx l kx ∈ eraseIdx l k ↔ ∃ i h, i ≠ k ∧ l[i]'h = x
  | [], _ => by
    simp only [eraseIdx, not_mem_nil, false_iff]
    rintro ⟨i, h, -⟩
    exact Nat.not_lt_zero _ h
  | a::l, 0 => by simp [mem_iff_getElem, Nat.succ_lt_succ_iff]
  | a::l, k+1 => by
    rw [← Nat.or_exists_add_one]
    simp [mem_eraseIdx_iff_getElem, @eq_comm _ a, succ_inj', Nat.succ_lt_succ_iff]

Membership in List After Removal at Index via Indexing

Informal description

For any element $x$ of type $\alpha$, list $l$ of type $\text{List}\ \alpha$, and natural number index $k$, the element $x$ is in the list obtained by removing the element at index $k$ from $l$ if and only if there exists an index $i$ (with proof $h$ that $i$ is a valid index) such that $i \neq k$ and the $i$-th element of $l$ is equal to $x$.

List.mem_eraseIdx_iff_getElem? theorem

{x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x

Full source

theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l kx ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x := by
  simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, exists_and_left]
  refine exists_congr fun i => and_congr_right' ?_
  constructor
  · rintro ⟨_, h⟩; exact h
  · rintro h;
    obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h
    exact ⟨h', h⟩

Membership in List After Removal via Optional Indexing

Informal description

For any element $x$ of type $\alpha$, list $l$ of type $\text{List}\,\alpha$, and natural number index $k$, the element $x$ belongs to the list obtained by removing the element at index $k$ from $l$ if and only if there exists an index $i \neq k$ such that the optional indexing operation $l[i]?$ returns $\text{some}\,x$. In symbols: $$x \in \text{eraseIdx}\,l\,k \leftrightarrow \exists i \neq k, l[i]? = \text{some}\,x$$

List.min?_eq_some_iff' theorem

{xs : List Nat} : xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b)

Full source

theorem min?_eq_some_iff' {xs : List Nat} :
    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
  min?_eq_some_iff
    (le_refl := Nat.le_refl)
    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
    (le_min_iff := fun _ _ _ => Nat.le_min)

Characterization of List Minimum: $\text{min?}\ xs = \text{some}\ a \leftrightarrow (a \in xs \land \forall b \in xs, a \leq b)$

Informal description

For a list `xs` of natural numbers, the minimum element of `xs` is `some a` if and only if `a` is an element of `xs` and `a` is less than or equal to every element in `xs`. In symbols: $$\text{min?}\ xs = \text{some}\ a \leftrightarrow (a \in xs \land \forall b \in xs, a \leq b)$$

List.min?_get_le_of_mem theorem

{l : List Nat} {a : Nat} (h : a ∈ l) : l.min?.get (isSome_min?_of_mem h) ≤ a

Full source

theorem min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    l.min?.get (isSome_min?_of_mem h) ≤ a := by
  induction l with
  | nil => simp at h
  | cons b t ih =>
    simp only [min?_cons, Option.get_some] at ih ⊢
    rcases mem_cons.1 h with (rfl|h)
    · cases t.min? with
      | none => simp
      | some b => simpa using Nat.min_le_left _ _
    · obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_min?_of_mem h)
      simp only [hq, Option.elim_some] at ih ⊢
      exact Nat.le_trans (Nat.min_le_right _ _) (ih h)

Minimum Element in List is Less Than or Equal to Any Member

Informal description

For any list $l$ of natural numbers and any element $a \in l$, the minimum element of $l$ (extracted via `get` from the `Option` result of `min?`) is less than or equal to $a$.

List.min?_getD_le_of_mem theorem

{l : List Nat} {a k : Nat} (h : a ∈ l) : l.min?.getD k ≤ a

Full source

theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : l.min?.getD k ≤ a :=
  Option.get_eq_getD _ ▸ min?_get_le_of_mem h

Minimum with Default is Bounded by List Elements

Informal description

For any list $l$ of natural numbers, any element $a \in l$, and any natural number $k$, the minimum element of $l$ (with default value $k$ if $l$ is empty) is less than or equal to $a$.

List.max?_eq_some_iff' theorem

{xs : List Nat} : xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a)

Full source

theorem max?_eq_some_iff' {xs : List Nat} :
    xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
  max?_eq_some_iff
    (le_refl := Nat.le_refl)
    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
    (max_le_iff := fun _ _ _ => Nat.max_le)

Characterization of Maximum Element in List of Natural Numbers: Existence and Dominance

Informal description

For a list of natural numbers `xs`, the maximum element of `xs` exists and equals `a` (i.e., `xs.max? = some a`) if and only if `a` is an element of `xs` and every element `b` in `xs` satisfies `b ≤ a`.

List.le_max?_get_of_mem theorem

{l : List Nat} {a : Nat} (h : a ∈ l) : a ≤ l.max?.get (isSome_max?_of_mem h)

Full source

theorem le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    a ≤ l.max?.get (isSome_max?_of_mem h) := by
  induction l with
  | nil => simp at h
  | cons b t ih =>
    simp only [max?_cons, Option.get_some] at ih ⊢
    rcases mem_cons.1 h with (rfl|h)
    · cases t.max? with
      | none => simp
      | some b => simpa using Nat.le_max_left _ _
    · obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_max?_of_mem h)
      simp only [hq, Option.elim_some] at ih ⊢
      exact Nat.le_trans (ih h) (Nat.le_max_right _ _)

Element in List is Bounded by Maximum: $a \in l \implies a \leq \text{max}(l)$

Informal description

For any list $l$ of natural numbers and any element $a \in l$, the element $a$ is less than or equal to the maximum element of $l$ (extracted from the `Option` using the proof that the maximum exists).

List.le_max?_getD_of_mem theorem

{l : List Nat} {a k : Nat} (h : a ∈ l) : a ≤ l.max?.getD k

Full source

theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
    a ≤ l.max?.getD k :=
  Option.get_eq_getD _ ▸ le_max?_get_of_mem h

Element in List is Bounded by Maximum with Default: $a \in l \implies a \leq \text{max?}(l).\text{getD}(k)$

Informal description

For any list $l$ of natural numbers, any element $a \in l$, and any natural number $k$, the element $a$ is less than or equal to the maximum element of $l$ (with a default value $k$ if $l$ is empty), i.e., $a \leq \text{max?}(l).\text{getD}(k)$.

List.minimum?_eq_some_iff' abbrev

Full source

@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'

Characterization of List Minimum: $\text{min?}\ xs = \text{some}\ a \leftrightarrow (a \in xs \land \forall b \in xs, a \leq b)$

Informal description

For a list `xs` of natural numbers, the minimum element of `xs` is `some a` if and only if `a` is an element of `xs` and `a` is less than or equal to every element in `xs`. In symbols: $$\text{min?}\ xs = \text{some}\ a \leftrightarrow (a \in xs \land \forall b \in xs, a \leq b)$$

List.minimum?_cons' abbrev

Full source

@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'

Minimum of Non-Empty List via Left Fold

Informal description

For any non-empty list $x :: \text{xs}$ of elements of type $\alpha$ with a minimum operation, the minimum of the list is equal to the left fold of the `min` operation over the list starting with the initial value $x$.

List.minimum?_getD_le_of_mem abbrev

Full source

@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem

Minimum with Default is Bounded by List Elements

Informal description

For any list $l$ of natural numbers, if an element $a$ belongs to $l$, then the minimum element of $l$ (with a default value $k$ if $l$ is empty) is less than or equal to $a$. In other words, if $a \in l$, then $\text{min?}(l).\text{getD}(k) \leq a$.

List.maximum?_eq_some_iff' abbrev

Full source

@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff'

Characterization of Maximum Element in a List of Natural Numbers

Informal description

For a list of natural numbers $xs$, the maximum element of $xs$ exists and equals $a$ (i.e., $\text{max?}(xs) = \text{some } a$) if and only if $a$ is an element of $xs$ and every element $b$ in $xs$ satisfies $b \leq a$.

List.maximum?_cons' abbrev

Full source

@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons'

Maximum of Non-Empty List via Left Fold

Informal description

For any type $\alpha$ with a maximum operation and any non-empty list $x :: xs$ of elements of type $\alpha$, the maximum value of the list (as an optional value) is equal to the left fold of the `max` operation over the list with initial value $x$, i.e., $\text{max?}(x :: xs) = \text{foldl max } x \ xs$.

List.le_maximum?_getD_of_mem abbrev

Full source

@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem

List Element Bounded by Maximum with Default: $a \in l \implies a \leq \text{max?}(l).\text{getD}(k)$

Informal description

For any list $l$ of natural numbers, any element $a \in l$, and any natural number $k$, the element $a$ is less than or equal to the maximum element of $l$ (with a default value $k$ if $l$ is empty), i.e., $a \leq \text{max?}(l).\text{getD}(k)$.