Init.Data.List.Erase

List.eraseP_nil theorem

: [].eraseP p = []

Full source

@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl

Empty List Invariance under `eraseP`

Informal description

For any predicate $p : \alpha \to \text{Bool}$, applying the `eraseP` function to the empty list `[]` results in the empty list `[]`, i.e., $\text{eraseP}\ p\ [] = []$.

List.eraseP_cons theorem

{a : α} {l : List α} : (a :: l).eraseP p = bif p a then l else a :: l.eraseP p

Full source

theorem eraseP_cons {a : α} {l : List α} :
    (a :: l).eraseP p = bif p a then l else a :: l.eraseP p := rfl

Recursive Definition of List Erasure with Predicate

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the result of applying `eraseP p` to the list $a :: l$ is equal to $l$ if the predicate $p$ holds for $a$, and otherwise it is equal to $a$ prepended to the result of applying `eraseP p` to $l$. In other words: $$(a :: l).\text{eraseP } p = \begin{cases} l & \text{if } p(a) \\ a :: (l.\text{eraseP } p) & \text{otherwise} \end{cases}$$

List.eraseP_cons_of_pos theorem

{l : List α} {p} (h : p a) : (a :: l).eraseP p = l

Full source

@[simp] theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l := by
  simp [eraseP_cons, h]

Removing First Satisfying Element from List Head

Informal description

For any list `l : List α` and predicate `p : α → Bool`, if the predicate `p` holds for the head element `a` (i.e., `p a = true`), then removing the first element satisfying `p` from the list `a :: l` results in the tail `l`. In other words, if `p a` is true, then `(a :: l).eraseP p = l`.

List.eraseP_cons_of_neg theorem

{l : List α} {p} (h : ¬p a) : (a :: l).eraseP p = a :: l.eraseP p

Full source

@[simp] theorem eraseP_cons_of_neg {l : List α} {p} (h : ¬p a) :
    (a :: l).eraseP p = a :: l.eraseP p := by simp [eraseP_cons, h]

Preservation of Non-Matching Head in List Erasure: $\neg p(a) \to (a :: l).\text{eraseP}~p = a :: (l.\text{eraseP}~p)$

Informal description

For any list `a :: l` of type `List α` and predicate `p : α → Bool`, if `¬p a` holds (i.e., the predicate `p` evaluates to `false` on `a`), then the result of `eraseP p` on the list `a :: l` is equal to `a` prepended to the result of `eraseP p` on the list `l`. In other words, $(a :: l).\text{eraseP}~p = a :: (l.\text{eraseP}~p)$ when $\neg p(a)$.

List.eraseP_of_forall_not theorem

{l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l

Full source

theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l := by
  induction l with
  | nil => rfl
  | cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]

List remains unchanged under `eraseP` when predicate is never satisfied

Informal description

For any list $l$ of elements of type $\alpha$ and predicate $p : \alpha \to \text{Bool}$, if no element $a$ in $l$ satisfies $p(a)$, then the result of removing the first element satisfying $p$ from $l$ is $l$ itself. In other words, if $\forall a \in l, \neg p(a)$, then $l.\text{eraseP}~p = l$.

List.eraseP_eq_nil_iff theorem

{xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x]

Full source

@[simp] theorem eraseP_eq_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    simp only [eraseP_cons, cond_eq_if]
    split <;> rename_i h
    · simp only [reduceCtorEq, cons.injEq, false_or]
      constructor
      · rintro rfl
        simpa
      · rintro ⟨_, _, rfl, rfl⟩
        rfl
    · simp only [reduceCtorEq, cons.injEq, false_or, false_iff, not_exists, not_and]
      rintro x h' rfl
      simp_all

Empty List Condition for Predicate-Based Removal: $\text{eraseP}\ p\ \text{xs} = [] \leftrightarrow \text{xs} = [] \lor (\exists x, p x \land \text{xs} = [x])$

Informal description

For any list `xs` of elements of type `α` and any predicate `p : α → Bool`, the result of removing the first element satisfying `p` from `xs` is the empty list if and only if either `xs` is empty or there exists an element `x` such that `p x` holds and `xs` is the singleton list `[x]`. In other words, the following equivalence holds: $$ \text{eraseP}\ p\ \text{xs} = [] \leftrightarrow \text{xs} = [] \lor (\exists x, p x \land \text{xs} = [x]) $$

List.eraseP_eq_nil abbrev

Full source

@[deprecated eraseP_eq_nil_iff (since := "2025-01-30")]
abbrev eraseP_eq_nil := @eraseP_eq_nil_iff

Empty List Condition for Predicate-Based Removal: $\text{eraseP}\ p\ \text{xs} = [] \leftrightarrow \text{xs} = [] \lor (\exists x, p x \land \text{xs} = [x])$

Informal description

For any list `xs` of elements of type `α` and any predicate `p : α → Bool`, the result of removing the first element satisfying `p` from `xs` is the empty list if and only if either `xs` is empty or there exists an element `x` such that `p x` holds and `xs` is the singleton list `[x]`. In other words, the following equivalence holds: $$ \text{eraseP}\ p\ \text{xs} = [] \leftrightarrow \text{xs} = [] \lor (\exists x, p x \land \text{xs} = [x]) $$

List.eraseP_ne_nil_iff theorem

{xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x]

Full source

theorem eraseP_ne_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p ≠ []xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by
  simp

Non-emptiness Condition for List After Predicate-Based Removal

Informal description

For any list `xs` of elements of type `α` and any predicate `p : α → Bool`, the result of removing the first element satisfying `p` from `xs` is non-empty if and only if `xs` is non-empty and for every element `x` in `xs`, if `p x` holds then `xs` is not a singleton list containing only `x`. In other words, the following equivalence holds: $$ \text{eraseP}\ p\ \text{xs} \neq [] \leftrightarrow \text{xs} \neq [] \land (\forall x, p x \to \text{xs} \neq [x]) $$

List.eraseP_ne_nil abbrev

Full source

@[deprecated eraseP_ne_nil_iff (since := "2025-01-30")]
abbrev eraseP_ne_nil := @eraseP_ne_nil_iff

Non-emptiness Implication for List After Predicate-Based Removal

Informal description

For any list `xs` of elements of type `α` and any predicate `p : α → Bool`, if the result of removing the first element satisfying `p` from `xs` is non-empty, then `xs` is non-empty and for every element `x` in `xs`, if `p x` holds then `xs` is not a singleton list containing only `x`. In other words, the following implication holds: $$ \text{eraseP}\ p\ \text{xs} \neq [] \to \text{xs} \neq [] \land (\forall x, p x \to \text{xs} \neq [x]) $$

List.exists_of_eraseP theorem

 :
  ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a),
    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂

Full source

theorem exists_of_eraseP : ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a),
    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂
  | b :: l, _, al, pa =>
    if pb : p b then
      ⟨b, [], l, forall_mem_nil _, pb, by simp [pb]⟩
    else
      match al with
      | .head .. => nomatch pb pa
      | .tail _ al =>
        let ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ := exists_of_eraseP al pa
        ⟨c, b::l₁, l₂, (forall_mem_cons ..).2 ⟨pb, h₁⟩,
          h₂, by rw [h₃, cons_append], by simp [pb, h₄]⟩

Decomposition of List After Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$ and any element $a \in l$ such that the predicate $p$ holds for $a$ (i.e., $p(a)$ is true), there exist an element $a'$, and two lists $l_1$ and $l_2$ such that: 1. For every element $b \in l_1$, the predicate $p(b)$ does not hold (i.e., $\forall b \in l_1, \neg p(b)$), 2. $p(a')$ holds, 3. The original list $l$ can be decomposed as $l = l_1 ++ a' :: l_2$ (where $++$ denotes list concatenation and $::$ denotes cons), and 4. The result of removing the first element satisfying $p$ from $l$ is $l_1 ++ l_2$. In other words, if $a$ is an element of $l$ and $p(a)$ holds, then $l$ can be split into a prefix $l_1$ where no element satisfies $p$, followed by $a'$ (which satisfies $p$) and a suffix $l_2$, such that removing the first occurrence of an element satisfying $p$ from $l$ yields $l_1$ concatenated with $l_2$.

List.exists_or_eq_self_of_eraseP theorem

 (p) (l : List α) : l.eraseP p = l ∨ ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂

Full source

theorem exists_or_eq_self_of_eraseP (p) (l : List α) :
    l.eraseP p = l ∨
    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂ :=
  if h : ∃ a ∈ l, p a then
    let ⟨_, ha, pa⟩ := h
    .inr (exists_of_eraseP ha pa)
  else
    .inl (eraseP_of_forall_not (h ⟨·, ·, ·⟩))

Decomposition or Identity of List Under Predicate-Based Removal

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, either: 1. The list remains unchanged after removing the first element satisfying $p$ (i.e., $l.\text{eraseP}~p = l$), or 2. There exists an element $a$ and two lists $l_1, l_2$ such that: - No element in $l_1$ satisfies $p$ (i.e., $\forall b \in l_1, \neg p(b)$), - $p(a)$ holds, - The original list decomposes as $l = l_1 ++ a :: l_2$, and - The result of removing the first element satisfying $p$ is $l_1 ++ l_2$.

List.length_eraseP_of_mem theorem

(al : a ∈ l) (pa : p a) : length (l.eraseP p) = length l - 1

Full source

@[simp] theorem length_eraseP_of_mem (al : a ∈ l) (pa : p a) :
    length (l.eraseP p) = length l - 1 := by
  let ⟨_, l₁, l₂, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
  rw [e₂]; simp [length_append, e₁]; rfl

