Init.Data.List.Nat.Modify

List.length_modifyHead theorem

{f : α → α} {l : List α} : (l.modifyHead f).length = l.length

Full source

@[simp] theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length := by
  cases l <;> simp [modifyHead]

Length Preservation under Head Modification: $\text{length}(\text{modifyHead } f \, l) = \text{length}(l)$

Informal description

For any function $f : \alpha \to \alpha$ and any list $l$ of elements of type $\alpha$, the length of the list remains unchanged after modifying its head element with $f$. That is, $\text{length}(\text{modifyHead } f \, l) = \text{length}(l)$.

List.modifyHead_eq_set theorem

[Inhabited α] (f : α → α) (l : List α) : l.modifyHead f = l.set 0 (f (l[0]?.getD default))

Full source

theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
    l.modifyHead f = l.set 0 (f (l[0]?.getD default)) := by cases l <;> simp [modifyHead]

Equivalence of Head Modification and Indexed Update: $\text{modifyHead } f = \text{set } 0 (f (\text{head } l))$

Informal description

For any type $\alpha$ with a default element (given by `[Inhabited α]`), any function $f : \alpha \to \alpha$, and any list $l$ of elements of type $\alpha$, modifying the head of $l$ with $f$ is equivalent to setting the element at index $0$ of $l$ to $f$ applied to the first element of $l$ (or the default value if $l$ is empty). In other words: $$l.\text{modifyHead } f = l.\text{set } 0 \big(f (l[0]?.\text{getD default})\big)$$ where: - $l[0]?$ is the optional first element of $l$, - $\text{getD}$ returns the default value if $l$ is empty, - $\text{set } 0$ updates the element at index $0$ (or leaves $l$ unchanged if it's empty).

List.modifyHead_eq_nil_iff theorem

{f : α → α} {l : List α} : l.modifyHead f = [] ↔ l = []

Full source

@[simp] theorem modifyHead_eq_nil_iff {f : α → α} {l : List α} :
    l.modifyHead f = [] ↔ l = [] := by cases l <;> simp [modifyHead]

Empty List Characterization under Head Modification: $l.\text{modifyHead } f = [] \leftrightarrow l = []$

Informal description

For any function $f : \alpha \to \alpha$ and any list $l$ of elements of type $\alpha$, the modified list obtained by applying $f$ to the head of $l$ is empty if and only if the original list $l$ is empty. In other words, $l.\text{modifyHead } f = [] \leftrightarrow l = []$.

List.modifyHead_modifyHead theorem

{l : List α} {f g : α → α} : (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f)

Full source

@[simp] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]

Composition of Head Modifications on Lists: $(l.\text{modifyHead } f).\text{modifyHead } g = l.\text{modifyHead } (g \circ f)$

Informal description

For any list $l$ of elements of type $\alpha$ and any functions $f, g : \alpha \to \alpha$, modifying the head of $l$ with $f$ and then modifying the resulting list's head with $g$ is equivalent to modifying the head of $l$ once with the composition $g \circ f$.

List.getElem_modifyHead theorem

 {l : List α} {f : α → α} {i} (h : i < (l.modifyHead f).length) :
  (l.modifyHead f)[i] = if h' : i = 0 then f (l[0]'(by simp at h; omega)) else l[i]'(by simpa using h)

Full source

theorem getElem_modifyHead {l : List α} {f : α → α} {i} (h : i < (l.modifyHead f).length) :
    (l.modifyHead f)[i] = if h' : i = 0 then f (l[0]'(by simp at h; omega)) else l[i]'(by simpa using h) := by
  cases l with
  | nil => simp at h
  | cons hd tl => cases i <;> simp

Element Access in List with Modified Head: $(l.\text{modifyHead } f)[i] = \begin{cases} f(l[0]) & \text{if } i = 0 \\ l[i] & \text{otherwise} \end{cases}$

Informal description

For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \alpha$, and any natural number index $i$ such that $i < \text{length}(l.\text{modifyHead } f)$, the $i$-th element of the modified list is: - $f(l[0])$ if $i = 0$ - $l[i]$ otherwise where $l[0]$ is the first element of $l$ (when $l$ is non-empty) and $l[i]$ is the $i$-th element of $l$.

List.getElem_modifyHead_zero theorem

