Init.Data.List.Nat.Erase

List.getElem?_eraseIdx theorem

{l : List α} {i : Nat} {j : Nat} : (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

Full source

theorem getElem?_eraseIdx {l : List α} {i : Nat} {j : Nat} :
    (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]? := by
  rw [eraseIdx_eq_take_drop_succ, getElem?_append]
  split <;> rename_i h
  · rw [getElem?_take]
    split
    · rfl
    · simp_all
      omega
  · rw [getElem?_drop]
    split <;> rename_i h'
    · simp only [length_take, Nat.min_def, Nat.not_lt] at h
      split at h
      · omega
      · simp_all [getElem?_eq_none]
        omega
    · simp only [length_take]
      simp only [length_take, Nat.min_def, Nat.not_lt] at h
      split at h
      · congr 1
        omega
      · rw [getElem?_eq_none, getElem?_eq_none] <;> omega

Optional Indexing After List Removal: $(l.\text{eraseIdx}\ i)[j]? = \text{if } j < i \text{ then } l[j]? \text{ else } l[j+1]?$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$, the optional indexing operation on the list obtained by removing the element at position $i$ satisfies: $$(l.\text{eraseIdx}\ i)[j]? = \begin{cases} l[j]? & \text{if } j < i \\ l[j+1]? & \text{otherwise} \end{cases}$$

List.getElem?_eraseIdx_of_lt theorem

{l : List α} {i : Nat} {j : Nat} (h : j < i) : (l.eraseIdx i)[j]? = l[j]?

Full source

theorem getElem?_eraseIdx_of_lt {l : List α} {i : Nat} {j : Nat} (h : j < i) :
    (l.eraseIdx i)[j]? = l[j]? := by
  rw [getElem?_eraseIdx]
  simp [h]

Optional Indexing Preserved Before Removal Point: $(l.\text{eraseIdx}\ i)[j]? = l[j]?$ when $j < i$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$ such that $j < i$, the optional indexing operation on the list obtained by removing the element at position $i$ satisfies $(l.\text{eraseIdx}\ i)[j]? = l[j]?$.

List.getElem?_eraseIdx_of_ge theorem

{l : List α} {i : Nat} {j : Nat} (h : i ≤ j) : (l.eraseIdx i)[j]? = l[j + 1]?

Full source

theorem getElem?_eraseIdx_of_ge {l : List α} {i : Nat} {j : Nat} (h : i ≤ j) :
    (l.eraseIdx i)[j]? = l[j + 1]? := by
  rw [getElem?_eraseIdx]
  simp only [dite_eq_ite, ite_eq_right_iff]
  intro h'
  omega

Optional Indexing After List Removal for Indices Greater Than or Equal to Removal Point: $(l.\text{eraseIdx}\ i)[j]? = l[j+1]?$ when $i \leq j$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$ such that $i \leq j$, the optional indexing operation on the list obtained by removing the element at position $i$ satisfies $(l.\text{eraseIdx}\ i)[j]? = l[j + 1]?$.

List.getElem_eraseIdx theorem

 {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) :
  (l.eraseIdx i)[j] =
    if h' : j < i then l[j]'(by have := length_eraseIdx_le l i; omega)
    else l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega)

Full source

theorem getElem_eraseIdx {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) :
    (l.eraseIdx i)[j] = if h' : j < i then
        l[j]'(by have := length_eraseIdx_le l i; omega)
      else
        l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
  apply Option.some.inj
  rw [← getElem?_eq_getElem, getElem?_eraseIdx]
  split <;> simp

Element Access After List Removal: $(l.\text{eraseIdx}\ i)[j] = \text{if } j < i \text{ then } l[j] \text{ else } l[j+1]$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$ such that $j$ is a valid index in the list obtained by removing the $i$-th element of $l$ (i.e., $j < \text{length}(l.\text{eraseIdx}\ i)$), the element at position $j$ in the modified list satisfies: $$(l.\text{eraseIdx}\ i)[j] = \begin{cases} l[j] & \text{if } j < i \\ l[j+1] & \text{otherwise} \end{cases}$$