Length Decrease by One After Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$, if an element $a$ is in $l$ (i.e., $a \in l$) and satisfies the predicate $p$ (i.e., $p(a)$ holds), then the length of the list obtained by removing the first occurrence of $a$ from $l$ is one less than the length of $l$, i.e., $$\text{length}(l.\text{eraseP}\ p) = \text{length}(l) - 1.$$

List.length_eraseP theorem

{l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length

Full source

theorem length_eraseP {l : List α} : (l.eraseP p).length = if l.any p then l.length - 1 else l.length := by
  split <;> rename_i h
  · simp only [any_eq_true] at h
    obtain ⟨x, m, h⟩ := h
    simp [length_eraseP_of_mem m h]
  · simp only [any_eq_true] at h
    rw [eraseP_of_forall_not]
    simp_all

Length of List After Predicate-Based Removal: $\text{length}(l.\text{eraseP}~p) = \text{length}(l) - \mathbb{1}_{\exists x \in l, p(x)}$

Informal description

For any list $l$ of elements of type $\alpha$ and predicate $p : \alpha \to \text{Bool}$, the length of the list obtained by removing the first element satisfying $p$ is equal to $\text{length}(l) - 1$ if there exists an element in $l$ satisfying $p$, and $\text{length}(l)$ otherwise. That is, $$\text{length}(l.\text{eraseP}~p) = \begin{cases} \text{length}(l) - 1 & \text{if } \exists x \in l, p(x), \\ \text{length}(l) & \text{otherwise.} \end{cases}$$

List.eraseP_sublist theorem

{l : List α} : l.eraseP p <+ l

Full source

theorem eraseP_sublist {l : List α} : l.eraseP p <+ l := by
  match exists_or_eq_self_of_eraseP p l with
  | .inl h => rw [h]; apply Sublist.refl
  | .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp

Sublist Property of Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the list obtained by removing the first element satisfying $p$ is a sublist of $l$. That is, $l.\text{eraseP}\ p <+ l$.

List.eraseP_subset theorem

{l : List α} : l.eraseP p ⊆ l

Full source

theorem eraseP_subset {l : List α} : l.eraseP p ⊆ l := eraseP_sublist.subset

Subset Property of Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the list obtained by removing the first element satisfying $p$ is a subset of $l$. That is, $\text{eraseP}\ p\ l \subseteq l$.

List.Sublist.eraseP theorem

: l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p

Full source

protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
  | .slnil => Sublist.refl _
  | .cons a s => by
    by_cases h : p a
    · simpa [h] using s.eraseP.trans eraseP_sublist
    · simpa [h] using s.eraseP.cons _
  | .cons₂ a s => by
    by_cases h : p a
    · simpa [h] using s
    · simpa [h] using s.eraseP

Sublist Preservation under Predicate-Based Removal: $l_1 <+ l_2 \to l_1.\text{eraseP}~p <+ l_2.\text{eraseP}~p$

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the list obtained by removing the first element satisfying $p$ from $l_1$ is a sublist of the list obtained by removing the first element satisfying $p$ from $l_2$ (i.e., $l_1.\text{eraseP}~p <+ l_2.\text{eraseP}~p$).

List.length_eraseP_le theorem

{l : List α} : (l.eraseP p).length ≤ l.length

Full source

theorem length_eraseP_le {l : List α} : (l.eraseP p).length ≤ l.length :=
  eraseP_sublist.length_le

Length of List After Predicate-Based Removal is Non-Increasing

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the length of the list obtained by removing the first element satisfying $p$ is less than or equal to the length of the original list $l$. That is, $|\text{eraseP}\ p\ l| \leq |l|$.

List.le_length_eraseP theorem

{l : List α} : l.length - 1 ≤ (l.eraseP p).length

Full source

theorem le_length_eraseP {l : List α} : l.length - 1 ≤ (l.eraseP p).length := by
  rw [length_eraseP]
  split <;> simp

Lower Bound on Length After Predicate-Based Removal: $\text{length}(l) - 1 \leq \text{length}(l.\text{eraseP}~p)$

Informal description

For any list $l$ of elements of type $\alpha$ and predicate $p : \alpha \to \text{Bool}$, the length of the list after removing the first element satisfying $p$ is at least the length of the original list minus one. That is, $\text{length}(l) - 1 \leq \text{length}(l.\text{eraseP}~p)$.

List.mem_of_mem_eraseP theorem

{l : List α} : a ∈ l.eraseP p → a ∈ l

Full source

theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset ·)

Membership Preservation in Predicate-Based List Removal

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, if an element $a$ is in the list obtained by removing the first element satisfying $p$, then $a$ was in the original list $l$. That is, $a \in \text{eraseP}\ p\ l \to a \in l$.

List.mem_eraseP_of_neg theorem

