Mathlib.Data.List.InsertIdx

List.sublist_insertIdx theorem

(l : List α) (n : ℕ) (a : α) : l <+ (l.insertIdx n a)

Full source

@[simp]
theorem sublist_insertIdx (l : List α) (n : ℕ) (a : α) : l <+ (l.insertIdx n a) := by
  simpa only [eraseIdx_insertIdx] using eraseIdx_sublist (l.insertIdx n a) n

Sublist Property of List Insertion at Index

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $n$, and any element $a$ of type $\alpha$, the list $l$ is a sublist of the list obtained by inserting $a$ at position $n$ in $l$.

List.subset_insertIdx theorem

(l : List α) (n : ℕ) (a : α) : l ⊆ l.insertIdx n a

Full source

@[simp]
theorem subset_insertIdx (l : List α) (n : ℕ) (a : α) : l ⊆ l.insertIdx n a :=
  (sublist_insertIdx ..).subset

Subset Property of List Insertion at Index

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $n$, and any element $a$ of type $\alpha$, the list $l$ is a subset of the list obtained by inserting $a$ at position $n$ in $l$.

List.insertIdx_eraseIdx theorem

{l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) : (l.eraseIdx n).insertIdx n a = l.set n a

Full source

/-- Erasing `n`th element of a list, then inserting `a` at the same place
is the same as setting `n`th element to `a`.

We assume that `n ≠ length l`, because otherwise LHS equals `l ++ [a]` while RHS equals `l`. -/
@[simp]
theorem insertIdx_eraseIdx {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
    (l.eraseIdx n).insertIdx n a = l.set n a := by
  induction n generalizing l <;> cases l <;> simp_all

Inserting After Erasing Equals Setting: $(l.\text{eraseIdx}\,n).\text{insertIdx}\,n\,a = l.\text{set}\,n\,a$ when $n \neq \text{length}\,l$

Informal description

For any list $l$ of type $\alpha$, natural number $n$, and element $a$ of type $\alpha$, if $n$ is not equal to the length of $l$, then inserting $a$ at position $n$ in the list obtained by erasing the $n$-th element of $l$ is equal to setting the $n$-th element of $l$ to $a$.

List.insertIdx_eraseIdx_getElem theorem

{l : List α} {n : ℕ} (hn : n < length l) : (l.eraseIdx n).insertIdx n l[n] = l

Full source

theorem insertIdx_eraseIdx_getElem {l : List α} {n : ℕ} (hn : n < length l) :
    (l.eraseIdx n).insertIdx n l[n] = l := by
  simp [hn.ne]

Reconstruction of List via Insertion and Erasure: $(l.\text{eraseIdx}\,n).\text{insertIdx}\,n\,l[n] = l$ for $n < \text{length}\,l$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n$ is less than the length of $l$, inserting the $n$-th element of $l$ at position $n$ in the list obtained by erasing the $n$-th element of $l$ results in the original list $l$. That is, $(l.\text{eraseIdx}\,n).\text{insertIdx}\,n\,l[n] = l$.

List.insertIdx_subset_cons theorem

(n : ℕ) (a : α) (l : List α) : l.insertIdx n a ⊆ a :: l

Full source

theorem insertIdx_subset_cons (n : ℕ) (a : α) (l : List α) : l.insertIdx n a ⊆ a :: l := by
  intro b hb
  simpa using eq_or_mem_of_mem_insertIdx hb

Inserted List is Subset of Prepended List

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the list obtained by inserting $a$ at index $n$ in $l$ is a subset of the list obtained by prepending $a$ to $l$.

List.insertIdx_pmap theorem

 {p : α → Prop} (f : ∀ a, p a → β) {l : List α} {a : α} {n : ℕ} (hl : ∀ x ∈ l, p x) (ha : p a) :
  (l.pmap f hl).insertIdx n (f a ha) =
    (l.insertIdx n a).pmap f (fun _ h ↦ (eq_or_mem_of_mem_insertIdx h).elim (fun heq ↦ heq ▸ ha) (hl _))

Full source

theorem insertIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} {a : α} {n : ℕ}
    (hl : ∀ x ∈ l, p x) (ha : p a) :
    (l.pmap f hl).insertIdx n (f a ha) = (l.insertIdx n a).pmap f
      (fun _ h ↦ (eq_or_mem_of_mem_insertIdx h).elim (fun heq ↦ heq ▸ ha) (hl _)) := by
  induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all

Commutativity of `insertIdx` and `pmap` for Lists with Predicate

Informal description