List.getElem_eraseIdx_of_lt theorem

 {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) (h' : j < i) :
  (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega)

Full source

theorem getElem_eraseIdx_of_lt {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) (h' : j < i) :
    (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega) := by
  rw [getElem_eraseIdx]
  simp only [dite_eq_left_iff, Nat.not_lt]
  intro h'
  omega

Element Access After List Removal for Indices Less Than Removal Index: $(l.\text{eraseIdx}\ i)[j] = l[j]$ when $j < i$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$ such that $j$ is a valid index in the list obtained by removing the $i$-th element of $l$ (i.e., $j < \text{length}(l.\text{eraseIdx}\ i)$) and $j < i$, the element at position $j$ in the modified list equals the element at position $j$ in the original list, i.e., $(l.\text{eraseIdx}\ i)[j] = l[j]$.

List.getElem_eraseIdx_of_ge theorem

 {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
  (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega)

Full source

theorem getElem_eraseIdx_of_ge {l : List α} {i : Nat} {j : Nat} (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
    (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
  rw [getElem_eraseIdx, dif_neg]
  omega

Element Access After List Removal for Indices Greater Than or Equal to Removal Index: $(l.\text{eraseIdx}\ i)[j] = l[j+1]$ when $i \leq j$

Informal description

For any list $l$ of elements of type $\alpha$ and natural numbers $i$ and $j$ such that $j$ is a valid index in the list obtained by removing the $i$-th element of $l$ (i.e., $j < \text{length}(l.\text{eraseIdx}\ i)$) and $i \leq j$, the element at position $j$ in the modified list equals the element at position $j+1$ in the original list, i.e., $(l.\text{eraseIdx}\ i)[j] = l[j+1]$.

List.eraseIdx_eq_dropLast theorem

{l : List α} {i : Nat} (h : i + 1 = l.length) : l.eraseIdx i = l.dropLast

Full source

theorem eraseIdx_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) :
    l.eraseIdx i = l.dropLast := by
  simp [eraseIdx_eq_take_drop_succ, h]
  rw [take_eq_dropLast h]

Equality of Element Removal and Last Element Removal: $\text{eraseIdx}(l, i) = \text{dropLast}(l)$ when $i + 1 = |l|$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $i$ such that $i + 1$ equals the length of $l$, removing the element at index $i$ from $l$ is equivalent to removing the last element of $l$, i.e., $\text{eraseIdx}(l, i) = \text{dropLast}(l)$.

List.eraseIdx_set_eq theorem

{l : List α} {i : Nat} {a : α} : (l.set i a).eraseIdx i = l.eraseIdx i

Full source

theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
    (l.set i a).eraseIdx i = l.eraseIdx i := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro n h₁ h₂
    rw [getElem_eraseIdx, getElem_eraseIdx]
    split <;>
    · rw [getElem_set_ne]
      omega

Element Removal After Replacement at Same Index: $(l.\text{set}\ i\ a).\text{eraseIdx}\ i = l.\text{eraseIdx}\ i$

Informal description

For any list $l$ of elements of type $\alpha$, any natural number index $i$, and any element $a$ of type $\alpha$, removing the element at index $i$ from the list obtained by setting the $i$-th element of $l$ to $a$ yields the same result as removing the element at index $i$ from the original list $l$. That is, $(l.\text{set}\ i\ a).\text{eraseIdx}\ i = l.\text{eraseIdx}\ i$.

List.eraseIdx_set_lt theorem

{l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) : (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a

Full source

theorem eraseIdx_set_lt {l : List α} {i : Nat} {j : Nat} {a : α} (h : j < i) :
    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro n h₁ h₂
    simp only [length_eraseIdx, length_set] at h₁
    simp only [getElem_eraseIdx, getElem_set]
    split
    · split
      · split
        · rfl
        · omega
      · split
        · omega
        · rfl
    · split
      · split
        · rfl
        · omega
      · have t : i - 1 ≠ n := by omega
        simp [t]

Element Removal and Replacement Commute When $j < i$: $(l.\text{set}(i, a)).\text{eraseIdx}(j) = (l.\text{eraseIdx}(j)).\text{set}(i-1, a)$

Informal description

For any list $l$ of elements of type $\alpha$, any natural numbers $i$ and $j$, and any element $a \in \alpha$, if $j < i$, then removing the element at index $j$ from the list obtained by setting the $i$-th element of $l$ to $a$ is equal to first removing the $j$-th element from $l$ and then setting the $(i-1)$-th element of the resulting list to $a$. In mathematical notation: $$(l.\text{set}(i, a)).\text{eraseIdx}(j) = (l.\text{eraseIdx}(j)).\text{set}(i-1, a)$$

List.eraseIdx_set_gt theorem

{l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) : (l.set i a).eraseIdx j = (l.eraseIdx j).set i a

Full source

theorem eraseIdx_set_gt {l : List α} {i : Nat} {j : Nat} {a : α} (h : i < j) :
    (l.set i a).eraseIdx j = (l.eraseIdx j).set i a := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro n h₁ h₂
    simp only [length_eraseIdx, length_set] at h₁
    simp only [getElem_eraseIdx, getElem_set]
    split
    · rfl
    · split
      · split
        · rfl
        · omega
      · have t : i ≠ n := by omega
        simp [t]

Commutativity of List Replacement and Removal for $i < j$: $(l[i \mapsto a]).\text{erase}(j) = (l.\text{erase}(j))[i \mapsto a]$

Informal description

For any list $l$ of elements of type $\alpha$, indices $i$ and $j$, and element $a \in \alpha$, if $i < j$, then removing the element at index $j$ from the list obtained by setting the $i$-th element of $l$ to $a$ is equal to first removing the element at index $j$ from $l$ and then setting the $i$-th element of the resulting list to $a$. In other words: $$(l.\text{set}(i, a)).\text{eraseIdx}(j) = (l.\text{eraseIdx}(j)).\text{set}(i, a)$$

List.set_getElem_succ_eraseIdx_succ theorem

{l : List α} {i : Nat} (h : i + 1 < l.length) : (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

Full source

@[simp] theorem set_getElem_succ_eraseIdx_succ
    {l : List α} {i : Nat} (h : i + 1 < l.length) :
    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i := by
  apply ext_getElem
  · simp only [length_set, length_eraseIdx, h, ↓reduceIte]
    rw [if_pos]
    omega
  · intro n h₁ h₂
    simp [getElem_set, getElem_eraseIdx]
    split
    · split
      · omega
      · simp_all
    · split
      · split
        · rfl
        · omega
      · have t : ¬ n < i := by omega
        simp [t]

List Modification Identity: $(l \setminus \{i+1\})[i := l[i+1]] = l \setminus \{i\}$ when $i+1 < \text{length}(l)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number index $i$ such that $i + 1$ is a valid index in $l$ (i.e., $i + 1 < \text{length}(l)$), the following equality holds: $$(l.\text{eraseIdx}(i + 1)).\text{set}(i, l[i + 1]) = l.\text{eraseIdx}(i)$$

List.eraseIdx_length_sub_one theorem

{l : List α} : (l.eraseIdx (l.length - 1)) = l.dropLast

Full source

@[simp] theorem eraseIdx_length_sub_one {l : List α} :
    (l.eraseIdx (l.length - 1)) = l.dropLast := by
  apply ext_getElem
  · simp [length_eraseIdx]
    omega
  · intro n h₁ h₂
    rw [getElem_eraseIdx_of_lt, getElem_dropLast]
    simp_all

Removing Last Element by Index Equals Dropping Last Element

Informal description

For any list $l$ of elements of type $\alpha$, removing the element at index $\text{length}(l) - 1$ (the last element) results in the same list as applying the `dropLast` operation to $l$, i.e., $$ \text{eraseIdx}(l, \text{length}(l) - 1) = \text{dropLast}(l). $$