{l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l

Full source

@[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP pa ∈ l.eraseP p ↔ a ∈ l := by
  refine ⟨mem_of_mem_eraseP, fun al => ?_⟩
  match exists_or_eq_self_of_eraseP p l with
  | .inl h => rw [h]; assumption
  | .inr ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ =>
    rw [h₄]; rw [h₃] at al
    have : a ≠ c := fun h => (h ▸ pa).elim h₂
    simp [this] at al; simp [al]

Membership Preservation in Predicate-Based List Removal for Non-Satisfying Elements: $a \in \text{eraseP}\ p\ l \leftrightarrow a \in l$ when $\neg p(a)$

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, if an element $a$ does not satisfy $p$ (i.e., $\neg p(a)$ holds), then $a$ is in the list obtained by removing the first element satisfying $p$ if and only if $a$ is in the original list $l$. That is, $$a \in \text{eraseP}\ p\ l \leftrightarrow a \in l.$$

List.eraseP_eq_self_iff theorem

{p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬p a

Full source

@[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by
  rw [← Sublist.length_eq eraseP_sublist, length_eraseP]
  split <;> rename_i h
  · simp only [any_eq_true, length_eq_zero_iff] at h
    constructor
    · intro; simp_all [Nat.sub_one_eq_self]
    · intro; obtain ⟨x, m, h⟩ := h; simp_all
  · simp_all

Equality Condition for Predicate-Based List Removal: $\text{eraseP}\ p\ l = l \leftrightarrow \forall a \in l, \neg p(a)$

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the list obtained by removing the first element satisfying $p$ is equal to $l$ if and only if no element in $l$ satisfies $p$. That is, $$l.\text{eraseP}\ p = l \leftrightarrow \forall a \in l, \neg p(a).$$

List.eraseP_map theorem

{f : β → α} : ∀ {l : List β}, (map f l).eraseP p = map f (l.eraseP (p ∘ f))

Full source

theorem eraseP_map {f : β → α} : ∀ {l : List β}, (map f l).eraseP p = map f (l.eraseP (p ∘ f))
  | [] => rfl
  | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map, eraseP_cons_of_pos]

Commutativity of List Mapping and Predicate-Based Erasure: $\text{map}\ f \circ \text{eraseP}\ p = \text{eraseP}\ (p \circ f) \circ \text{map}\ f$

Informal description

For any function $f : \beta \to \alpha$ and any list $l$ of type $\text{List}\ \beta$, the result of applying $\text{eraseP}\ p$ to the mapped list $\text{map}\ f\ l$ is equal to mapping $f$ over the list obtained by applying $\text{eraseP}\ (p \circ f)$ to $l$. In other words, $$(\text{map}\ f\ l).\text{eraseP}\ p = \text{map}\ f\ (l.\text{eraseP}\ (p \circ f)).$$

List.eraseP_filterMap theorem

 {f : α → Option β} :
  ∀ {l : List α},
    (filterMap f l).eraseP p =
      filterMap f
        (l.eraseP
          (fun x =>
            match f x with
            | some y => p y
            | none => false))

Full source

theorem eraseP_filterMap {f : α → Option β} : ∀ {l : List α},
    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
  | [] => rfl
  | a::l => by
    rw [filterMap_cons, eraseP_cons]
    split <;> rename_i h
    · simp [h, eraseP_filterMap]
    · rename_i b
      rw [h, eraseP_cons]
      by_cases w : p b
      · simp [w]
      · simp only [w, cond_false]
        rw [filterMap_cons_some h, eraseP_filterMap]

Commutation of `eraseP` and `filterMap` with Predicate Adaptation

Informal description

For any function $f : \alpha \to \text{Option } \beta$ and any list $l$ of elements of type $\alpha$, the result of applying `eraseP p` to the list obtained by `filterMap f l` is equal to applying `filterMap f` to the list obtained by applying `eraseP` to $l$ with the predicate that checks $p(y)$ when $f(x) = \text{some } y$ and returns `false` otherwise. In other words: $$(\text{filterMap } f\ l).\text{eraseP } p = \text{filterMap } f\ (l.\text{eraseP } (\lambda x.\, \text{match } f(x) \text{ with } | \text{some } y \Rightarrow p(y) | \text{none } \Rightarrow \text{false}))$$

List.eraseP_filter theorem

{f : α → Bool} {l : List α} : (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x))

Full source

theorem eraseP_filter {f : α → Bool} {l : List α} :
    (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x)) := by
  rw [← filterMap_eq_filter, eraseP_filterMap]
  congr
  ext x
  simp only [Option.guard]
  split <;> split at * <;> simp_all

Commutation of `eraseP` and `filter` with Combined Predicate

Informal description

For any predicate $f : \alpha \to \text{Bool}$ and any list $l$ of elements of type $\alpha$, the result of applying $\text{eraseP } p$ to the filtered list $\text{filter } f\ l$ is equal to filtering $f$ over the list obtained by applying $\text{eraseP}$ to $l$ with the combined predicate $\lambda x.\, p(x) \land f(x)$. In other words: $$(\text{filter } f\ l).\text{eraseP } p = \text{filter } f\ (l.\text{eraseP } (\lambda x.\, p(x) \land f(x)))$$

List.eraseP_append_left theorem

{a : α} (pa : p a) : ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂

Full source

theorem eraseP_append_left {a : α} (pa : p a) :
    ∀ {l₁ : List α} l₂, a ∈ l₁ → (l₁++l₂).eraseP p = l₁.eraseP p ++ l₂
  | x :: xs, l₂, h => by
    by_cases h' : p x <;> simp [h']
    rw [eraseP_append_left pa l₂ ((mem_cons.1 h).resolve_left (mt _ h'))]
    intro | rfl => exact pa

Concatenation Preservation under `eraseP` with Matching Element in Left List

Informal description

For any element $a$ of type $\alpha$ satisfying a predicate $p$ (i.e., $p(a)$ holds), and for any lists $l₁$ and $l₂$ of elements of type $\alpha$ such that $a \in l₁$, the result of applying `eraseP p` to the concatenated list $l₁ ++ l₂$ is equal to the concatenation of `eraseP p` applied to $l₁$ with $l₂$. In other words, $(l₁ ++ l₂).\text{eraseP}~p = (l₁.\text{eraseP}~p) ++ l₂$ when $p(a)$ and $a \in l₁$.

List.eraseP_append_right theorem

: ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁ ++ l₂) = l₁ ++ l₂.eraseP p

Full source

theorem eraseP_append_right :
    ∀ {l₁ : List α} l₂, (∀ b ∈ l₁, ¬p b) → eraseP p (l₁++l₂) = l₁ ++ l₂.eraseP p
  | [],     _, _ => rfl
  | _ :: _, _, h => by
    simp [(forall_mem_cons.1 h).1, eraseP_append_right _ (forall_mem_cons.1 h).2]

Preservation of Concatenation under `eraseP` when Left List Has No Matching Elements

Informal description

For any lists $l₁$ and $l₂$ of elements of type $\alpha$, if no element $b$ in $l₁$ satisfies the predicate $p$, then the result of applying `eraseP p` to the concatenated list $l₁ ++ l₂$ is equal to the concatenation of $l₁$ with the result of applying `eraseP p` to $l₂$. In other words, if $\forall b \in l₁, \neg p(b)$, then $(l₁ ++ l₂).\text{eraseP}~p = l₁ ++ (l₂.\text{eraseP}~p)$.

List.eraseP_append theorem

{l₁ l₂ : List α} : (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p

Full source

theorem eraseP_append {l₁ l₂ : List α} :
    (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p := by
  split <;> rename_i h
  · simp only [any_eq_true] at h
    obtain ⟨x, m, h⟩ := h
    rw [eraseP_append_left h _ m]
  · simp only [any_eq_true] at h
    rw [eraseP_append_right _]
    simp_all

Conditional Distribution of `eraseP` over List Concatenation

Informal description

For any lists $l₁$ and $l₂$ of elements of type $\alpha$, the result of applying `eraseP p` to the concatenated list $l₁ ++ l₂$ is equal to: - $l₁.\text{eraseP}~p ++ l₂$ if there exists an element in $l₁$ satisfying the predicate $p$ (i.e., $\text{any}~p~l₁$ is true), - $l₁ ++ l₂.\text{eraseP}~p$ otherwise. In other words, $(l₁ ++ l₂).\text{eraseP}~p = \text{if}~(\text{any}~p~l₁)~\text{then}~(l₁.\text{eraseP}~p ++ l₂)~\text{else}~(l₁ ++ l₂.\text{eraseP}~p)$.

List.eraseP_replicate theorem

{n : Nat} {a : α} {p : α → Bool} : (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a

Full source

theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
    (replicate n a).eraseP p = if p a then replicate (n - 1) a else replicate n a := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [replicate_succ, eraseP_cons]
    split <;> simp [*]

Behavior of $\mathrm{eraseP}$ on Replicated Lists: $\mathrm{eraseP}\ p\ (a^n) = \mathrm{if}\ p(a)\ \mathrm{then}\ a^{n-1}\ \mathrm{else}\ a^n$

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and predicate $p : \alpha \to \mathtt{Bool}$, the result of applying $\mathrm{eraseP}$ to a list of $n$ copies of $a$ is: - A list of $n-1$ copies of $a$ if $p(a)$ is true, - The original list of $n$ copies of $a$ otherwise. In other words, $\mathrm{eraseP}\ p\ (\mathrm{replicate}\ n\ a) = \mathrm{if}\ p(a)\ \mathrm{then}\ \mathrm{replicate}\ (n-1)\ a\ \mathrm{else}\ \mathrm{replicate}\ n\ a$.

List.eraseP_replicate_of_pos theorem

{n : Nat} {a : α} (h : p a) : (replicate n a).eraseP p = replicate (n - 1) a

Full source

@[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
    (replicate n a).eraseP p = replicate (n - 1) a := by
  cases n <;> simp [replicate_succ, h]

Effect of `eraseP` on Replicated List When Predicate Holds: $(replicate\ n\ a).eraseP\ p = replicate\ (n-1)\ a$

Informal description

For any natural number $n$ and element $a$ of type $\alpha$, if the predicate $p$ holds for $a$ (i.e., $p(a)$ is true), then removing the first occurrence of an element satisfying $p$ from the list consisting of $n$ copies of $a$ results in a list with $n-1$ copies of $a$. In other words, $(\text{replicate}\ n\ a).\text{eraseP}\ p = \text{replicate}\ (n-1)\ a$.

List.eraseP_replicate_of_neg theorem

{n : Nat} {a : α} (h : ¬p a) : (replicate n a).eraseP p = replicate n a

Full source

@[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
    (replicate n a).eraseP p = replicate n a := by
  rw [eraseP_of_forall_not (by simp_all)]

Invariance of Replicated List under `eraseP` when Predicate Fails

Informal description

For any natural number $n$ and element $a$ of type $\alpha$, if the predicate $p$ does not hold for $a$ (i.e., $\neg p(a)$), then removing the first occurrence of an element satisfying $p$ from the list consisting of $n$ copies of $a$ leaves the list unchanged. In other words, $(\text{replicate}\ n\ a).\text{eraseP}\ p = \text{replicate}\ n\ a$.

List.IsPrefix.eraseP theorem

(h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p

Full source

protected theorem IsPrefix.eraseP (h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p := by
  rw [IsPrefix] at h
  obtain ⟨t, rfl⟩ := h
  rw [eraseP_append]
  split
  · exact prefix_append (eraseP p l₁) t
  · rw [eraseP_of_forall_not (by simp_all)]
    exact prefix_append l₁ (eraseP p t)

Preservation of Prefix Relation under `eraseP` Operation

Informal description

For any lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = l_1 ++ t$), then the result of removing the first element satisfying predicate $p$ from $l_1$ is a prefix of the result of removing the first element satisfying $p$ from $l_2$. In other words, if $l_1 <+: l_2$, then $l_1.\text{eraseP}~p <+: l_2.\text{eraseP}~p$.

List.eraseP_eq_iff theorem

 {p} {l : List α} :
  l.eraseP p = l' ↔ ((∀ a ∈ l, ¬p a) ∧ l = l') ∨ ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Full source

theorem eraseP_eq_iff {p} {l : List α} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
  cases exists_or_eq_self_of_eraseP p l with
  | inl h =>
    constructor
    · intro h'
      left
      exact ⟨eraseP_eq_self_iff.1 h, by simp_all⟩
    · rintro (⟨-, rfl⟩ | ⟨a, l₁, l₂, h₁, h₂, rfl, rfl⟩)
      · assumption
      · rw [eraseP_append_right _ h₁, eraseP_cons_of_pos h₂]
  | inr h =>
    obtain ⟨a, l₁, l₂, h₁, h₂, w₁, w₂⟩ := h
    rw [w₂]
    subst w₁
    constructor
    · rintro rfl
      right
      refine ⟨a, l₁, l₂, ?_⟩
      simp_all
    · rintro (h | h)
      · simp_all
      · obtain ⟨a', l₁', l₂', h₁', h₂', h, rfl⟩ := h
        have p : l₁ = l₁' := by
          have q : l₁ = takeWhile (fun x => !p x) (l₁ ++ a :: l₂) := by
            rw [takeWhile_append_of_pos (by simp_all),
              takeWhile_cons_of_neg (by simp [h₂]), append_nil]
          have q' : l₁' = takeWhile (fun x => !p x) (l₁' ++ a' :: l₂') := by
            rw [takeWhile_append_of_pos (by simpa using h₁'),
              takeWhile_cons_of_neg (by simp [h₂']), append_nil]
          simp [h] at q
          rw [q', q]
        subst p
        simp_all

Characterization of List Equality under Predicate-Based Removal: $l.\text{eraseP}~p = l'$

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any lists $l, l'$ of elements of type $\alpha$, the equality $l.\text{eraseP}~p = l'$ holds if and only if one of the following conditions is satisfied: 1. No element in $l$ satisfies $p$ (i.e., $\forall a \in l, \neg p(a)$) and $l = l'$, or 2. There exists an element $a$ and lists $l_1, l_2$ such that: - No element in $l_1$ satisfies $p$ (i.e., $\forall b \in l_1, \neg p(b)$), - $p(a)$ holds, - The original list decomposes as $l = l_1 ++ a :: l_2$, and - The resulting list is $l' = l_1 ++ l_2$.

List.Pairwise.eraseP theorem

(q) : Pairwise p l → Pairwise p (l.eraseP q)

Full source

theorem Pairwise.eraseP (q) : Pairwise p l → Pairwise p (l.eraseP q) :=
  Pairwise.sublist <| eraseP_sublist

Preservation of Pairwise Relation under Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$ and predicates $p, q : \alpha \to \text{Bool}$, if the relation $p$ holds pairwise for all elements in $l$, then $p$ also holds pairwise for the list obtained by removing the first element satisfying $q$ from $l$. In other words, if $\text{Pairwise}\ p\ l$, then $\text{Pairwise}\ p\ (l.\text{eraseP}\ q)$.

List.Nodup.eraseP theorem

(p) : Nodup l → Nodup (l.eraseP p)

Full source

theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
  Pairwise.eraseP p

Preservation of No-Duplicates Property under Predicate-Based Removal

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, if $l$ has no duplicate elements, then the list obtained by removing the first element of $l$ satisfying $p$ also has no duplicate elements. In other words, if $\text{Nodup}\ l$, then $\text{Nodup}\ (l.\text{eraseP}\ p)$.

List.eraseP_comm theorem

{l : List α} (h : ∀ a ∈ l, ¬p a ∨ ¬q a) : (l.eraseP p).eraseP q = (l.eraseP q).eraseP p

Full source

theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
    (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by
  induction l with
  | nil => rfl
  | cons a l ih =>
    simp only [eraseP_cons]
    by_cases h₁ : p a
    · by_cases h₂ : q a
      · simp_all
      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
    · by_cases h₂ : q a
      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
      · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]

Commutativity of List Erasure under Disjoint Predicates

Informal description

For any list $l$ of elements of type $\alpha$ and predicates $p, q : \alpha \to \text{Bool}$, if for every element $a \in l$ either $\neg p(a)$ or $\neg q(a)$ holds, then the order of erasing elements using $p$ and $q$ does not matter. That is, $(l.\text{eraseP}~p).\text{eraseP}~q = (l.\text{eraseP}~q).\text{eraseP}~p$.

List.head_eraseP_mem theorem

{xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs

Full source

theorem head_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).head h ∈ xs :=
  eraseP_sublist.head_mem h

Head of Erased List Remains in Original List

Informal description

For any non-empty list $xs$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the head element of the list obtained by removing the first element satisfying $p$ is still an element of the original list $xs$.

List.getLast_eraseP_mem theorem

{xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs

Full source

theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).getLast h ∈ xs :=
  eraseP_sublist.getLast_mem h

Last Element of Erased List Remains in Original List

Informal description

For any non-empty list $xs$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the last element of the list obtained by removing the first element satisfying $p$ is still an element of the original list $xs$.

List.eraseP_eq_eraseIdx theorem

 {xs : List α} {p : α → Bool} :
  xs.eraseP p =
    match xs.findIdx? p with
    | none => xs
    | some i => xs.eraseIdx i

Full source

theorem eraseP_eq_eraseIdx {xs : List α} {p : α → Bool} :
    xs.eraseP p = match xs.findIdx? p with
    | none => xs
    | somesome i => xs.eraseIdx i := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    rw [eraseP_cons, findIdx?_cons]
    by_cases h : p x
    · simp [h]
    · simp only [h]
      rw [ih]
      split <;> simp [*]

Equivalence of Predicate-Based and Index-Based List Erasure: $\text{eraseP}~p~xs = \text{eraseIdx}~xs~i$ when $i$ is the first index satisfying $p$

Informal description

For any list $xs$ of elements of type $\alpha$ and any predicate $p : \alpha \to \text{Bool}$, the result of removing the first element satisfying $p$ from $xs$ (i.e., $\text{eraseP}~p~xs$) is equal to: - $xs$ if no element satisfies $p$ (i.e., $\text{findIdx?}~p~xs = \text{none}$), or - the result of removing the element at the first index where $p$ holds (i.e., $\text{eraseIdx}~xs~i$) if $\text{findIdx?}~p~xs = \text{some}~i$. In other words: $$ \text{eraseP}~p~xs = \begin{cases} xs & \text{if } \text{findIdx?}~p~xs = \text{none} \\ \text{eraseIdx}~xs~i & \text{if } \text{findIdx?}~p~xs = \text{some}~i \end{cases} $$

List.erase_cons_head theorem

[LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l

Full source

@[simp] theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l := by
  simp [erase_cons]

Removing Head Element from List: $\text{erase}(a :: l, a) = l$

Informal description

For any type $\alpha$ with a lawful boolean equality relation and any element $a \in \alpha$ and list $l$ of elements of $\alpha$, removing the first occurrence of $a$ from the list $a :: l$ results in $l$. In other words, $\text{erase}(a :: l, a) = l$.

List.erase_cons_tail theorem

{a b : α} {l : List α} (h : ¬(b == a)) : (b :: l).erase a = b :: l.erase a

Full source

@[simp] theorem erase_cons_tail {a b : α} {l : List α} (h : ¬(b == a)) :
    (b :: l).erase a = b :: l.erase a := by simp only [erase_cons, if_neg h]

Tail Preservation in List Erasure: $\text{erase}~(b :: l)~a = b :: \text{erase}~l~a$ when $b \neq a$

Informal description

For any type $\alpha$ with a boolean equality relation, and elements $a, b \in \alpha$ and a list $l$ of elements of type $\alpha$, if $b$ is not equal to $a$ (i.e., $b == a$ is false), then removing the first occurrence of $a$ from the list $b :: l$ results in $b$ followed by the list obtained by removing the first occurrence of $a$ from $l$. In mathematical notation: $$\text{erase}~(b :: l)~a = b :: \text{erase}~l~a \quad \text{when } b \neq a$$

List.erase_of_not_mem theorem

[LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l

Full source

theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l → l.erase a = l
  | [], _ => rfl
  | b :: l, h => by
    rw [mem_cons, not_or] at h
    simp only [erase_cons, if_neg, erase_of_not_mem h.2, beq_iff_eq, Ne.symm h.1, not_false_eq_true]

List remains unchanged when erasing a non-member element

Informal description

For any type $\alpha$ with a lawful boolean equality relation, and any element $a \in \alpha$, if $a$ does not belong to a list $l$ (i.e., $a \notin l$), then removing $a$ from $l$ leaves the list unchanged, i.e., $\text{erase}~l~a = l$.

List.erase_eq_eraseP' theorem

(a : α) (l : List α) : l.erase a = l.eraseP (· == a)

Full source

theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a) := by
  induction l
  · simp
  · next b t ih =>
    rw [erase_cons, eraseP_cons, ih]
    if h : b == a then simp [h] else simp [h]

Equivalence of List Erasure and Predicate-Based Erasure: $\text{erase}~l~a = \text{eraseP}~(\lambda x, x == a)~l$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the result of removing the first occurrence of $a$ from $l$ is equal to the result of removing the first element in $l$ that satisfies the predicate $\lambda x, x == a$. In mathematical notation: $$\text{erase}~l~a = \text{eraseP}~(\lambda x, x == a)~l$$

List.erase_eq_eraseP theorem

[LawfulBEq α] (a : α) : ∀ (l : List α), l.erase a = l.eraseP (a == ·)

Full source

theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ (l : List α), l.erase a = l.eraseP (a == ·)
  | [] => rfl
  | b :: l => by
    if h : a = b then simp [h] else simp [h, Ne.symm h, erase_eq_eraseP (l := l)]

Equivalence of List Erasure and Predicate-Based Erasure: $\text{erase}~l~a = \text{eraseP}~(a == \cdot)~l$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any list $l$ of elements of type $\alpha$, the result of removing the first occurrence of $a$ from $l$ is equal to the result of removing the first element in $l$ that is equal to $a$ (i.e., satisfies the predicate $\lambda x, a == x$). In mathematical notation: $$\text{erase}~l~a = \text{eraseP}~(a == \cdot)~l$$

List.erase_eq_nil_iff theorem

[LawfulBEq α] {xs : List α} {a : α} : xs.erase a = [] ↔ xs = [] ∨ xs = [a]

Full source

@[simp] theorem erase_eq_nil_iff [LawfulBEq α] {xs : List α} {a : α} :
    xs.erase a = [] ↔ xs = [] ∨ xs = [a] := by
  rw [erase_eq_eraseP]
  simp

Empty List After Erasure: $\text{erase}~xs~a = [] \leftrightarrow xs = [] \lor xs = [a]$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $xs$ of elements of type $\alpha$, and any element $a \in \alpha$, the result of removing the first occurrence of $a$ from $xs$ is the empty list if and only if $xs$ is either empty or contains only the element $a$. In mathematical notation: $$\text{erase}~xs~a = [] \leftrightarrow xs = [] \lor xs = [a]$$

List.erase_eq_nil abbrev

Full source

@[deprecated erase_eq_nil_iff (since := "2025-01-30")]
abbrev erase_eq_nil := @erase_eq_nil_iff

Empty List After Erasure: $\text{erase}~xs~a = [] \leftrightarrow xs = [] \lor xs = [a]$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $xs$ of elements of type $\alpha$, and any element $a \in \alpha$, the result of removing the first occurrence of $a$ from $xs$ is the empty list if and only if $xs$ is either empty or contains only the element $a$. In mathematical notation: $$\text{erase}~xs~a = [] \leftrightarrow xs = [] \lor xs = [a]$$

List.erase_ne_nil_iff theorem

[LawfulBEq α] {xs : List α} {a : α} : xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a]

Full source

theorem erase_ne_nil_iff [LawfulBEq α] {xs : List α} {a : α} :
    xs.erase a ≠ []xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a] := by
  rw [erase_eq_eraseP]
  simp

Non-emptiness of List After Erasure: $\text{erase}~xs~a \neq [] \leftrightarrow xs \neq [] \land xs \neq [a]$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $xs$ of elements of type $\alpha$, and any element $a \in \alpha$, the list obtained by removing the first occurrence of $a$ from $xs$ is non-empty if and only if $xs$ is non-empty and $xs$ is not equal to the singleton list $[a]$. In mathematical notation: $$ \text{erase}~xs~a \neq [] \leftrightarrow xs \neq [] \land xs \neq [a] $$

List.erase_ne_nil abbrev

Full source

@[deprecated erase_ne_nil_iff (since := "2025-01-30")]
abbrev erase_ne_nil := @erase_ne_nil_iff

Implication of Non-emptiness After List Erasure: $\text{erase}~xs~a \neq [] \to xs \neq [] \land xs \neq [a]$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $xs$ of elements of type $\alpha$, and any element $a \in \alpha$, if the list obtained by removing the first occurrence of $a$ from $xs$ is non-empty, then $xs$ is non-empty and $xs$ is not equal to the singleton list $[a]$. In mathematical notation: $$ \text{erase}~xs~a \neq [] \to xs \neq [] \land xs \neq [a] $$

List.exists_erase_eq theorem

 [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂

Full source

theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
    ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by
  let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)
  rw [erase_eq_eraseP]; exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩

List Decomposition Under Element Removal: $l = l_1 ++ a :: l_2 \implies \text{erase}~l~a = l_1 ++ l_2$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any list $l$ of elements of type $\alpha$ containing $a$, there exist two lists $l_1$ and $l_2$ such that: 1. $a$ does not appear in $l_1$, 2. The original list $l$ can be decomposed as $l = l_1 ++ a :: l_2$ (where $++$ denotes list concatenation and $::$ denotes cons), and 3. The result of removing the first occurrence of $a$ from $l$ is $l_1 ++ l_2$.

List.length_erase_of_mem theorem

[LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : length (l.erase a) = length l - 1

Full source

@[simp] theorem length_erase_of_mem [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
    length (l.erase a) = length l - 1 := by
  rw [erase_eq_eraseP]; exact length_eraseP_of_mem h (beq_self_eq_true a)

Length Decrease by One After Element Removal in List

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any list $l$ of elements of type $\alpha$, if $a$ is a member of $l$, then the length of the list obtained by removing the first occurrence of $a$ from $l$ is one less than the length of $l$, i.e., $$\text{length}(l \setminus a) = \text{length}(l) - 1.$$

List.length_erase theorem

[LawfulBEq α] {a : α} {l : List α} : length (l.erase a) = if a ∈ l then length l - 1 else length l

Full source

theorem length_erase [LawfulBEq α] {a : α} {l : List α} :
    length (l.erase a) = if a ∈ l then length l - 1 else length l := by
  rw [erase_eq_eraseP, length_eraseP]
  split <;> split <;> simp_all

Length of List After Element Removal: $\text{length}(l.\text{erase}~a) = \text{length}(l) - \mathbb{1}_{a \in l}$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any list $l$ of elements of type $\alpha$, the length of the list obtained by removing the first occurrence of $a$ from $l$ is equal to $\text{length}(l) - 1$ if $a$ is in $l$, and $\text{length}(l)$ otherwise. That is, $$\text{length}(l.\text{erase}~a) = \begin{cases} \text{length}(l) - 1 & \text{if } a \in l, \\ \text{length}(l) & \text{otherwise.} \end{cases}$$

List.erase_sublist theorem

{a : α} {l : List α} : l.erase a <+ l

Full source

theorem erase_sublist {a : α} {l : List α} : l.erase a <+ l :=
  erase_eq_eraseP' a l ▸ eraseP_sublist ..

Sublist Property of List Erasure: $l \setminus a <+ l$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list obtained by removing the first occurrence of $a$ from $l$ is a sublist of $l$. In other words, $l \setminus a <+ l$.

List.erase_subset theorem

{a : α} {l : List α} : l.erase a ⊆ l

Full source

theorem erase_subset {a : α} {l : List α} : l.erase a ⊆ l := erase_sublist.subset

Subset Property of List Erasure: $l \setminus a \subseteq l$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list obtained by removing the first occurrence of $a$ from $l$ is a subset of $l$. In other words, $l \setminus a \subseteq l$.

List.Sublist.erase theorem

(a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a

Full source

theorem Sublist.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₁.erase a <+ l₂.erase a := by
  simp only [erase_eq_eraseP']; exact h.eraseP

Sublist Preservation under Element Removal: $l_1 <+ l_2 \to l_1 \setminus a <+ l_2 \setminus a$

Informal description

For any element $a$ of type $\alpha$ and any lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the list obtained by removing the first occurrence of $a$ from $l_1$ is a sublist of the list obtained by removing the first occurrence of $a$ from $l_2$ (i.e., $l_1 \setminus a <+ l_2 \setminus a$).

List.IsPrefix.erase theorem

(a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a

Full source

theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁.erase a <+: l₂.erase a := by
  simp only [erase_eq_eraseP']; exact h.eraseP

Prefix Preservation under Element Removal: $\text{erase}~l_1~a <+: \text{erase}~l_2~a$ when $l_1 <+: l_2$

Informal description

For any element $a$ of type $\alpha$ and any lists $l_1, l_2$ of elements of type $\alpha$, if $l_1$ is a prefix of $l_2$ (i.e., there exists a list $t$ such that $l_2 = l_1 ++ t$), then the result of removing the first occurrence of $a$ from $l_1$ is a prefix of the result of removing the first occurrence of $a$ from $l_2$. In mathematical notation: $$l_1 <+: l_2 \implies \text{erase}~l_1~a <+: \text{erase}~l_2~a$$

List.length_erase_le theorem

{a : α} {l : List α} : (l.erase a).length ≤ l.length

Full source

theorem length_erase_le {a : α} {l : List α} : (l.erase a).length ≤ l.length :=
  erase_sublist.length_le

Monotonicity of List Length under Erasure: $|\text{erase}(l, a)| \leq |l|$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the length of the list obtained by removing the first occurrence of $a$ from $l$ is less than or equal to the length of $l$. In mathematical notation: $$|\text{erase}(l, a)| \leq |l|$$

List.le_length_erase theorem

[LawfulBEq α] {a : α} {l : List α} : l.length - 1 ≤ (l.erase a).length

Full source

theorem le_length_erase [LawfulBEq α] {a : α} {l : List α} : l.length - 1 ≤ (l.erase a).length := by
  rw [length_erase]
  split <;> simp

Lower Bound on List Length After Element Removal: $\text{length}(l) - 1 \leq \text{length}(l.\text{erase}~a)$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any list $l$ of elements of type $\alpha$, the length of $l$ minus one is less than or equal to the length of the list obtained by removing the first occurrence of $a$ from $l$. That is, $$\text{length}(l) - 1 \leq \text{length}(l.\text{erase}~a).$$

List.mem_of_mem_erase theorem

{a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l

Full source

theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset h

Membership Preservation under List Erasure: $a \in l \setminus b \to a \in l$

Informal description

For any elements $a, b$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if $a$ is an element of the list obtained by removing the first occurrence of $b$ from $l$, then $a$ is also an element of $l$. In other words: $$ a \in \text{erase}(l, b) \implies a \in l $$

List.mem_erase_of_ne theorem

[LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) : a ∈ l.erase b ↔ a ∈ l

Full source

@[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
    a ∈ l.erase ba ∈ l.erase b ↔ a ∈ l :=
  erase_eq_eraseP b l ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)

Membership Preservation under List Erasure for Distinct Elements: $a \in l \setminus b \leftrightarrow a \in l$ when $a \neq b$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any distinct elements $a$ and $b$ of type $\alpha$ (i.e., $a \neq b$), and any list $l$ of elements of type $\alpha$, the element $a$ belongs to the list obtained by removing the first occurrence of $b$ from $l$ if and only if $a$ belongs to $l$. In mathematical notation: $$ a \in \text{erase}(l, b) \leftrightarrow a \in l $$

List.erase_eq_self_iff theorem

[LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l

Full source

@[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l := by
  rw [erase_eq_eraseP', eraseP_eq_self_iff]
  simp [forall_mem_ne']

Erasure Preserves List Identity if and only if Element is Absent

Informal description

For any list $l$ of elements of type $\alpha$ with a lawful boolean equality relation, the list obtained by removing the first occurrence of $a$ from $l$ is equal to $l$ if and only if $a$ does not belong to $l$. In other words: $$ \text{erase}\ l\ a = l \leftrightarrow a \notin l $$

List.erase_filter theorem

[LawfulBEq α] {f : α → Bool} {l : List α} : (filter f l).erase a = filter f (l.erase a)

Full source

theorem erase_filter [LawfulBEq α] {f : α → Bool} {l : List α} :
    (filter f l).erase a = filter f (l.erase a) := by
  induction l with
  | nil => rfl
  | cons x xs ih =>
    by_cases h : a = x
    · rw [erase_cons]
      simp only [h, beq_self_eq_true, ↓reduceIte]
      rw [filter_cons]
      split
      · rw [erase_cons_head]
      · rw [erase_of_not_mem]
        simp_all [mem_filter]
    · rw [erase_cons_tail (by simpa using Ne.symm h), filter_cons, filter_cons]
      split
      · rw [erase_cons_tail (by simpa using Ne.symm h), ih]
      · rw [ih]

Commutativity of Erasure and Filtering: $\text{erase} \circ \text{filter}\ f = \text{filter}\ f \circ \text{erase}$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any predicate $f : \alpha \to \text{Bool}$, and any list $l$ of elements of type $\alpha$, removing the first occurrence of $a$ from the filtered list $\text{filter}\ f\ l$ is equal to filtering $f$ after removing the first occurrence of $a$ from $l$. In other words: $$ \text{erase}\ (\text{filter}\ f\ l)\ a = \text{filter}\ f\ (\text{erase}\ l\ a) $$

List.erase_append_left theorem

[LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) : (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

Full source

theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁) :
    (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ := by
  simp [erase_eq_eraseP]; exact eraseP_append_left (beq_self_eq_true a) l₂ h

Erasure Commutes with Left Concatenation: $\text{erase}~(l_1 ++ l_2)~a = (\text{erase}~l_1~a) ++ l_2$ when $a \in l_1$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $l_1$ of elements of type $\alpha$ containing an element $a$, and any list $l_2$ of elements of type $\alpha$, removing the first occurrence of $a$ from the concatenated list $l_1 ++ l_2$ is equal to the concatenation of $l_1$ with $a$ removed and $l_2$. In other words: $$ \text{erase}~(l_1 ++ l_2)~a = (\text{erase}~l_1~a) ++ l_2 $$

List.erase_append_right theorem

 [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) : (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a)

Full source

theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) :
    (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by
  rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
  intros b h' h''; rw [eq_of_beq h''] at h; exact h h'

Right Concatenation Preservation under Erasure: $(l₁ ++ l₂).\text{erase}~a = l₁ ++ (l₂.\text{erase}~a)$ when $a \notin l₁$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any lists $l₁, l₂$ of elements of type $\alpha$, if $a$ does not belong to $l₁$, then removing the first occurrence of $a$ from the concatenated list $l₁ ++ l₂$ is equal to concatenating $l₁$ with the result of removing the first occurrence of $a$ from $l₂$. In other words: $$ (l₁ ++ l₂).\text{erase}~a = l₁ ++ (l₂.\text{erase}~a) $$

List.erase_append theorem

 [LawfulBEq α] {a : α} {l₁ l₂ : List α} : (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

Full source

theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
    (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a := by
  simp [erase_eq_eraseP, eraseP_append]

Conditional Distribution of List Erasure over Concatenation: $(l_1 ++ l_2).\text{erase}~a = \text{if } a \in l_1 \text{ then } l_1.\text{erase}~a ++ l_2 \text{ else } l_1 ++ l_2.\text{erase}~a$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any element $a \in \alpha$, and any lists $l_1, l_2$ of elements of type $\alpha$, the result of removing the first occurrence of $a$ from the concatenated list $l_1 ++ l_2$ is: - $l_1.\text{erase}~a ++ l_2$ if $a$ appears in $l_1$, - $l_1 ++ l_2.\text{erase}~a$ otherwise. In mathematical notation: $$(l_1 ++ l_2).\text{erase}~a = \begin{cases} l_1.\text{erase}~a ++ l_2 & \text{if } a \in l_1 \\ l_1 ++ l_2.\text{erase}~a & \text{otherwise} \end{cases}$$

List.erase_replicate theorem

[LawfulBEq α] {n : Nat} {a b : α} : (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a

Full source

theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
    (replicate n a).erase b = if b == a then replicate (n - 1) a else replicate n a := by
  rw [erase_eq_eraseP]
  simp [eraseP_replicate]

Behavior of List Erasure on Replicated Elements: $\text{erase}~(a^n)~b = \text{if}~b = a~\text{then}~a^{n-1}~\text{else}~a^n$

Informal description

For any natural number $n$ and elements $a, b$ of a type $\alpha$ with a lawful boolean equality relation, the result of removing the first occurrence of $b$ from a list of $n$ copies of $a$ is: - A list of $n-1$ copies of $a$ if $b$ is equal to $a$, - The original list of $n$ copies of $a$ otherwise. In other words, $\text{erase}~(\text{replicate}~n~a)~b = \text{if}~b = a~\text{then}~\text{replicate}~(n-1)~a~\text{else}~\text{replicate}~n~a$.

List.erase_comm theorem

[LawfulBEq α] (a b : α) {l : List α} : (l.erase a).erase b = (l.erase b).erase a

Full source

theorem erase_comm [LawfulBEq α] (a b : α) {l : List α} :
    (l.erase a).erase b = (l.erase b).erase a := by
  if ab : a == b then rw [eq_of_beq ab] else ?_
  if ha : a ∈ l then ?_ else
    simp only [erase_of_not_mem ha, erase_of_not_mem (mt mem_of_mem_erase ha)]
  if hb : b ∈ l then ?_ else
    simp only [erase_of_not_mem hb, erase_of_not_mem (mt mem_of_mem_erase hb)]
  match l, l.erase a, exists_erase_eq ha with
  | _, _, ⟨l₁, l₂, ha', rfl, rfl⟩ =>
    if h₁ : b ∈ l₁ then
      rw [erase_append_left _ h₁, erase_append_left _ h₁,
          erase_append_right _ (mt mem_of_mem_erase ha'), erase_cons_head]
    else
      rw [erase_append_right _ h₁, erase_append_right _ h₁, erase_append_right _ ha',
          erase_cons_tail ab, erase_cons_head]

Commutativity of List Element Removal: $(l \setminus a) \setminus b = (l \setminus b) \setminus a$

Informal description

For any type $\alpha$ with a lawful boolean equality relation and any elements $a, b \in \alpha$, the order of removing $a$ and $b$ from a list $l$ does not affect the result. That is, removing $a$ first and then $b$ yields the same list as removing $b$ first and then $a$: $$(l \setminus a) \setminus b = (l \setminus b) \setminus a$$

List.erase_eq_iff theorem

 [LawfulBEq α] {a : α} {l : List α} :
  l.erase a = l' ↔ (a ∉ l ∧ l = l') ∨ ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂

Full source

theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
    l.erase a = l' ↔
      (a ∉ l ∧ l = l') ∨
        ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ := by
  rw [erase_eq_eraseP', eraseP_eq_iff]
  simp only [beq_iff_eq, forall_mem_ne', exists_and_left]
  constructor
  · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, xs, rfl, rfl⟩)
    · left; simp_all
    · right; refine ⟨l', h, xs, by simp⟩
  · rintro (⟨h, rfl⟩ | ⟨l₁, h, xs, rfl, rfl⟩)
    · left; simp_all
    · right; refine ⟨a, l₁, h, by simp⟩

Characterization of List Erasure: $l.\text{erase}~a = l'$ if and only if $a \notin l$ and $l = l'$ or $l$ splits around $a$ as $l_1 ++ [a] ++ l_2$ with $l' = l_1 ++ l_2$

Informal description

For a type $\alpha$ with a lawful boolean equality relation, an element $a \in \alpha$, and lists $l, l'$ of elements of type $\alpha$, the equality $l.\text{erase}~a = l'$ holds if and only if either: 1. $a$ does not appear in $l$ and $l = l'$, or 2. There exist lists $l_1, l_2$ such that: - $a$ does not appear in $l_1$, - $l$ decomposes as $l = l_1 ++ [a] ++ l_2$ (where $++$ denotes list concatenation), - $l' = l_1 ++ l_2$.

List.erase_replicate_self theorem

[LawfulBEq α] {a : α} : (replicate n a).erase a = replicate (n - 1) a

Full source

@[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
    (replicate n a).erase a = replicate (n - 1) a := by
  cases n <;> simp [replicate_succ]

Removing an element from a replicated list: $\text{erase}(\text{replicate}(n, a), a) = \text{replicate}(n - 1, a)$

Informal description

For any type $\alpha$ with a lawful boolean equality relation and any element $a \in \alpha$, removing the first occurrence of $a$ from a list containing $n$ copies of $a$ results in a list containing $n-1$ copies of $a$. That is, $\text{erase}(\text{replicate}(n, a), a) = \text{replicate}(n - 1, a)$.

List.erase_replicate_ne theorem

[LawfulBEq α] {a b : α} (h : !b == a) : (replicate n a).erase b = replicate n a

Full source

@[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
    (replicate n a).erase b = replicate n a := by
  rw [erase_of_not_mem]
  simp_all

Erasing a Non-Matching Element from a Replicated List Leaves it Unchanged

Informal description

For any type $\alpha$ with a lawful boolean equality relation, and any elements $a, b \in \alpha$ such that $b \neq a$, the list obtained by removing the first occurrence of $b$ from a list containing $n$ copies of $a$ is equal to the original list of $n$ copies of $a$. In other words, $\text{erase}~(\text{replicate}~n~a)~b = \text{replicate}~n~a$.

List.Pairwise.erase theorem

[LawfulBEq α] {l : List α} (a) : Pairwise p l → Pairwise p (l.erase a)

Full source

theorem Pairwise.erase [LawfulBEq α] {l : List α} (a) : Pairwise p l → Pairwise p (l.erase a) :=
  Pairwise.sublist <| erase_sublist

Preservation of Pairwise Relation under Element Removal: $\text{Pairwise}(p, l) \to \text{Pairwise}(p, l \setminus a)$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $l$ of elements of type $\alpha$, and any element $a \in \alpha$, if the relation $p$ holds pairwise for all elements in $l$, then $p$ also holds pairwise for all elements in the list obtained by removing the first occurrence of $a$ from $l$.

List.Nodup.erase_eq_filter theorem

[LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a)

Full source

theorem Nodup.erase_eq_filter [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
  induction d with
  | nil => rfl
  | cons m _n ih =>
    rename_i b l
    by_cases h : b = a
    · subst h
      rw [erase_cons_head, filter_cons_of_neg (by simp)]
      apply Eq.symm
      rw [filter_eq_self]
      simpa [@eq_comm α] using m
    · simp [beq_false_of_ne h, ih, h]

Erase Equals Filter for Duplicate-Free Lists: $\text{erase}(l, a) = \text{filter}(x \neq a, l)$ when $l$ has no duplicates

Informal description

For any type $\alpha$ with a lawful boolean equality relation, and any list $l$ of elements of type $\alpha$ with no duplicates, the list obtained by removing the first occurrence of an element $a$ from $l$ is equal to the list obtained by filtering out all elements equal to $a$ from $l$. That is, $\text{erase}(l, a) = \text{filter}(\lambda x, x \neq a, l)$.

List.Nodup.mem_erase_iff theorem

[LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Full source

theorem Nodup.mem_erase_iff [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase ba ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
  rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]

Membership in Erased List for Duplicate-Free Lists: $a \in \text{erase}(l, b) \leftrightarrow a \neq b \land a \in l$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $l$ of elements of type $\alpha$ with no duplicates, and any elements $a, b \in \alpha$, the element $a$ belongs to the list obtained by removing the first occurrence of $b$ from $l$ if and only if $a$ is not equal to $b$ and $a$ belongs to $l$. That is: $$a \in \text{erase}(l, b) \leftrightarrow a \neq b \land a \in l$$

List.Nodup.not_mem_erase theorem

[LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a

Full source

theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
  simpa using ((Nodup.mem_erase_iff h).mp H).left

Non-membership in Erased List for Duplicate-Free Lists: $a \notin \text{erase}(l, a)$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $l$ of elements of type $\alpha$ with no duplicates, and any element $a \in \alpha$, the element $a$ does not belong to the list obtained by removing its first occurrence from $l$. That is, $a \notin \text{erase}(l, a)$.

List.Nodup.erase theorem

[LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a)

Full source

theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
  Pairwise.erase a

Preservation of Duplicate-Free Property under Element Removal: $\text{Nodup}(l) \to \text{Nodup}(l \setminus a)$

Informal description

For any type $\alpha$ with a lawful boolean equality relation, any list $l$ of elements of type $\alpha$, and any element $a \in \alpha$, if $l$ has no duplicate elements, then the list obtained by removing the first occurrence of $a$ from $l$ also has no duplicate elements.

List.head_erase_mem theorem

(xs : List α) (a : α) (h) : (xs.erase a).head h ∈ xs

Full source

theorem head_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).head h ∈ xs :=
  erase_sublist.head_mem h

Head of Erased List is in Original List

Informal description

For any non-empty list $xs$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, the head of the list obtained by removing the first occurrence of $a$ from $xs$ is an element of the original list $xs$. In other words, if $xs \setminus a$ is non-empty, then $\text{head}(xs \setminus a) \in xs$.

List.getLast_erase_mem theorem

(xs : List α) (a : α) (h) : (xs.erase a).getLast h ∈ xs

Full source

theorem getLast_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).getLast h ∈ xs :=
  erase_sublist.getLast_mem h

Membership of Last Element After Erasure: $\text{last}(xs \setminus a) \in xs$

Informal description

For any list $xs$ of elements of type $\alpha$, any element $a$ of type $\alpha$, and any proof $h$ that $xs \setminus a$ is non-empty, the last element of $xs \setminus a$ is an element of $xs$.

List.erase_eq_eraseIdx theorem

 (l : List α) (a : α) :
  l.erase a =
    match l.idxOf? a with
    | none => l
    | some i => l.eraseIdx i

Full source

theorem erase_eq_eraseIdx (l : List α) (a : α) :
    l.erase a = match l.idxOf? a with
    | none => l
    | somesome i => l.eraseIdx i := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    rw [erase_cons, idxOf?_cons]
    split
    · simp
    · simp [ih]
      split <;> simp [*]

Equivalence of List Erasure Methods: $\text{erase } l a = \text{eraseIdx } l (\text{first index of } a \text{ in } l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, the result of removing the first occurrence of $a$ from $l$ is equal to: - $l$ if $a$ does not appear in $l$ (i.e., $\text{idxOf? } a l = \text{none}$), or - the result of removing the element at the first index where $a$ appears in $l$ (i.e., $\text{eraseIdx } l i$ where $\text{idxOf? } a l = \text{some } i$). In mathematical notation: $$ \text{erase } l a = \begin{cases} l & \text{if } \text{idxOf? } a l = \text{none} \\ \text{eraseIdx } l i & \text{if } \text{idxOf? } a l = \text{some } i \end{cases} $$

List.length_eraseIdx theorem

{l : List α} {i : Nat} : (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length

Full source

theorem length_eraseIdx {l : List α} {i : Nat} :
    (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
  induction l generalizing i with
  | nil => simp
  | cons x l ih =>
    cases i with
    | zero => simp
    | succ i =>
      simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]
      split
      · cases l <;> simp_all
      · rfl

Length of List After Element Removal: $\text{length}(\text{eraseIdx}(l, i)) = \text{length}(l) - 1$ if $i < \text{length}(l)$, else $\text{length}(l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number index $i$, the length of the list obtained by removing the element at index $i$ (denoted $\text{eraseIdx}(l, i)$) is equal to: - $l.\text{length} - 1$ if $i$ is a valid index in $l$ (i.e., $i < l.\text{length}$), or - $l.\text{length}$ otherwise. In mathematical notation: $$ \text{length}(\text{eraseIdx}(l, i)) = \begin{cases} \text{length}(l) - 1 & \text{if } i < \text{length}(l) \\ \text{length}(l) & \text{otherwise} \end{cases} $$

List.length_eraseIdx_of_lt theorem

{l : List α} {i} (h : i < length l) : (l.eraseIdx i).length = length l - 1

Full source

theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
    (l.eraseIdx i).length = length l - 1 := by
  simp [length_eraseIdx, h]

Length Decreases by One When Removing Element at Valid Index: $\text{length}(\text{eraseIdx}(l, i)) = \text{length}(l) - 1$ for $i < \text{length}(l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number index $i$ such that $i < \text{length}(l)$, the length of the list obtained by removing the element at index $i$ is equal to $\text{length}(l) - 1$.

List.eraseIdx_zero theorem

{l : List α} : eraseIdx l 0 = l.tail

Full source

@[simp] theorem eraseIdx_zero {l : List α} : eraseIdx l 0 = l.tail := by cases l <;> rfl

Removing First Element Yields Tail of List

Informal description

For any list $L$ of elements of type $\alpha$, removing the element at index $0$ (the first element) results in the tail of the list, i.e., $\text{eraseIdx}(L, 0) = \text{tail}(L)$.

List.eraseIdx_eq_take_drop_succ theorem

: ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)

Full source

theorem eraseIdx_eq_take_drop_succ :
    ∀ (l : List α) (i : Nat), l.eraseIdx i = l.take i ++ l.drop (i + 1)
  | nil, _ => by simp
  | a::l, 0 => by simp
  | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]

List Removal via Take and Drop: $\text{eraseIdx}(L, i) = \text{take}(i, L) \mathbin{+\kern-0.5em+} \text{drop}(i+1, L)$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the list obtained by removing the element at position $i$ is equal to the concatenation of the first $i$ elements of $L$ and the elements of $L$ starting from position $i+1$. That is, \[ \text{eraseIdx}(L, i) = \text{take}(i, L) \mathbin{+\kern-0.5em+} \text{drop}(i+1, L). \]

List.eraseIdx_eq_nil_iff theorem

{l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0)

Full source

@[simp] theorem eraseIdx_eq_nil_iff {l : List α} {i : Nat} : eraseIdxeraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by
  match l, i with
  | [], _
  | a::l, 0
  | a::l, i + 1 => simp [Nat.succ_inj']

Empty List After Removal: $\text{eraseIdx}(L, i) = [] \leftrightarrow L = [] \lor (\text{length}(L) = 1 \land i = 0)$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the list obtained by removing the element at index $i$ is empty if and only if either $L$ is empty, or $L$ has length $1$ and $i = 0$.

List.eraseIdx_eq_nil abbrev

Full source

@[deprecated eraseIdx_eq_nil_iff (since := "2025-01-30")]
abbrev eraseIdx_eq_nil := @eraseIdx_eq_nil_iff

Empty List After Removal: $\text{eraseIdx}(L, i) = [] \leftrightarrow L = [] \lor (\text{length}(L) = 1 \land i = 0)$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the list obtained by removing the element at index $i$ is empty if and only if either $L$ is empty, or $L$ has length $1$ and $i = 0$.

List.eraseIdx_ne_nil_iff theorem

{l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0)

Full source

theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdxeraseIdx l i ≠ []eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0) := by
  match l with
  | []
  | [a]
  | a::b::l => simp [Nat.succ_inj']

Non-Empty List After Removal: $\text{eraseIdx}(L, i) \neq [] \leftrightarrow \text{length}(L) \geq 2 \lor (\text{length}(L) = 1 \land i \neq 0)$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the list obtained by removing the element at index $i$ is non-empty if and only if either the length of $L$ is at least 2, or $L$ has length 1 and $i \neq 0$.

List.eraseIdx_ne_nil abbrev

Full source

@[deprecated eraseIdx_ne_nil_iff (since := "2025-01-30")]
abbrev eraseIdx_ne_nil := @eraseIdx_ne_nil_iff

Non-Empty List After Element Removal: $\text{eraseIdx}(L, i) \neq [] \leftrightarrow \text{length}(L) \geq 2 \lor (\text{length}(L) = 1 \land i \neq 0)$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the list obtained by removing the element at index $i$ is non-empty if and only if either the length of $L$ is at least 2, or $L$ has length 1 and $i \neq 0$.

List.eraseIdx_sublist theorem

: ∀ (l : List α) (k : Nat), eraseIdx l k <+ l

Full source

theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdxeraseIdx l k <+ l
  | [], _ => by simp
  | a::l, 0 => by simp
  | a::l, k + 1 => by simp [eraseIdx_sublist]

Sublist Property of List Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $k$, the list obtained by removing the element at position $k$ from $L$ is a sublist of $L$. In other words, $\text{eraseIdx}(L, k) <+ L$.

List.mem_of_mem_eraseIdx theorem

{l : List α} {i : Nat} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l

Full source

theorem mem_of_mem_eraseIdx {l : List α} {i : Nat} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l :=
  (eraseIdx_sublist _ _).mem h

Membership Preservation under List Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$, any index $i \in \mathbb{N}$, and any element $a \in \alpha$, if $a$ is a member of the list obtained by removing the element at index $i$ from $L$, then $a$ is also a member of the original list $L$.

List.eraseIdx_subset theorem

{l : List α} {k : Nat} : eraseIdx l k ⊆ l

Full source

theorem eraseIdx_subset {l : List α} {k : Nat} : eraseIdxeraseIdx l k ⊆ l :=
  (eraseIdx_sublist _ _).subset

Subset Property of List Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $k$, the list obtained by removing the element at position $k$ from $L$ is a subset of $L$. In other words, $\text{eraseIdx}(L, k) \subseteq L$.

List.eraseIdx_eq_self theorem

: ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k

Full source

@[simp]
theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdxeraseIdx l k = l ↔ length l ≤ k
  | [], _ => by simp
  | a::l, 0 => by simp [(cons_ne_self _ _).symm]
  | a::l, k + 1 => by simp [eraseIdx_eq_self]

Condition for List Unchanged by Element Removal: $\text{eraseIdx}(L, k) = L \leftrightarrow \text{length}(L) \leq k$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $k$, the list obtained by removing the element at position $k$ from $L$ is equal to $L$ itself if and only if the length of $L$ is less than or equal to $k$. In other words, $\text{eraseIdx}(L, k) = L \leftrightarrow \text{length}(L) \leq k$.

List.eraseIdx_of_length_le theorem

{l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l

Full source

theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
  rw [eraseIdx_eq_self.2 h]

List Unchanged Under `eraseIdx` When Index Exceeds Length: $\text{eraseIdx}(L, k) = L$ if $\text{length}(L) \leq k$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $k$, if the length of $L$ is less than or equal to $k$, then removing the element at position $k$ from $L$ leaves the list unchanged, i.e., $\text{eraseIdx}(L, k) = L$.

List.length_eraseIdx_le theorem

(l : List α) (i : Nat) : length (l.eraseIdx i) ≤ length l

Full source

theorem length_eraseIdx_le (l : List α) (i : Nat) : length (l.eraseIdx i) ≤ length l :=
  (eraseIdx_sublist _ _).length_le

Length Does Not Increase After Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the length of the list obtained by removing the element at position $i$ from $L$ is less than or equal to the length of $L$. In other words, $\text{length}(\text{eraseIdx}(L, i)) \leq \text{length}(L)$.

List.le_length_eraseIdx theorem

(l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i)

Full source

theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i) := by
  rw [length_eraseIdx]
  split <;> simp

Lower Bound on List Length After Element Removal: $\text{length}(L) - 1 \leq \text{length}(\text{eraseIdx}(L, i))$

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number index $i$, the length of $L$ minus one is less than or equal to the length of the list obtained by removing the element at index $i$ from $L$. In other words, $\text{length}(L) - 1 \leq \text{length}(\text{eraseIdx}(L, i))$.

List.eraseIdx_append_of_lt_length theorem

{l : List α} {k : Nat} (hk : k < length l) (l' : List α) : eraseIdx (l ++ l') k = eraseIdx l k ++ l'

Full source

theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
    eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
  induction l generalizing k with
  | nil => simp_all
  | cons x l ih =>
    cases k with
    | zero => rfl
    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_lt_succ_iff]

Removing an Element from Concatenated Lists When Index is in First List

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $k$ such that $k < \text{length}(l)$, and any list $l'$ of elements of type $\alpha$, the result of removing the element at index $k$ from the concatenated list $l \mathbin{+\!\!+} l'$ is equal to the concatenation of the list obtained by removing the element at index $k$ from $l$ and the list $l'$.

List.eraseIdx_append_of_length_le theorem

{l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) : eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l)

Full source

theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤ k) (l' : List α) :
    eraseIdx (l ++ l') k = l ++ eraseIdx l' (k - length l) := by
  induction l generalizing k with
  | nil => simp_all
  | cons x l ih =>
    cases k with
    | zero => simp_all
    | succ k => simp_all [eraseIdx_cons_succ, Nat.succ_sub_succ]

Removing an Element from Concatenated Lists When Index is in Second List

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $k$ such that $\text{length}(l) \leq k$, and any list $l'$ of elements of $\alpha$, the result of removing the element at index $k$ from the concatenated list $l \mathbin{+\!\!+} l'$ is equal to the concatenation of $l$ and the list obtained by removing the element at index $k - \text{length}(l)$ from $l'$.

List.eraseIdx_replicate theorem

{n : Nat} {a : α} {k : Nat} : (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a

Full source

theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
    (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
  split <;> rename_i h
  · rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]
    simp only [length_replicate, true_and]
    intro b m
    replace m := mem_of_mem_eraseIdx m
    simp only [mem_replicate] at m
    exact m.2
  · rw [eraseIdx_of_length_le (by simpa using h)]

Effect of `eraseIdx` on Replicated Lists: $\text{eraseIdx}(\text{replicate}\,n\,a, k) = \text{if } k < n \text{ then } \text{replicate}\,(n-1)\,a \text{ else } \text{replicate}\,n\,a$

Informal description

For any natural number $n$, any element $a$ of type $\alpha$, and any index $k$, removing the element at position $k$ from a list consisting of $n$ copies of $a$ results in: - A list of $n-1$ copies of $a$ if $k < n$ - The original list of $n$ copies of $a$ otherwise In other words: $$\text{eraseIdx}(\text{replicate}\,n\,a, k) = \begin{cases} \text{replicate}\,(n-1)\,a & \text{if } k < n \\ \text{replicate}\,n\,a & \text{otherwise} \end{cases}$$

List.Pairwise.eraseIdx theorem

{l : List α} (k) : Pairwise p l → Pairwise p (l.eraseIdx k)

Full source

theorem Pairwise.eraseIdx {l : List α} (k) : Pairwise p l → Pairwise p (l.eraseIdx k) :=
  Pairwise.sublist <| eraseIdx_sublist _ _

Preservation of Pairwise Relation under Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$ and any index $k$, if the relation $p$ holds pairwise for all elements in $L$, then $p$ also holds pairwise for the list obtained by removing the element at position $k$ from $L$.

List.Nodup.eraseIdx theorem

{l : List α} (k) : Nodup l → Nodup (l.eraseIdx k)

Full source

theorem Nodup.eraseIdx {l : List α} (k) : Nodup l → Nodup (l.eraseIdx k) :=
  Pairwise.eraseIdx k

Preservation of No-Duplicates Property under Element Removal by Index

Informal description

For any list $L$ of elements of type $\alpha$ and any index $k$, if $L$ has no duplicate elements, then the list obtained by removing the element at position $k$ from $L$ also has no duplicate elements.

List.IsPrefix.eraseIdx theorem

{l l' : List α} (h : l <+: l') (k : Nat) : eraseIdx l k <+: eraseIdx l' k

Full source

protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
    eraseIdxeraseIdx l k <+: eraseIdx l' k := by
  rcases h with ⟨t, rfl⟩
  if hkl : k < length l then
    simp [eraseIdx_append_of_lt_length hkl]
  else
    rw [Nat.not_lt] at hkl
    simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]

Prefix Preservation under Index Removal: $\text{eraseIdx}(l, k) <+: \text{eraseIdx}(l', k)$ when $l <+: l'$

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ is a prefix of $l'$ (i.e., there exists a list $t$ such that $l' = l \mathbin{+\!\!+} t$), then for any natural number index $k$, the list obtained by removing the element at position $k$ from $l$ is a prefix of the list obtained by removing the element at position $k$ from $l'$.

List.erase_eq_eraseIdx_of_idxOf theorem

[BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} (w : l.idxOf a = i) : l.erase a = l.eraseIdx i

Full source

theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
    {l : List α} {a : α} {i : Nat} (w : l.idxOf a = i) :
    l.erase a = l.eraseIdx i := by
  subst w
  rw [erase_eq_iff]
  by_cases h : a ∈ l
  · right
    obtain ⟨as, bs, rfl, h'⟩ := eq_append_cons_of_mem h
    refine ⟨as, bs, h', by simp, ?_⟩
    rw [idxOf_append, if_neg h', idxOf_cons_self, eraseIdx_append_of_length_le] <;>
      simp
  · left
    refine ⟨h, ?_⟩
    rw [eq_comm, eraseIdx_eq_self]
    exact Nat.le_of_eq (idxOf_eq_length h).symm

Equivalence of Element Removal by Value and by Index in Lists with Lawful Boolean Equality

Informal description

For a type $\alpha$ with a lawful boolean equality relation, given a list $l$ of elements of type $\alpha$, an element $a \in \alpha$, and a natural number $i$ such that the index of the first occurrence of $a$ in $l$ equals $i$, the list obtained by removing the first occurrence of $a$ from $l$ is equal to the list obtained by removing the element at index $i$ from $l$.

List.erase_eq_eraseIdx_of_indexOf abbrev

Full source

@[deprecated erase_eq_eraseIdx_of_idxOf (since := "2025-01-29")]
abbrev erase_eq_eraseIdx_of_indexOf := @erase_eq_eraseIdx_of_idxOf

Equivalence of Element Removal by Value and by Index in Lists with Lawful Boolean Equality

Informal description

For a type $\alpha$ with a lawful boolean equality relation, given a list $l$ of elements of type $\alpha$, an element $a \in \alpha$, and a natural number $i$ such that the index of the first occurrence of $a$ in $l$ equals $i$, the list obtained by removing the first occurrence of $a$ from $l$ is equal to the list obtained by removing the element at index $i$ from $l$.