Let $p$ be a predicate on elements of type $\alpha$, and let $f : \forall a, p(a) \to \beta$ be a function that maps elements satisfying $p$ to type $\beta$. Given a list $l$ of elements of type $\alpha$, an element $a$ of type $\alpha$, and a natural number $n$, if every element $x$ in $l$ satisfies $p(x)$ and $a$ satisfies $p(a)$, then the following equality holds: \[ (l.\mathrm{pmap}\, f\, hl).\mathrm{insertIdx}\, n\, (f\, a\, ha) = (l.\mathrm{insertIdx}\, n\, a).\mathrm{pmap}\, f\, \left(\lambda \_ h \mapsto (\mathrm{eq\_or\_mem\_of\_mem\_insertIdx}\, h).\mathrm{elim}\, (\lambda heq \mapsto heq \triangleright ha)\, (hl\, \_)\right) \] where $hl$ is a proof that all elements in $l$ satisfy $p$, and $ha$ is a proof that $a$ satisfies $p$.

List.map_insertIdx theorem

(f : α → β) (l : List α) (n : ℕ) (a : α) : (l.insertIdx n a).map f = (l.map f).insertIdx n (f a)

Full source

theorem map_insertIdx (f : α → β) (l : List α) (n : ℕ) (a : α) :
    (l.insertIdx n a).map f = (l.map f).insertIdx n (f a) := by
  simpa only [pmap_eq_map] using (insertIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) trivial).symm

Commutativity of Map and Insert at Index for Lists

Informal description

For any function $f : \alpha \to \beta$, list $l$ of elements of type $\alpha$, natural number $n$, and element $a : \alpha$, the following equality holds: \[ \text{map}\, f\, (l.\text{insertIdx}\, n\, a) = (\text{map}\, f\, l).\text{insertIdx}\, n\, (f\, a) \] where $\text{map}$ applies $f$ to each element of the list, and $\text{insertIdx}$ inserts an element at the specified index in the list.

List.eraseIdx_pmap theorem

 {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl : ∀ a ∈ l, p a) (n : ℕ) :
  (pmap f l hl).eraseIdx n = (l.eraseIdx n).pmap f fun a ha ↦ hl a (eraseIdx_subset ha)

Full source

theorem eraseIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl : ∀ a ∈ l, p a) (n : ℕ) :
    (pmap f l hl).eraseIdx n = (l.eraseIdx n).pmap f fun a ha ↦ hl a (eraseIdx_subset ha) :=
  match l, hl, n with
  | [], _, _ => rfl
  | a :: _, _, 0 => rfl
  | a :: as, h, n + 1 => by rw [forall_mem_cons] at h; simp [eraseIdx_pmap f h.2 n]

Partial Map Commutes with Erase at Index

Informal description

Let $p$ be a predicate on elements of type $\alpha$, and let $f : \forall a, p(a) \to \beta$ be a function that maps elements satisfying $p$ to $\beta$. Given a list $l$ of elements of type $\alpha$ where every element $a \in l$ satisfies $p(a)$, and given an index $n$, the following equality holds: $$(\text{pmap}\, f\, l\, hl).\text{eraseIdx}\, n = (\text{pmap}\, f\, (l.\text{eraseIdx}\, n)\, (\lambda a\, ha, hl\, a\, (\text{eraseIdx\_subset}\, ha)))$$ where $\text{pmap}$ is the partial map operation, $\text{eraseIdx}$ removes the element at index $n$, and $\text{eraseIdx\_subset}$ ensures that the erased element was originally in the list.

List.eraseIdx_map theorem

(f : α → β) (l : List α) (n : ℕ) : (map f l).eraseIdx n = (l.eraseIdx n).map f

Full source

/-- Erasing an index commutes with `List.map`. -/
theorem eraseIdx_map (f : α → β) (l : List α) (n : ℕ) :
    (map f l).eraseIdx n = (l.eraseIdx n).map f := by
  simpa only [pmap_eq_map] using eraseIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) n

List Mapping Commutes with Erase at Index

Informal description

For any function $f : \alpha \to \beta$, any list $l$ of elements of type $\alpha$, and any index $n$, the following equality holds: $$(f \circ l).\text{eraseIdx}\, n = f \circ (l.\text{eraseIdx}\, n)$$ where $\circ$ denotes list mapping and $\text{eraseIdx}\, n$ removes the element at index $n$.

List.insertIdx_injective theorem

(n : ℕ) (x : α) : Function.Injective (fun l : List α => l.insertIdx n x)

Full source

theorem insertIdx_injective (n : ℕ) (x : α) :
    Function.Injective (fun l : List α => l.insertIdx n x) := by
  induction n with
  | zero => simp
  | succ n IH => rintro (_ | ⟨a, as⟩) (_ | ⟨b, bs⟩) h <;> simpa [IH.eq_iff] using h

Injectivity of List Insertion at Fixed Index

Informal description

For any natural number $n$ and element $x$ of type $\alpha$, the function that inserts $x$ at index $n$ in a list is injective. That is, for any lists $l_1, l_2 : \text{List}\,\alpha$, if $l_1.\text{insertIdx}\,n\,x = l_2.\text{insertIdx}\,n\,x$, then $l_1 = l_2$.