{l : List α} {f : α → α} {h} : (l.modifyHead f)[0] = f (l[0]'(by simpa using h))

Full source

@[simp] theorem getElem_modifyHead_zero {l : List α} {f : α → α} {h} :
    (l.modifyHead f)[0] = f (l[0]'(by simpa using h)) := by simp [getElem_modifyHead]

First Element of List with Modified Head: $(\text{modifyHead}\,f\,l)[0] = f(l[0])$

Informal description

For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \alpha$, the first element of the modified list $\text{modifyHead}\,f\,l$ is equal to $f$ applied to the first element of $l$, i.e., $(\text{modifyHead}\,f\,l)[0] = f(l[0])$.

List.getElem_modifyHead_succ theorem

 {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
  (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h)

Full source

@[simp] theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
    (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]

Element Access at Successor Index in Modified List: $(l.\text{modifyHead } f)[n + 1] = l[n + 1]$

Informal description

For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \alpha$, and any natural number $n$ such that $n + 1$ is a valid index for the modified list $l.\text{modifyHead } f$, the element at index $n + 1$ in the modified list is equal to the element at index $n + 1$ in the original list $l$.

List.getElem?_modifyHead theorem

{l : List α} {f : α → α} {i} : (l.modifyHead f)[i]? = if i = 0 then l[i]?.map f else l[i]?

Full source

theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
    (l.modifyHead f)[i]? = if i = 0 then l[i]?.map f else l[i]? := by
  cases l with
  | nil => simp
  | cons hd tl => cases i <;> simp

Optional Indexing of Modified List Head: $(l.\text{modifyHead}\,f)[i]? = \text{if } i=0 \text{ then } l[i]?.map\,f \text{ else } l[i]?$

Informal description

For any list $l$ of type $\text{List}\,\alpha$, function $f : \alpha \to \alpha$, and index $i$, the optional indexing operation on the modified list $\text{modifyHead}\,f\,l$ satisfies: $$(l.\text{modifyHead}\,f)[i]? = \begin{cases} l[i]?.map\,f & \text{if } i = 0 \\ l[i]? & \text{otherwise} \end{cases}$$

List.getElem?_modifyHead_zero theorem

{l : List α} {f : α → α} : (l.modifyHead f)[0]? = l[0]?.map f

Full source

@[simp] theorem getElem?_modifyHead_zero {l : List α} {f : α → α} :
    (l.modifyHead f)[0]? = l[0]?.map f := by simp [getElem?_modifyHead]

Optional Indexing at Zero of Modified List Head: $(l.\text{modifyHead}\,f)[0]? = l[0]?.map\,f$

Informal description

For any list $l$ of type $\text{List}\,\alpha$ and function $f : \alpha \to \alpha$, the optional indexing operation at index $0$ on the modified list $\text{modifyHead}\,f\,l$ satisfies: $$(l.\text{modifyHead}\,f)[0]? = l[0]?.map\,f$$

List.getElem?_modifyHead_succ theorem

{l : List α} {f : α → α} {n} : (l.modifyHead f)[n + 1]? = l[n + 1]?

Full source

@[simp] theorem getElem?_modifyHead_succ {l : List α} {f : α → α} {n} :
    (l.modifyHead f)[n + 1]? = l[n + 1]? := by simp [getElem?_modifyHead]

Optional Indexing of Modified List Tail: $(l.\text{modifyHead}\,f)[n+1]? = l[n+1]?$

Informal description

For any list $l$ of type $\text{List}\,\alpha$, function $f : \alpha \to \alpha$, and natural number index $n$, the optional indexing operation on the modified list $\text{modifyHead}\,f\,l$ at position $n+1$ satisfies: $$(l.\text{modifyHead}\,f)[n + 1]? = l[n + 1]?$$

List.head_modifyHead theorem

(f : α → α) (l : List α) (h) : (l.modifyHead f).head h = f (l.head (by simpa using h))

Full source

@[simp] theorem head_modifyHead (f : α → α) (l : List α) (h) :
    (l.modifyHead f).head h = f (l.head (by simpa using h)) := by
  cases l with
  | nil => simp at h
  | cons hd tl => simp

Head of Modified List Equals Function Applied to Original Head

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of type $\text{List } \alpha$, and any proof $h$ that $l$ is non-empty, the head of the modified list $\text{modifyHead } f \, l$ is equal to $f$ applied to the head of $l$. That is, $(\text{modifyHead } f \, l).\text{head } h = f (l.\text{head } h')$, where $h'$ is a proof that $l$ is non-empty derived from $h$.

List.head?_modifyHead theorem

{l : List α} {f : α → α} : (l.modifyHead f).head? = l.head?.map f

Full source

@[simp] theorem head?_modifyHead {l : List α} {f : α → α} :
    (l.modifyHead f).head? = l.head?.map f := by cases l <;> simp

Head Preservation Under List Head Modification

Informal description

For any list $L$ of elements of type $\alpha$ and any function $f : \alpha \to \alpha$, the first element of the modified list $\text{modifyHead } f \, L$ (wrapped in an option) is equal to applying $f$ to the first element of $L$ (if it exists). More precisely: $$(\text{modifyHead } f \, L).\text{head?} = L.\text{head?}.map f$$

List.tail_modifyHead theorem

{f : α → α} {l : List α} : (l.modifyHead f).tail = l.tail

Full source

@[simp] theorem tail_modifyHead {f : α → α} {l : List α} :
    (l.modifyHead f).tail = l.tail := by cases l <;> simp

Tail Preservation Under Head Modification

Informal description

For any function $f : \alpha \to \alpha$ and any list $l$ of type $\text{List } \alpha$, the tail of the list obtained by modifying the head of $l$ with $f$ is equal to the tail of $l$. In other words, $\text{tail}(\text{modifyHead } f \, l) = \text{tail } l$.

List.take_modifyHead theorem

{f : α → α} {l : List α} {i} : (l.modifyHead f).take i = (l.take i).modifyHead f

Full source

@[simp] theorem take_modifyHead {f : α → α} {l : List α} {i} :
    (l.modifyHead f).take i = (l.take i).modifyHead f := by
  cases l <;> cases i <;> simp

Commutation of List Head Modification and Taking Prefix Elements

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of type $\text{List } \alpha$, and any natural number $i$, taking the first $i$ elements of the list obtained by modifying the head of $l$ with $f$ is equal to modifying the head of the first $i$ elements of $l$ with $f$. In other words: $$(\text{modifyHead } f \, l).\text{take } i = \text{modifyHead } f (l.\text{take } i)$$

List.drop_modifyHead_of_pos theorem

{f : α → α} {l : List α} {i} (h : 0 < i) : (l.modifyHead f).drop i = l.drop i

Full source

@[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {i} (h : 0 < i) :
    (l.modifyHead f).drop i = l.drop i := by
  cases l <;> cases i <;> simp_all

Drop Operation Commutes with Head Modification for Positive Indices: $\text{drop}\ i\ (\text{modifyHead}\ f\ l) = \text{drop}\ i\ l$ when $i > 0$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any positive natural number $i > 0$, dropping the first $i$ elements from the list obtained by modifying the head of $l$ with $f$ is equal to dropping the first $i$ elements from $l$ itself. That is, $\text{drop}\ i\ (\text{modifyHead}\ f\ l) = \text{drop}\ i\ l$.

List.eraseIdx_modifyHead_zero theorem

{f : α → α} {l : List α} : (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0

Full source

theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp

Index Zero Removal Commutes with Head Modification in Lists

Informal description

For any function $f : \alpha \to \alpha$ and any list $l$ of type $\text{List } \alpha$, removing the element at index $0$ from the list obtained by modifying the head of $l$ with $f$ is equal to removing the element at index $0$ from $l$ itself. That is, $\text{eraseIdx}(\text{modifyHead } f \, l, 0) = \text{eraseIdx}(l, 0)$.

List.eraseIdx_modifyHead_of_pos theorem

{f : α → α} {l : List α} {i} (h : 0 < i) : (l.modifyHead f).eraseIdx i = (l.eraseIdx i).modifyHead f

Full source

@[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {i} (h : 0 < i) :
    (l.modifyHead f).eraseIdx i = (l.eraseIdx i).modifyHead f := by cases l <;> cases i <;> simp_all

Commutativity of Head Modification and Index Removal for Positive Indices: $\text{eraseIdx}(\text{modifyHead } f \, l, i) = \text{modifyHead } f (\text{eraseIdx}(l, i))$ for $i > 0$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any positive index $i > 0$, removing the element at index $i$ from the list obtained by modifying the head of $l$ with $f$ is equal to first removing the element at index $i$ from $l$ and then modifying the head of the resulting list with $f$. That is, $\text{eraseIdx}(\text{modifyHead } f \, l, i) = \text{modifyHead } f (\text{eraseIdx}(l, i))$.

List.modifyHead_id theorem

: modifyHead (id : α → α) = id

Full source

@[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp

Identity Function Preserves List Head Modification

Informal description

For any type $\alpha$, applying the `modifyHead` operation with the identity function `id` is equivalent to the identity function itself on lists of type $\text{List } \alpha$. That is, $\text{modifyHead } \text{id} = \text{id}$.

List.modifyHead_dropLast theorem

{l : List α} {f : α → α} : l.dropLast.modifyHead f = (l.modifyHead f).dropLast

Full source

@[simp] theorem modifyHead_dropLast {l : List α} {f : α → α} :
    l.dropLast.modifyHead f = (l.modifyHead f).dropLast := by
  rcases l with _|⟨a, l⟩
  · simp
  · rcases l with _|⟨b, l⟩ <;> simp

Commutativity of Head Modification and Last Element Removal in Lists

Informal description

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

List.modifyTailIdx_id theorem

: ∀ i (l : List α), l.modifyTailIdx i id = l

Full source

@[simp] theorem modifyTailIdx_id : ∀ i (l : List α), l.modifyTailIdx i id = l
  | 0, _ => rfl
  | _+1, [] => rfl
  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)

Identity Function Preserves List Tail Modification at Index

Informal description

For any natural number $i$ and any list $l$ of elements of type $\alpha$, applying the `modifyTailIdx` operation with the identity function `id` at index $i$ leaves the list unchanged, i.e., $\text{modifyTailIdx } l \ i \ \text{id} = l$.

List.eraseIdx_eq_modifyTailIdx theorem

: ∀ i (l : List α), eraseIdx l i = l.modifyTailIdx i tail

Full source

theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modifyTailIdx i tail
  | 0, l => by cases l <;> rfl
  | _+1, [] => rfl
  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)

List Element Removal as Tail Modification: $\text{eraseIdx}(L, i) = \text{modifyTailIdx}(L, i, \text{tail})$

Informal description

For any natural number index $i$ and any list $L$ of elements of type $\alpha$, removing the element at position $i$ from $L$ is equivalent to modifying the tail sublist starting at index $i$ by taking its tail (i.e., removing its first element).

List.length_modifyTailIdx theorem

 (f : List α → List α) (H : ∀ l, (f l).length = l.length) : ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length

Full source

@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
    ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length
  | _, 0 => H _
  | [], _+1 => rfl
  | _ :: _, _+1 => congrArg (·+1) (length_modifyTailIdx _ H _ _)

Length Preservation under Tail Modification: $\text{length}(\text{modifyTailIdx}\ l\ i\ f) = \text{length}(l)$

Informal description

For any function $f$ on lists of type $\alpha$ that preserves the length of any list (i.e., $\text{length}(f(l)) = \text{length}(l)$ for all $l$), any list $l$ of type $\alpha$, and any natural number $i$, the length of the list obtained by modifying the tail sublist starting at index $i$ with $f$ is equal to the length of the original list $l$. That is, $\text{length}(\text{modifyTailIdx}\ l\ i\ f) = \text{length}(l)$.

List.modifyTailIdx_add theorem

 (f : List α → List α) (i) (l₁ l₂ : List α) : (l₁ ++ l₂).modifyTailIdx (l₁.length + i) f = l₁ ++ l₂.modifyTailIdx i f

Full source

theorem modifyTailIdx_add (f : List α → List α) (i) (l₁ l₂ : List α) :
    (l₁ ++ l₂).modifyTailIdx (l₁.length + i) f = l₁ ++ l₂.modifyTailIdx i f := by
  induction l₁ <;> simp [*, Nat.succ_add]

Modify Tail Index Distributes Over Concatenation: $(l_1 +\!\!+ l_2).\text{modifyTailIdx}\ (|l_1| + i)\ f = l_1 +\!\!+ (l_2.\text{modifyTailIdx}\ i\ f)$

Informal description

For any function $f$ on lists of type $\alpha$, any natural number $i$, and any two lists $l_1$ and $l_2$ of type $\alpha$, modifying the tail sublist of the concatenated list $l_1 +\!\!+ l_2$ starting at index $|l_1| + i$ with $f$ is equal to concatenating $l_1$ with the result of modifying the tail sublist of $l_2$ starting at index $i$ with $f$. In other words: $$(l_1 +\!\!+ l_2).\text{modifyTailIdx}\ (|l_1| + i)\ f = l_1 +\!\!+ (l_2.\text{modifyTailIdx}\ i\ f)$$

List.modifyTailIdx_eq_take_drop theorem

(f : List α → List α) (H : f [] = []) : ∀ (l : List α) i, l.modifyTailIdx i f = l.take i ++ f (l.drop i)

Full source

theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
    ∀ (l : List α) i, l.modifyTailIdx i f = l.take i ++ f (l.drop i)
  | _, 0 => rfl
  | [], _ + 1 => H.symm
  | b :: l, i + 1 => congrArg (cons b) (modifyTailIdx_eq_take_drop f H l i)

Decomposition of `modifyTailIdx` into `take` and `drop` operations

Informal description

For any function $f$ on lists of type $\alpha$ that preserves the empty list (i.e., $f([]) = []$), any list $l$ of type $\alpha$, and any natural number $i$, the operation `modifyTailIdx` applied to $l$ at index $i$ with function $f$ is equal to the concatenation of the first $i$ elements of $l$ with $f$ applied to the remaining elements of $l$ after dropping the first $i$ elements. In other words, $l.\text{modifyTailIdx}\ i\ f = l.\text{take}\ i +\!\!+ f(l.\text{drop}\ i)$.

List.exists_of_modifyTailIdx theorem

 (f : List α → List α) {i} {l : List α} (h : i ≤ l.length) :
  ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i ∧ l.modifyTailIdx i f = l₁ ++ f l₂

Full source

theorem exists_of_modifyTailIdx (f : List α → List α) {i} {l : List α} (h : i ≤ l.length) :
    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i ∧ l.modifyTailIdx i f = l₁ ++ f l₂ := by
  obtain ⟨l₁, l₂, rfl, rfl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i :=
    ⟨_, _, (take_append_drop i l).symm, length_take_of_le h⟩
  exact ⟨l₁, l₂, rfl, rfl, modifyTailIdx_add f 0 l₁ l₂⟩

Decomposition of List Modification at Index $i$ into Prefix and Modified Suffix

Informal description

For any function $f$ on lists of type $\alpha$, any natural number $i$, and any list $l$ of type $\alpha$ with $i \leq \text{length}(l)$, there exist sublists $l_1$ and $l_2$ such that: 1. $l = l_1 \mathbin{+\kern-0.5em+} l_2$ (the list $l$ is the concatenation of $l_1$ and $l_2$), 2. $\text{length}(l_1) = i$ (the length of $l_1$ is exactly $i$), and 3. $l.\text{modifyTailIdx}\ i\ f = l_1 \mathbin{+\kern-0.5em+} f(l_2)$ (modifying the tail of $l$ starting at index $i$ with $f$ is equivalent to concatenating $l_1$ with $f$ applied to $l_2$).

List.modifyTailIdx_modifyTailIdx theorem

 {f g : List α → List α} (i : Nat) :
  ∀ (j) (l : List α),
    (l.modifyTailIdx j f).modifyTailIdx (i + j) g = l.modifyTailIdx j (fun l => (f l).modifyTailIdx i g)

Full source

theorem modifyTailIdx_modifyTailIdx {f g : List α → List α} (i : Nat) :
    ∀ (j) (l : List α),
      (l.modifyTailIdx j f).modifyTailIdx (i + j) g =
        l.modifyTailIdx j (fun l => (f l).modifyTailIdx i g)
  | 0, _ => rfl
  | _ + 1, [] => rfl
  | n + 1, a :: l => congrArg (List.cons a) (modifyTailIdx_modifyTailIdx i n l)

Composition of List Tail Modifications at Different Indices

Informal description

For any two functions $f, g : \text{List } \alpha \to \text{List } \alpha$, natural number $i$, and list $l : \text{List } \alpha$, the following equality holds for all natural numbers $j$: $$(l.\text{modifyTailIdx } j f).\text{modifyTailIdx } (i + j) g = l.\text{modifyTailIdx } j \left( \lambda l' \mapsto (f l').\text{modifyTailIdx } i g \right)$$

List.modifyTailIdx_modifyTailIdx_le theorem

 {f g : List α → List α} (i j : Nat) (l : List α) (h : j ≤ i) :
  (l.modifyTailIdx j f).modifyTailIdx i g = l.modifyTailIdx j (fun l => (f l).modifyTailIdx (i - j) g)

Full source

theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (i j : Nat) (l : List α)
    (h : j ≤ i) :
    (l.modifyTailIdx j f).modifyTailIdx i g =
      l.modifyTailIdx j (fun l => (f l).modifyTailIdx (i - j) g) := by
  rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
  rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]

Composition of List Tail Modifications with Index Shift when $j \leq i$

Informal description

For any two functions $f, g : \text{List } \alpha \to \text{List } \alpha$, natural numbers $i, j$, and list $l : \text{List } \alpha$ such that $j \leq i$, the following equality holds: $$(l.\text{modifyTailIdx } j f).\text{modifyTailIdx } i g = l.\text{modifyTailIdx } j \left( \lambda l' \mapsto (f l').\text{modifyTailIdx } (i - j) g \right)$$

List.modifyTailIdx_modifyTailIdx_self theorem

 {f g : List α → List α} (i : Nat) (l : List α) : (l.modifyTailIdx i f).modifyTailIdx i g = l.modifyTailIdx i (g ∘ f)

Full source

theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (l : List α) :
    (l.modifyTailIdx i f).modifyTailIdx i g = l.modifyTailIdx i (g ∘ f) := by
  rw [modifyTailIdx_modifyTailIdx_le i i l (Nat.le_refl i), Nat.sub_self]; rfl

Composition of List Tail Modifications at Same Index

Informal description

For any two functions $f, g : \text{List } \alpha \to \text{List } \alpha$, natural number $i$, and list $l : \text{List } \alpha$, the following equality holds: $$(l.\text{modifyTailIdx } i f).\text{modifyTailIdx } i g = l.\text{modifyTailIdx } i (g \circ f)$$

List.modify_nil theorem

(f : α → α) (i) : [].modify i f = []

Full source

@[simp] theorem modify_nil (f : α → α) (i) : [].modify i f = [] := by cases i <;> rfl

Modification of Empty List is Empty

Informal description

For any function $f : \alpha \to \alpha$ and any natural number index $i$, modifying the empty list $[]$ at index $i$ with $f$ results in the empty list $[]$.

List.modify_zero_cons theorem

(f : α → α) (a : α) (l : List α) : (a :: l).modify 0 f = f a :: l

Full source

@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
    (a :: l).modify 0 f = f a :: l := rfl

Modification of First Element in Cons List

Informal description

For any function $f : \alpha \to \alpha$, element $a \in \alpha$, and list $l$ of elements of type $\alpha$, modifying the first element (index 0) of the list $a :: l$ with $f$ results in the list $f(a) :: l$. That is, $(a :: l).\text{modify}\,0\,f = f(a) :: l$.

List.modify_succ_cons theorem

(f : α → α) (a : α) (l : List α) (i) : (a :: l).modify (i + 1) f = a :: l.modify i f

Full source

@[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
    (a :: l).modify (i + 1) f = a :: l.modify i f := by rfl

Modification of Successor Index in List Cons

Informal description

For any function $f : \alpha \to \alpha$, element $a \in \alpha$, list $L$ of elements of type $\alpha$, and natural number index $i$, modifying the $(i+1)$-th element of the list $a :: L$ with $f$ is equivalent to prepending $a$ to the list obtained by modifying the $i$-th element of $L$ with $f$. More precisely: \[ \text{modify}(a :: L, i+1, f) = a :: \text{modify}(L, i, f). \]

List.modifyHead_eq_modify_zero theorem

(f : α → α) (l : List α) : l.modifyHead f = l.modify 0 f

Full source

theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
    l.modifyHead f = l.modify 0 f := by cases l <;> simp

Equivalence of Head Modification and Zero-Index Modification in Lists

Informal description

For any function $f : \alpha \to \alpha$ and any list $L$ of elements of type $\alpha$, modifying the head of $L$ with $f$ is equivalent to modifying the element at index $0$ of $L$ with $f$. That is, $\text{modifyHead}\,f\,L = \text{modify}\,L\,0\,f$.

List.modify_eq_nil_iff theorem

{f : α → α} {i} {l : List α} : l.modify i f = [] ↔ l = []

Full source

@[simp] theorem modify_eq_nil_iff {f : α → α} {i} {l : List α} :
    l.modify i f = [] ↔ l = [] := by cases l <;> cases i <;> simp

Empty List Modification Equivalence: $\text{modify}(L, i, f) = [] \leftrightarrow L = []$

Informal description

For any function $f : \alpha \to \alpha$, natural number index $i$, and list $L$ of elements of type $\alpha$, modifying the $i$-th element of $L$ with $f$ results in the empty list if and only if $L$ itself is the empty list. In other words: \[ \text{modify}(L, i, f) = [] \leftrightarrow L = []. \]

List.getElem?_modify theorem

(f : α → α) : ∀ i (l : List α) j, (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?

Full source

theorem getElem?_modify (f : α → α) :
    ∀ i (l : List α) j, (l.modify i f)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
  | n, l, 0 => by cases l <;> cases n <;> simp
  | n, [], _+1 => by cases n <;> rfl
  | 0, _ :: l, j+1 => by cases h : l[j]? <;> simp [h, modify, j.succ_ne_zero.symm]
  | i+1, a :: l, j+1 => by
    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
    refine (getElem?_modify f i l j).trans ?_
    cases h' : l[j]? <;> by_cases h : i = j <;>
      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']

Optional Indexing of Modified List: $(l.\text{modify}\,i\,f)[j]? = (\lambda a.\,\text{if }i=j\text{ then }f\,a\text{ else }a) <\$> l[j]?$

Informal description

For any function $f : \alpha \to \alpha$, natural numbers $i$ and $j$, and list $l$ of type $\text{List}\,\alpha$, the optional indexing operation on the modified list $\text{modify}\,l\,i\,f$ at position $j$ is equal to applying the function $\lambda a.\,\text{if }i = j\text{ then }f\,a\text{ else }a$ to the optionally indexed element $l[j]?$. In other words: $$(l.\text{modify}\,i\,f)[j]? = \begin{cases} \text{some}\,(f\,a) & \text{if }i = j\text{ and }l[j]? = \text{some}\,a \\ \text{some}\,a & \text{if }i \neq j\text{ and }l[j]? = \text{some}\,a \\ \text{none} & \text{if }l[j]? = \text{none} \end{cases}$$

List.length_modify theorem

(f : α → α) : ∀ (l : List α) i, (l.modify i f).length = l.length

Full source

@[simp] theorem length_modify (f : α → α) : ∀ (l : List α) i, (l.modify i f).length = l.length :=
  length_modifyTailIdx _ fun l => by cases l <;> rfl

Length Preservation under List Modification: $\text{length}(\text{modify}\ L\ i\ f) = \text{length}(L)$

Informal description

For any function $f : \alpha \to \alpha$, any list $L$ of elements of type $\alpha$, and any natural number index $i$, the length of the list obtained by modifying the element at position $i$ in $L$ with $f$ is equal to the length of $L$. That is, $\text{length}(\text{modify}\ L\ i\ f) = \text{length}(L)$.

List.getElem?_modify_eq theorem

(f : α → α) (i) (l : List α) : (l.modify i f)[i]? = f <$> l[i]?

Full source

@[simp] theorem getElem?_modify_eq (f : α → α) (i) (l : List α) :
    (l.modify i f)[i]? = f <$> l[i]? := by
  simp only [getElem?_modify, if_pos]

Optional Indexing at Modified Position: $(l.\text{modify}\,i\,f)[i]? = f <\$> l[i]?$

Informal description

For any function $f : \alpha \to \alpha$, any natural number index $i$, and any list $l$ of type $\text{List}\,\alpha$, the optional indexing operation on the modified list $\text{modify}\,l\,i\,f$ at position $i$ is equal to applying $f$ to the optionally indexed element $l[i]?$. In other words: $$(l.\text{modify}\,i\,f)[i]? = \begin{cases} \text{some}\,(f\,a) & \text{if }l[i]? = \text{some}\,a \\ \text{none} & \text{if }l[i]? = \text{none} \end{cases}$$

List.getElem?_modify_ne theorem

(f : α → α) {i j} (l : List α) (h : i ≠ j) : (l.modify i f)[j]? = l[j]?

Full source

@[simp] theorem getElem?_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) :
    (l.modify i f)[j]? = l[j]? := by
  simp only [getElem?_modify, if_neg h, id_map']

Optional Index Unchanged by Distant Modification: $(\text{modify}\ l\ i\ f)[j]? = l[j]?$ when $i \neq j$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any distinct indices $i$ and $j$, the optional element at position $j$ in the modified list $\text{modify}\ l\ i\ f$ is equal to the optional element at position $j$ in the original list $l$. That is, $(\text{modify}\ l\ i\ f)[j]? = l[j]?$.

List.getElem_modify theorem

 (f : α → α) (i) (l : List α) (j) (h : j < (l.modify i f).length) :
  (l.modify i f)[j] = if i = j then f (l[j]'(by simp at h; omega)) else l[j]'(by simp at h; omega)

Full source

theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (l.modify i f).length) :
    (l.modify i f)[j] =
      if i = j then f (l[j]'(by simp at h; omega)) else l[j]'(by simp at h; omega) := by
  rw [getElem_eq_iff, getElem?_modify]
  simp at h
  simp [h]

Element-wise Modification of List: $(l.\text{modify}\,i\,f)[j] = f(l[j])$ if $i = j$, else $l[j]$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of type $\text{List}\,\alpha$, and any indices $i, j$ with $j < \text{length}(l.\text{modify}\,i\,f)$, the element at position $j$ in the modified list is given by: $$(l.\text{modify}\,i\,f)[j] = \begin{cases} f(l[j]) & \text{if } i = j \\ l[j] & \text{if } i \neq j \end{cases}$$

List.getElem_modify_eq theorem

(f : α → α) (i) (l : List α) (h) : (l.modify i f)[i] = f (l[i]'(by simpa using h))

Full source

@[simp] theorem getElem_modify_eq (f : α → α) (i) (l : List α) (h) :
    (l.modify i f)[i] = f (l[i]'(by simpa using h)) := by simp [getElem_modify]

Modification at Index: $(\text{modify}\,l\,i\,f)[i] = f(l[i])$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any index $i$ such that $i$ is a valid index for $l$, the element at position $i$ in the modified list $\text{modify}\,l\,i\,f$ is equal to $f$ applied to the element at position $i$ in the original list $l$. That is, $(\text{modify}\,l\,i\,f)[i] = f(l[i])$.

List.getElem_modify_ne theorem

(f : α → α) {i j} (l : List α) (h : i ≠ j) (h') : (l.modify i f)[j] = l[j]'(by simpa using h')

Full source

@[simp] theorem getElem_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) (h') :
    (l.modify i f)[j] = l[j]'(by simpa using h') := by simp [getElem_modify, h]

Preservation of List Elements under Modification at Distinct Indices: $(l.\text{modify}\,i\,f)[j] = l[j]$ for $i \neq j$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of type $\text{List}\,\alpha$, and any distinct indices $i$ and $j$ with $j < \text{length}(l.\text{modify}\,i\,f)$, the element at position $j$ in the modified list is equal to the original element at position $j$, i.e., $$(l.\text{modify}\,i\,f)[j] = l[j].$$

List.modify_eq_self theorem

{f : α → α} {i} {l : List α} (h : l.length ≤ i) : l.modify i f = l

Full source

theorem modify_eq_self {f : α → α} {i} {l : List α} (h : l.length ≤ i) :
    l.modify i f = l := by
  apply ext_getElem
  · simp
  · intro m h₁ h₂
    simp only [getElem_modify, ite_eq_right_iff]
    intro h
    omega

List Modification at Out-of-Bounds Index Preserves List

Informal description

For any function $f : \alpha \to \alpha$, any index $i$, and any list $l$ of elements of type $\alpha$, if the length of $l$ is less than or equal to $i$, then modifying $l$ at index $i$ with $f$ leaves the list unchanged, i.e., $l.\text{modify}\,i\,f = l$.

List.modify_modify_eq theorem

(f g : α → α) (i) (l : List α) : (l.modify i f).modify i g = l.modify i (g ∘ f)

Full source

theorem modify_modify_eq (f g : α → α) (i) (l : List α) :
    (l.modify i f).modify i g = l.modify i (g ∘ f) := by
  apply ext_getElem
  · simp
  · intro m h₁ h₂
    simp only [getElem_modify, Function.comp_apply]
    split <;> simp

Composition of List Modifications at Same Index: $(l.\text{modify}\,i\,f).\text{modify}\,i\,g = l.\text{modify}\,i\,(g \circ f)$

Informal description

For any functions $f, g : \alpha \to \alpha$, any natural number index $i$, and any list $l$ of elements of type $\alpha$, modifying the list $l$ at index $i$ first with $f$ and then with $g$ is equivalent to modifying $l$ at index $i$ with the composition $g \circ f$. That is, $$(l.\text{modify}\,i\,f).\text{modify}\,i\,g = l.\text{modify}\,i\,(g \circ f).$$

List.modify_modify_ne theorem

(f g : α → α) {i j} (l : List α) (h : i ≠ j) : (l.modify i f).modify j g = (l.modify j g).modify i f

Full source

theorem modify_modify_ne (f g : α → α) {i j} (l : List α) (h : i ≠ j) :
    (l.modify i f).modify j g = (l.modify j g).modify i f := by
  apply ext_getElem
  · simp
  · intro m' h₁ h₂
    simp only [getElem_modify, getElem_modify_ne, h₂]
    split <;> split <;> first | rfl | omega

Commutativity of List Modifications at Distinct Indices

Informal description

For any functions $f, g : \alpha \to \alpha$, any distinct indices $i \neq j$, and any list $l$ of elements of type $\alpha$, modifying the list $l$ at index $i$ with $f$ and then at index $j$ with $g$ is equivalent to first modifying at $j$ with $g$ and then at $i$ with $f$. That is, $$(l.\text{modify}\,i\,f).\text{modify}\,j\,g = (l.\text{modify}\,j\,g).\text{modify}\,i\,f.$$

List.modify_eq_set theorem

[Inhabited α] (f : α → α) (i) (l : List α) : l.modify i f = l.set i (f (l[i]?.getD default))

Full source

theorem modify_eq_set [Inhabited α] (f : α → α) (i) (l : List α) :
    l.modify i f = l.set i (f (l[i]?.getD default)) := by
  apply ext_getElem
  · simp
  · intro m h₁ h₂
    simp [getElem_modify, getElem_set, h₂]
    split <;> rename_i h
    · subst h
      simp only [length_modify] at h₁
      simp [h₁]
    · rfl

List Modification via Element Replacement: $\text{modify}\,l\,i\,f = \text{set}\,l\,i\,(f\,(l[i]\,\text{or default}))$

Informal description

Let $\alpha$ be a type with a default element. For any function $f : \alpha \to \alpha$, any index $i \in \mathbb{N}$, and any list $l$ of elements of type $\alpha$, modifying the list at index $i$ with $f$ is equivalent to replacing the element at index $i$ with $f$ applied to the original element (or the default value if the index is out of bounds). That is, $$ l.\text{modify}\,i\,f = l.\text{set}\,i\,(f\,(l[i]?.\text{getD}\,\text{default})). $$

List.modify_eq_take_drop theorem

(f : α → α) : ∀ (l : List α) i, l.modify i f = l.take i ++ modifyHead f (l.drop i)

Full source

theorem modify_eq_take_drop (f : α → α) :
    ∀ (l : List α) i, l.modify i f = l.take i ++ modifyHead f (l.drop i) :=
  modifyTailIdx_eq_take_drop _ rfl

Decomposition of List Modification via Take and Drop Operations

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any natural number index $i$, the modified list obtained by applying $f$ to the element at position $i$ in $l$ is equal to the concatenation of the first $i$ elements of $l$ with the result of applying $f$ to the head of the remaining elements after dropping the first $i$ elements. More precisely: \[ \text{modify}\ l\ i\ f = \text{take}\ i\ l +\!\!+ \text{modifyHead}\ f\ (\text{drop}\ i\ l) \]

List.modify_eq_take_cons_drop theorem

{f : α → α} {i} {l : List α} (h : i < l.length) : l.modify i f = l.take i ++ f l[i] :: l.drop (i + 1)

Full source

theorem modify_eq_take_cons_drop {f : α → α} {i} {l : List α} (h : i < l.length) :
    l.modify i f = l.take i ++ f l[i] :: l.drop (i + 1) := by
  rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl

List Modification Decomposition: $\text{modify}\ l\ i\ f = \text{take}\ i\ l +\!\!+ [f\ l[i]] +\!\!+ \text{drop}\ (i+1)\ l$

Informal description

For any function $f : \alpha \to \alpha$, any natural number index $i$, and any list $l$ of elements of type $\alpha$ such that $i < \text{length}(l)$, the modified list obtained by applying $f$ to the element at position $i$ in $l$ is equal to the concatenation of: 1. The first $i$ elements of $l$ ($\text{take}\ i\ l$), 2. The result of applying $f$ to the $i$-th element of $l$ ($f\ l[i]$), and 3. The remaining elements after the $(i+1)$-th position ($\text{drop}\ (i+1)\ l$). In symbols: \[ \text{modify}\ l\ i\ f = (\text{take}\ i\ l) +\!\!+ [f\ l[i]] +\!\!+ (\text{drop}\ (i+1)\ l) \]

List.exists_of_modify theorem

 (f : α → α) {i} {l : List α} (h : i < l.length) :
  ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ l.modify i f = l₁ ++ f a :: l₂

Full source

theorem exists_of_modify (f : α → α) {i} {l : List α} (h : i < l.length) :
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ l.modify i f = l₁ ++ f a :: l₂ :=
  match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
  | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
  | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)

Decomposition of List Modification into Prefix, Modified Element, and Suffix

Informal description

For any function $f : \alpha \to \alpha$, any natural number $i$, and any list $l$ of elements of type $\alpha$ such that $i < \text{length}(l)$, there exist sublists $l_1, l_2$ and an element $a$ such that: 1. $l = l_1 \mathbin{+\kern-0.5em+} [a] \mathbin{+\kern-0.5em+} l_2$ (the list $l$ is the concatenation of $l_1$, the singleton list $[a]$, and $l_2$), 2. $\text{length}(l_1) = i$ (the length of $l_1$ is exactly $i$), and 3. $\text{modify}\ l\ i\ f = l_1 \mathbin{+\kern-0.5em+} [f(a)] \mathbin{+\kern-0.5em+} l_2$ (modifying the list $l$ at index $i$ with $f$ is equivalent to concatenating $l_1$ with the modified element $f(a)$ and $l_2$).

List.modify_id theorem

(i) (l : List α) : l.modify i id = l

Full source

@[simp] theorem modify_id (i) (l : List α) : l.modify i id = l := by
  simp [modify]

Identity Function Preserves List Modification at Index

Informal description

For any natural number $i$ and any list $l$ of elements of type $\alpha$, applying the `modify` operation with the identity function $\text{id}$ at index $i$ leaves the list unchanged, i.e., $\text{modify } l \ i \ \text{id} = l$.

List.take_modify theorem

(f : α → α) (i j) (l : List α) : (l.modify i f).take j = (l.take j).modify i f

Full source

theorem take_modify (f : α → α) (i j) (l : List α) :
    (l.modify i f).take j = (l.take j).modify i f := by
  induction j generalizing l i with
  | zero => simp
  | succ n ih =>
    cases l with
    | nil => simp
    | cons hd tl =>
      cases i with
      | zero => simp
      | succ i => simp [ih]

Commutation of List Modification and Taking Prefix: $\text{take}_j \circ \text{modify}_i = \text{modify}_i \circ \text{take}_j$

Informal description

For any function $f : \alpha \to \alpha$, natural numbers $i$ and $j$, and list $l$ of elements of type $\alpha$, taking the first $j$ elements of the list modified at index $i$ with $f$ is equal to modifying the first $j$ elements of $l$ at index $i$ with $f$. In other words: \[ \text{take}_j (\text{modify}_i\ f\ l) = \text{modify}_i\ f\ (\text{take}_j\ l) \]

List.drop_modify_of_lt theorem

(f : α → α) (i j) (l : List α) (h : i < j) : (l.modify i f).drop j = l.drop j

Full source

theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
    (l.modify i f).drop j = l.drop j := by
  apply ext_getElem
  · simp
  · intro m' h₁ h₂
    simp only [getElem_drop, getElem_modify, ite_eq_right_iff]
    intro h'
    omega

List Drop Invariance Under Modification at Smaller Index: $i < j \implies \text{drop}_j \circ \text{modify}_i = \text{drop}_j$

Informal description

For any function $f : \alpha \to \alpha$, any natural numbers $i$ and $j$, and any list $l$ of elements of type $\alpha$, if $i < j$, then dropping the first $j$ elements from the list modified at index $i$ with $f$ is equal to dropping the first $j$ elements from the original list $l$. That is, $$(\text{modify}\ l\ i\ f).\text{drop}\ j = l.\text{drop}\ j.$$

List.drop_modify_of_ge theorem

(f : α → α) (i j) (l : List α) (h : i ≥ j) : (l.modify i f).drop j = (l.drop j).modify (i - j) f

Full source

theorem drop_modify_of_ge (f : α → α) (i j) (l : List α) (h : i ≥ j) :
    (l.modify i f).drop j = (l.drop j).modify (i - j) f  := by
  apply ext_getElem
  · simp
  · intro m' h₁ h₂
    simp [getElem_drop, getElem_modify, ite_eq_right_iff]
    split <;> split <;> first | rfl | omega

Modification-Drop Commutation for Lists: $\text{drop}_j \circ \text{modify}_i = \text{modify}_{i-j} \circ \text{drop}_j$ when $i \geq j$

Informal description

For any function $f : \alpha \to \alpha$, natural numbers $i$ and $j$, and list $l$ of elements of type $\alpha$, if $i \geq j$, then dropping the first $j$ elements of the list modified at index $i$ with $f$ is equal to modifying the list obtained by dropping the first $j$ elements of $l$ at index $i - j$ with $f$. In other words: \[ \text{drop}_j (\text{modify}_i\ f\ l) = \text{modify}_{i-j}\ f\ (\text{drop}_j\ l) \]

List.eraseIdx_modify_of_eq theorem

(f : α → α) (i) (l : List α) : (l.modify i f).eraseIdx i = l.eraseIdx i

Full source

theorem eraseIdx_modify_of_eq (f : α → α) (i) (l : List α) :
    (l.modify i f).eraseIdx i = l.eraseIdx i := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro m h₁ h₂
    simp only [getElem_eraseIdx, getElem_modify]
    split <;> split <;> first | rfl | omega

Modification Followed by Removal at Same Index Equals Direct Removal

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any index $i$, the operation of first modifying the $i$-th element of $l$ with $f$ and then removing the $i$-th element yields the same result as directly removing the $i$-th element from $l$. In other words, $(l.\text{modify}\,i\,f).\text{eraseIdx}\,i = l.\text{eraseIdx}\,i$.

List.eraseIdx_modify_of_lt theorem

(f : α → α) (i j) (l : List α) (h : j < i) : (l.modify i f).eraseIdx j = (l.eraseIdx j).modify (i - 1) f

Full source

theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (l.modify i f).eraseIdx j = (l.eraseIdx j).modify (i - 1) f := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro k h₁ h₂
    simp only [getElem_eraseIdx, getElem_modify]
    by_cases h' : i - 1 = k
    repeat' split
    all_goals (first | rfl | omega)

Commutativity of List Modification and Removal: $(l.\text{modify}\,i\,f).\text{eraseIdx}\,j = (l.\text{eraseIdx}\,j).\text{modify}\,(i-1)\,f$ when $j < i$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any indices $i, j$ with $j < i$, the following equality holds: $$(l.\text{modify}\,i\,f).\text{eraseIdx}\,j = (l.\text{eraseIdx}\,j).\text{modify}\,(i-1)\,f$$ where: - $\text{modify}\,i\,f$ modifies the element at position $i$ by applying $f$, - $\text{eraseIdx}\,j$ removes the element at position $j$, - $j < i$ ensures the modification and removal operations are performed in the correct order.

List.eraseIdx_modify_of_gt theorem

(f : α → α) (i j) (l : List α) (h : j > i) : (l.modify i f).eraseIdx j = (l.eraseIdx j).modify i f

Full source

theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
    (l.modify i f).eraseIdx j = (l.eraseIdx j).modify i f := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro k h₁ h₂
    simp only [getElem_eraseIdx, getElem_modify]
    by_cases h' : i = k
    repeat' split
    all_goals (first | rfl | omega)

Commutativity of List Modification and Element Removal for $j > i$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any indices $i, j$ with $j > i$, the following equality holds: $$(l.\text{modify}\,i\,f).\text{eraseIdx}\,j = (l.\text{eraseIdx}\,j).\text{modify}\,i\,f$$

List.modify_eraseIdx_of_lt theorem

(f : α → α) (i j) (l : List α) (h : j < i) : (l.eraseIdx i).modify j f = (l.modify j f).eraseIdx i

Full source

theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (l.eraseIdx i).modify j f = (l.modify j f).eraseIdx i := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro k h₁ h₂
    simp only [getElem_eraseIdx, getElem_modify]
    by_cases h' : j = k + 1
    repeat' split
    all_goals (first | rfl | omega)

Commutativity of List Modification and Element Removal for $j < i$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any indices $i, j$ with $j < i$, the following equality holds: $$(l.\text{eraseIdx}\,i).\text{modify}\,j\,f = (l.\text{modify}\,j\,f).\text{eraseIdx}\,i$$

List.modify_eraseIdx_of_ge theorem

(f : α → α) (i j) (l : List α) (h : j ≥ i) : (l.eraseIdx i).modify j f = (l.modify (j + 1) f).eraseIdx i

Full source

theorem modify_eraseIdx_of_ge (f : α → α) (i j) (l : List α) (h : j ≥ i) :
    (l.eraseIdx i).modify j f = (l.modify (j + 1) f).eraseIdx i := by
  apply ext_getElem
  · simp [length_eraseIdx]
  · intro k h₁ h₂
    simp only [getElem_eraseIdx, getElem_modify]
    by_cases h' : j + 1 = k + 1
    repeat' split
    all_goals (first | rfl | omega)

Commutativity of List Modification and Element Removal for $j \geq i$

Informal description

For any function $f : \alpha \to \alpha$, any list $l$ of elements of type $\alpha$, and any indices $i, j$ with $j \geq i$, the following equality holds: $$(l.\text{eraseIdx}\,i).\text{modify}\,j\,f = (l.\text{modify}\,(j+1)\,f).\text{eraseIdx}\,i$$