Module docstring
{"## Operations using indexes ","### mapFinIdx ","### mapIdx "}
List.mapFinIdx
definition
(as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β
Full source
/--
Applies a function to each element of the list along with the index at which that element is found,
returning the list of results. In addition to the index, the function is also provided with a proof
that the index is valid.
`List.mapIdx` is a variant that does not provide the function with evidence that the index is valid.
-/
@[inline] def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β :=
go as #[] (by simp)
where
/-- Auxiliary for `mapFinIdx`:
`mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]` -/
@[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → List β
| [], acc, h => acc.toList
| a :: as, acc, h =>
go as (acc.push (f acc.size a (by simp at h; omega))) (by simp at h ⊢; omega)Informal description
Given a list `as` of elements of type `α` and a function `f` that takes a natural number index `i`, an element of `α`, and a proof that `i` is a valid index for `as`, the function `List.mapFinIdx` applies `f` to each element of `as` along with its index and the proof of validity, returning the list of results.
More precisely, for each element `a` at position `i` in `as`, `f i a h` is computed where `h` is a proof that `i < as.length`, and the results are collected into a new list in the same order.
List.mapIdx
definition
(f : Nat → α → β) (as : List α) : List β
Full source
/--
Applies a function to each element of the list along with the index at which that element is found,
returning the list of results.
`List.mapFinIdx` is a variant that additionally provides the function with a proof that the index
is valid.
-/
@[inline] def mapIdx (f : Nat → α → β) (as : List α) : List β := go as #[] where
/-- Auxiliary for `mapIdx`:
`mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
@[specialize] go : List α → Array β → List β
| [], acc => acc.toList
| a :: as, acc => go as (acc.push (f acc.size a))Informal description
Given a function $f : \mathbb{N} \to \alpha \to \beta$ and a list $as$ of elements of type $\alpha$, the function `List.mapIdx` applies $f$ to each element of $as$ along with its index, returning the list of results in the same order.
More precisely, for each element $a$ at position $i$ in $as$, $f(i, a)$ is computed, and the results are collected into a new list. The indices start at $0$ for the first element of the list.
List.mapFinIdxM
definition
[Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β)
Full source
/--
Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results. In addition to the index, the function is also provided with a
proof that the index is valid.
`List.mapIdxM` is a variant that does not provide the function with evidence that the index is
valid.
-/
@[inline] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
go as #[] (by simp)
where
/-- Auxiliary for `mapFinIdxM`:
`mapFinIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]` -/
@[specialize] go : (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → m (List β)
| [], acc, h => pure acc.toList
| a :: as, acc, h => do
go as (acc.push (← f acc.size a (by simp at h; omega))) (by simp at h ⊢; omega)Informal description
Given a monad `m`, a list `as` of elements of type `α`, and a function `f` that takes a natural number index `i`, an element of `α`, and a proof that `i` is a valid index for `as`, the function `List.mapFinIdxM` applies `f` to each element of `as` along with its index and the proof of validity in the monadic context `m`, returning the list of results in the same order.
More precisely, for each element `a` at position `i` in `as`, `f i a h` is computed where `h` is a proof that `i < as.length`, and the results are collected into a new list in the same order within the monad `m`.
List.mapIdxM
definition
[Monad m] (f : Nat → α → m β) (as : List α) : m (List β)
Full source
/--
Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results.
`List.mapFinIdxM` is a variant that additionally provides the function with a proof that the index
is valid.
-/
@[inline] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
/-- Auxiliary for `mapIdxM`:
`mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
@[specialize] go : List α → Array β → m (List β)
| [], acc => pure acc.toList
| a :: as, acc => do go as (acc.push (← f acc.size a))Informal description
Given a monadic function \( f \) that takes a natural number index and an element of type \( \alpha \) to produce a monadic value of type \( \beta \), and a list \( as \) of elements of type \( \alpha \), `List.mapIdxM` applies \( f \) to each element of \( as \) along with its index in the list, collecting the results in a monadic context. The indices start at 0 for the first element of the list.
More precisely, for a list \([a_0, a_1, \ldots, a_{n-1}]\), the function returns the monadic computation that produces \([f(0, a_0), f(1, a_1), \ldots, f(n-1, a_{n-1})]\).
List.mapFinIdx_congr
theorem
{xs ys : List α} (w : xs = ys) (f : (i : Nat) → α → (h : i < xs.length) → β) :
mapFinIdx xs f = mapFinIdx ys (fun i a h => f i a (by simp [w]; omega))
Informal description
For any two lists $xs$ and $ys$ of type $\alpha$ such that $xs = ys$, and any function $f$ that takes a natural number index $i$, an element of $\alpha$, and a proof that $i$ is less than the length of $xs$, the application of `mapFinIdx` to $xs$ and $f$ is equal to the application of `mapFinIdx` to $ys$ and the function $\lambda i\ a\ h, f\ i\ a\ (\text{by simp }[w]; \text{omega})$. That is, $\text{mapFinIdx}\ xs\ f = \text{mapFinIdx}\ ys\ (\lambda i\ a\ h, f\ i\ a\ (\text{by simp }[w]; \text{omega}))$.
List.mapFinIdx_nil
theorem
{f : (i : Nat) → α → (h : i < 0) → β} : mapFinIdx [] f = []
Informal description
For any function $f$ that takes a natural number index $i$, an element of type $\alpha$, and a proof that $i$ is less than the length of an empty list, the application of `mapFinIdx` to the empty list and $f$ results in the empty list. That is, $\text{mapFinIdx}\ []\ f = []$.
List.length_mapFinIdx_go
theorem
: (mapFinIdx.go as f bs acc h).length = as.length
Full source
@[simp] theorem length_mapFinIdx_go :
(mapFinIdx.go as f bs acc h).length = as.length := by
induction bs generalizing acc with
| nil => simpa using h
| cons _ _ ih => simp [mapFinIdx.go, ih]Informal description
For any lists `as`, `bs`, and `acc`, and any function `f` with appropriate type constraints, the length of the list produced by the auxiliary function `mapFinIdx.go` applied to `as`, `f`, `bs`, `acc`, and `h` is equal to the length of the input list `as`. That is, $\text{length}(\text{mapFinIdx.go}\ as\ f\ bs\ acc\ h) = \text{length}(as)$.
List.length_mapFinIdx
theorem
{as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} : (as.mapFinIdx f).length = as.length
Full source
@[simp] theorem length_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
(as.mapFinIdx f).length = as.length := by
simp [mapFinIdx, length_mapFinIdx_go]Informal description
For any list `as` of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(as)) \to \beta$, the length of the list obtained by applying `mapFinIdx` to `as` and `f` is equal to the length of `as$. That is, $\text{length}(\text{mapFinIdx}\ as\ f) = \text{length}(as)$.
List.getElem_mapFinIdx_go
theorem
{as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} :
(mapFinIdx.go as f bs acc h)[i] =
if w' : i < acc.size then acc[i] else f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega)
Full source
theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} :
(mapFinIdx.go as f bs acc h)[i] =
if w' : i < acc.size then
acc[i]
else
f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega) := by
induction bs generalizing acc with
| nil =>
simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h
simp only [mapFinIdx.go, Array.getElem_toList]
rw [dif_pos]
| cons _ _ ih =>
simp [mapFinIdx.go]
rw [ih]
simp
split <;> rename_i h₁ <;> split <;> rename_i h₂
· rw [Array.getElem_push_lt]
· have h₃ : i = acc.size := by omega
subst h₃
simp
· omega
· have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega
simp [h₃]Informal description
For any lists `as` and `bs` of type `α`, any accumulator list `acc` of type `β`, any function `f : ℕ → α → (i < length as) → β`, and any index `i : ℕ` with proof `h` that `i < length (mapFinIdx.go as f bs acc h)`, the element at index `i` in the result of `mapFinIdx.go` is given by:
\[
(\text{mapFinIdx.go}\ as\ f\ bs\ acc\ h)[i] =
\begin{cases}
acc[i] & \text{if } i < \text{length}\ acc \\
f\ i\ (bs[i - \text{length}\ acc])\ (\text{proof}) & \text{otherwise}
\end{cases}
\]
where the proof terms ensure the indices are valid.
List.getElem_mapFinIdx
theorem
{as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} :
(as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega)
Full source
@[simp] theorem getElem_mapFinIdx {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} :
(as.mapFinIdx f)[i] = f i (as[i]'(by simp at h; omega)) (by simp at h; omega) := by
simp [mapFinIdx, getElem_mapFinIdx_go]Informal description
For any list `as` of elements of type $\alpha$, any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(as)) \to \beta$, and any index $i \in \mathbb{N}$ with proof $h$ that $i$ is a valid index for the mapped list, the element at index $i$ in the list obtained by applying `mapFinIdx` to `as` and $f$ is equal to $f$ applied to $i$, the $i$-th element of `as`, and the proof that $i$ is a valid index for `as$. That is:
\[
(\text{mapFinIdx}\ as\ f)[i] = f\ i\ (as[i])\ (h')
\]
where $h'$ is the proof that $i < \text{length}(as)$ derived from $h$.
List.mapFinIdx_eq_ofFn
theorem
{as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] i.2
Informal description
For any list $as$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(as)) \to \beta$, the indexed mapping $\text{mapFinIdx}\ as\ f$ is equal to the list constructed from the function $\lambda (i : \text{Fin}\ (\text{length}\ as)),\ f\ i\ (as[i])\ i.2$, where $i.2$ is the proof that $i$ is a valid index for $as$.
In other words:
\[
\text{mapFinIdx}\ as\ f = \text{List.ofFn}\ (\lambda (i : \text{Fin}\ (\text{length}\ as)),\ f\ i\ (as[i])\ i.2)
\]
List.getElem?_mapFinIdx
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} :
(l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1)
Full source
@[simp] theorem getElem?_mapFinIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {i : Nat} :
(l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f i x (by simp [getElem?_eq_some_iff] at m; exact m.1) := by
simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx]
split <;> simpInformal description
For any list $l$ of elements of type $\alpha$, any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, and any index $i \in \mathbb{N}$, the optional element at index $i$ in the list obtained by applying `mapFinIdx` to $l$ and $f$ is equal to the partial bind of the optional element at index $i$ in $l$ with the function $\lambda x\ m.\ f\ i\ x\ h$, where $h$ is a proof derived from $m$ that $i < \text{length}(l)$. That is:
\[
(l.\text{mapFinIdx}\ f)[i]? = l[i]?.\text{pbind}\ (\lambda x\ m.\ f\ i\ x\ h)
\]
where $h$ is constructed from $m$ via simplification of the proof that $l[i]?$ is `some x`.
List.mapFinIdx_cons
theorem
{l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} :
mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega))
Full source
@[simp]
theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i < l.length + 1) → β} :
mapFinIdx (a :: l) f = f 0 a (by omega) :: mapFinIdx l (fun i a h => f (i + 1) a (by omega)) := by
apply ext_getElem
· simp
· rintro (_|i) h₁ h₂ <;> simpInformal description
For any list `l` of elements of type $\alpha$, any element `a` of type $\alpha$, and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l) + 1) \to \beta$, the indexed mapping of the list `a :: l` under `f` is equal to the list obtained by applying `f` to the head element `a` with index `0`, followed by the indexed mapping of `l` where each element's index is incremented by `1`. That is:
\[
\text{mapFinIdx}\,(a :: l)\,f = f\,0\,a\,h_0 :: \text{mapFinIdx}\,l\,(\lambda i\,a\,h.\,f\,(i+1)\,a\,h')
\]
where $h_0$ is a proof that $0 < \text{length}(l) + 1$ and $h'$ is a proof that $i+1 < \text{length}(l) + 1$ derived from $h$.
List.mapFinIdx_append
theorem
{xs ys : List α} {f : (i : Nat) → α → (h : i < (xs ++ ys).length) → β} :
(xs ++ ys).mapFinIdx f =
xs.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
ys.mapFinIdx (fun i a h => f (i + xs.length) a (by simp; omega))
Full source
theorem mapFinIdx_append {xs ys : List α} {f : (i : Nat) → α → (h : i < (xs ++ ys).length) → β} :
(xs ++ ys).mapFinIdx f =
xs.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
ys.mapFinIdx (fun i a h => f (i + xs.length) a (by simp; omega)) := by
apply ext_getElem
· simp
· intro i h₁ h₂
rw [getElem_append]
simp only [getElem_mapFinIdx, length_mapFinIdx]
split <;> rename_i h
· rw [getElem_append_left]
· simp only [Nat.not_lt] at h
rw [getElem_append_right h]
congr
omegaInformal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(xs \mathbin{+\kern-1.5ex+} ys)) \to \beta$, the indexed mapping of the concatenated list $xs \mathbin{+\kern-1.5ex+} ys$ with $f$ is equal to the concatenation of:
1. The indexed mapping of $xs$ with the function $\lambda i\ a\ h.\ f\ i\ a\ h'$ (where $h'$ is derived from $h$)
2. The indexed mapping of $ys$ with the function $\lambda i\ a\ h.\ f\ (i + \text{length}(xs))\ a\ h''$ (where $h''$ is derived from $h$)
More formally:
\[
\text{mapFinIdx}\ (xs \mathbin{+\kern-1.5ex+} ys)\ f = \text{mapFinIdx}\ xs\ (\lambda i\ a\ h.\ f\ i\ a\ h') \mathbin{+\kern-1.5ex+} \text{mapFinIdx}\ ys\ (\lambda i\ a\ h.\ f\ (i + |xs|)\ a\ h'')
\]
where $h'$ and $h''$ are validity proofs constructed from $h$.
List.mapFinIdx_concat
theorem
{l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β} :
(l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)]
Full source
@[simp] theorem mapFinIdx_concat {l : List α} {e : α} {f : (i : Nat) → α → (h : i < (l ++ [e]).length) → β}:
(l ++ [e]).mapFinIdx f = l.mapFinIdx (fun i a h => f i a (by simp; omega)) ++ [f l.length e (by simp)] := by
simp [mapFinIdx_append]Informal description
For any list $l$ of elements of type $\alpha$, any element $e$ of type $\alpha$, and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l \mathbin{+\kern-1.5ex+} [e])) \to \beta$, the indexed mapping of the concatenated list $l \mathbin{+\kern-1.5ex+} [e]$ with $f$ is equal to the concatenation of:
1. The indexed mapping of $l$ with the function $\lambda i\ a\ h.\ f\ i\ a\ h'$ (where $h'$ is derived from $h$)
2. The singleton list containing $f\ \text{length}(l)\ e\ h''$ (where $h''$ is derived from the proof that $\text{length}(l) < \text{length}(l \mathbin{+\kern-1.5ex+} [e])$)
More formally:
\[
\text{mapFinIdx}\,(l \mathbin{+\kern-1.5ex+} [e])\,f = \text{mapFinIdx}\,l\,(\lambda i\ a\ h.\ f\ i\ a\ h') \mathbin{+\kern-1.5ex+} [f\,|l|\,e\,h'']
\]
where $h'$ and $h''$ are validity proofs constructed from $h$.
List.mapFinIdx_singleton
theorem
{a : α} {f : (i : Nat) → α → (h : i < 1) → β} : [a].mapFinIdx f = [f 0 a (by simp)]
Full source
theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
[a].mapFinIdx f = [f 0 a (by simp)] := by
simpInformal description
For any element $a$ of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < 1) \to \beta$, the indexed mapping of the singleton list $[a]$ under $f$ is equal to the singleton list $[f\,0\,a\,h]$, where $h$ is a proof that $0 < 1$.
In symbols:
\[
\text{mapFinIdx}\,[a]\,f = [f\,0\,a\,h]
\]
List.mapFinIdx_eq_zipIdx_map
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f =
l.zipIdx.attach.map fun ⟨⟨x, i⟩, m⟩ =>
f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1)
Full source
theorem mapFinIdx_eq_zipIdx_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l.zipIdx.attach.map
fun ⟨⟨x, i⟩, m⟩ =>
f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
apply ext_getElem <;> simpInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the indexed mapping operation $\text{mapFinIdx}\ l\ f$ is equal to mapping over the attached list of index-element pairs, where each pair $\langle (x, i), m \rangle$ consists of an element $x$ at index $i$ in $l$ and a proof $m$ that $(x, i)$ is in $\text{zipIdx}\ l$, applying $f$ to $i$, $x$, and the proof derived from $m$ that $i < \text{length}(l)$.
In symbols:
\[
\text{mapFinIdx}\ l\ f = \text{map}\ (\lambda \langle (x, i), m \rangle . f\ i\ x\ h)\ (\text{attach}\ (\text{zipIdx}\ l))
\]
where $h$ is the proof that $i < \text{length}(l)$ obtained from $m$.
List.mapFinIdx_eq_zipWithIndex_map
abbrev
Full source
@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_mapInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the indexed mapping operation $\text{mapFinIdx}\ l\ f$ is equal to mapping over the list of index-element pairs obtained by $\text{zipWithIndex}\ l$, where each pair $(x, i)$ consists of an element $x$ at index $i$ in $l$.
In symbols:
\[
\text{mapFinIdx}\ l\ f = \text{map}\ (\lambda (x, i). f\ i\ x\ h)\ (\text{zipWithIndex}\ l)
\]
where $h$ is a proof that $i < \text{length}(l)$ derived from the construction of $\text{zipWithIndex}\ l$.
List.mapFinIdx_eq_nil_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f = [] ↔ l = []
Full source
@[simp]
theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = [] ↔ l = [] := by
rw [mapFinIdx_eq_zipIdx_map, map_eq_nil_iff, attach_eq_nil_iff, zipIdx_eq_nil_iff]Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the mapped list $\text{mapFinIdx}\ l\ f$ is empty if and only if the original list $l$ is empty. In other words:
$$ \text{mapFinIdx}\ l\ f = [] \leftrightarrow l = [] $$
List.mapFinIdx_ne_nil_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.mapFinIdx f ≠ [] ↔ l ≠ []
Full source
theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f ≠ []l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
simpInformal description
For any list $l$ of elements of type $\alpha$ and any function $f$ that takes an index $i$, an element of $\alpha$, and a proof that $i$ is a valid index for $l$, the mapped list $\text{mapFinIdx}\ l\ f$ is non-empty if and only if the original list $l$ is non-empty.
List.exists_of_mem_mapFinIdx
theorem
{b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} (h : b ∈ l.mapFinIdx f) :
∃ (i : Nat) (h : i < l.length), f i l[i] h = b
Full source
theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
(h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
rw [mapFinIdx_eq_zipIdx_map] at h
replace h := exists_of_mem_map h
simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_zipIdx_iff_getElem?] at h
obtain ⟨b, i, h, rfl⟩ := h
rw [getElem?_eq_some_iff] at h
obtain ⟨h', rfl⟩ := h
exact ⟨i, h', rfl⟩Informal description
For any element $b$ of type $\beta$, any list $l$ of elements of type $\alpha$, and any function $f$ that takes an index $i$, an element of $\alpha$, and a proof that $i$ is a valid index for $l$, if $b$ is in the list obtained by applying $f$ to each element of $l$ along with its index and validity proof, then there exists an index $i$ such that $i$ is a valid index for $l$ and $f(i, l[i], h) = b$ (where $h$ is the proof that $i < \text{length}(l)$).
List.mem_mapFinIdx
theorem
{b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b
Full source
@[simp] theorem mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
b ∈ l.mapFinIdx fb ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
constructor
· intro h
exact exists_of_mem_mapFinIdx h
· rintro ⟨i, h, rfl⟩
rw [mem_iff_getElem]
exact ⟨i, by simpa using h, by simp⟩Informal description
For any element $b$ of type $\beta$, any list $l$ of elements of type $\alpha$, and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the element $b$ belongs to the list obtained by mapping $f$ over $l$ with indices if and only if there exists an index $i$ such that $i$ is a valid index for $l$ and $f(i, l[i], h) = b$, where $h$ is the proof that $i < \text{length}(l)$.
In symbols:
\[
b \in \text{mapFinIdx}\,l\,f \leftrightarrow \exists i < \text{length}(l),\, f(i, l[i], h) = b
\]
List.mapFinIdx_eq_cons_iff
theorem
{l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = b :: l₂ ↔
∃ (a : α) (l₁ : List α) (w : l = a :: l₁),
f 0 a (by simp [w]) = b ∧ l₁.mapFinIdx (fun i a h => f (i + 1) a (by simp [w]; omega)) = l₂
Full source
theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = b :: l₂ ↔
∃ (a : α) (l₁ : List α) (w : l = a :: l₁),
f 0 a (by simp [w]) = b ∧ l₁.mapFinIdx (fun i a h => f (i + 1) a (by simp [w]; omega)) = l₂ := by
cases l with
| nil => simp
| cons x l' =>
simp only [mapFinIdx_cons, cons.injEq, length_cons, Fin.zero_eta, Fin.cast_succ_eq,
exists_and_left]
constructor
· rintro ⟨rfl, rfl⟩
refine ⟨x, l', ⟨rfl, rfl⟩, by simp⟩
· rintro ⟨a, l', ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
exact ⟨rfl, by simp⟩Informal description
For any list $l$ of elements of type $\alpha$, any element $b$ of type $\beta$, and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the mapped list $\text{mapFinIdx}\ l\ f$ is equal to the cons list $b :: l_2$ if and only if there exists an element $a \in \alpha$ and a sublist $l_1$ such that:
1. $l$ can be decomposed as $a :: l_1$ (i.e., $l = a :: l_1$),
2. $f(0, a, h_0) = b$ where $h_0$ is a proof that $0 < \text{length}(l)$, and
3. The mapped sublist $\text{mapFinIdx}\ l_1\ (\lambda i\ a\ h.\ f(i+1, a, h'))$ equals $l_2$, where $h'$ is a proof that $i+1 < \text{length}(l)$ derived from $h$.
In symbols:
\[
\text{mapFinIdx}\ l\ f = b :: l_2 \leftrightarrow \exists a\ l_1, (l = a :: l_1) \land (f(0, a, h_0) = b) \land (\text{mapFinIdx}\ l_1\ (\lambda i\ a\ h.\ f(i+1, a, h')) = l_2)
\]
List.mapFinIdx_eq_cons_iff'
theorem
{l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = b :: l₂ ↔
l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧
l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂
Full source
theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = b :: l₂ ↔
l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧
l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂ := by
cases l <;> simpInformal description
For any list $l$ of elements of type $\alpha$, any element $b$ of type $\beta$, and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the following are equivalent:
1. The mapped list $\text{mapFinIdx}\,l\,f$ equals $b :: l₂$ (a list with head $b$ and tail $l₂$).
2. The head of $l$ (if it exists) satisfies $f(0, x, h) = b$ when mapped under $f$ (where $h$ is a proof that $0$ is a valid index), and the tail of $l$ (if it exists) maps to $l₂$ under the function $\lambda i\,a\,h.\,f(i+1, a, h')$ (where $h'$ is the corresponding validity proof for the tail).
In symbols:
\[
\text{mapFinIdx}\,l\,f = b :: l₂ \leftrightarrow
\begin{cases}
\text{head?}\,l \text{ maps to } \text{some }b \text{ under } f(0, \cdot, h_0), \text{ and} \\
\text{tail?}\,l \text{ maps to } \text{some }l₂ \text{ under } \lambda i\,a\,h.\,f(i+1, a, h')
\end{cases}
\]
List.mapFinIdx_eq_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h
Full source
theorem mapFinIdx_eq_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l' ↔ ∃ h : l'.length = l.length, ∀ (i : Nat) (h : i < l.length), l'[i] = f i l[i] h := by
constructor
· rintro rfl
simp
· rintro ⟨h, w⟩
apply ext_getElem <;> simp_allInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the mapped list $\text{mapFinIdx}\ l\ f$ is equal to another list $l'$ if and only if:
1. The lengths of $l'$ and $l$ are equal, and
2. For every index $i$ and proof $h$ that $i$ is a valid index for $l$, the $i$-th element of $l'$ satisfies $l'[i] = f(i, l[i], h)$.
In symbols:
\[
\text{mapFinIdx}\ l\ f = l' \leftrightarrow \exists h : \text{length}(l') = \text{length}(l), \forall i < \text{length}(l), l'[i] = f(i, l[i], h)
\]
List.mapFinIdx_eq_singleton_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
l.mapFinIdx f = [b] ↔ ∃ (a : α) (w : l = [a]), f 0 a (by simp [w]) = b
Full source
@[simp] theorem mapFinIdx_eq_singleton_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
l.mapFinIdx f = [b] ↔ ∃ (a : α) (w : l = [a]), f 0 a (by simp [w]) = b := by
simp [mapFinIdx_eq_cons_iff]Informal description
For any list $l$ of elements of type $\alpha$, any function $f$ that maps an index $i$, an element of $\alpha$, and a proof that $i$ is a valid index for $l$ to an element of type $\beta$, and any element $b$ of type $\beta$, the following are equivalent:
1. The result of applying `mapFinIdx` to $l$ and $f$ is the singleton list $[b]$.
2. There exists an element $a$ of type $\alpha$ such that $l = [a]$ and $f(0, a, h) = b$, where $h$ is a proof that $0$ is a valid index for $l$.
In symbols:
$$
\text{mapFinIdx}\ l\ f = [b] \leftrightarrow \exists a \in \alpha, l = [a] \land f(0, a, h) = b
$$
List.mapFinIdx_eq_append_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l₁ ++ l₂ ↔
∃ (l₁' : List α) (l₂' : List α) (w : l = l₁' ++ l₂'),
l₁'.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₁ ∧
l₂'.mapFinIdx (fun i a h => f (i + l₁'.length) a (by simp [w]; omega)) = l₂
Full source
theorem mapFinIdx_eq_append_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l₁ ++ l₂ ↔
∃ (l₁' : List α) (l₂' : List α) (w : l = l₁' ++ l₂'),
l₁'.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₁ ∧
l₂'.mapFinIdx (fun i a h => f (i + l₁'.length) a (by simp [w]; omega)) = l₂ := by
rw [mapFinIdx_eq_iff]
constructor
· intro ⟨h, w⟩
simp only [length_append] at h
refine ⟨l.take l₁.length, l.drop l₁.length, by simp, ?_⟩
constructor
· apply ext_getElem
· simp
omega
· intro i hi₁ hi₂
simp only [getElem_mapFinIdx, getElem_take]
specialize w i (by omega)
rw [getElem_append_left hi₂] at w
exact w.symm
· apply ext_getElem
· simp
omega
· intro i hi₁ hi₂
simp only [getElem_mapFinIdx, getElem_take]
simp only [length_take, getElem_drop]
have : l₁.length ≤ l.length := by omega
simp only [Nat.min_eq_left this, Nat.add_comm]
specialize w (i + l₁.length) (by omega)
rw [getElem_append_right (by omega)] at w
simpa using w.symm
· rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
refine ⟨by simp, fun i h => ?_⟩
rw [getElem_append]
split <;> rename_i h'
· simp [getElem_append_left (by simpa using h')]
· simp only [length_mapFinIdx, Nat.not_lt] at h'
have : i - l₁'.length + l₁'.length = i := by omega
simp [getElem_append_right h', this]Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the mapped list $\text{mapFinIdx}\ l\ f$ is equal to the concatenation of two lists $l_1$ and $l_2$ if and only if there exist sublists $l_1'$ and $l_2'$ of $l$ such that:
1. $l = l_1' \mathbin{+\kern-1.5ex+} l_2'$,
2. $\text{mapFinIdx}\ l_1'\ (\lambda i\ a\ h, f\ i\ a\ h') = l_1$, where $h'$ is derived from the proof that $l = l_1' \mathbin{+\kern-1.5ex+} l_2'$,
3. $\text{mapFinIdx}\ l_2'\ (\lambda i\ a\ h, f\ (i + \text{length}(l_1'))\ a\ h'') = l_2$, where $h''$ is similarly derived.
In symbols:
\[
\text{mapFinIdx}\ l\ f = l_1 \mathbin{+\kern-1.5ex+} l_2 \leftrightarrow \exists l_1', l_2', w : l = l_1' \mathbin{+\kern-1.5ex+} l_2', \text{mapFinIdx}\ l_1'\ (\lambda i\ a\ h, f\ i\ a\ h') = l_1 \land \text{mapFinIdx}\ l_2'\ (\lambda i\ a\ h, f\ (i + |l_1'|)\ a\ h'') = l_2
\]
List.mapFinIdx_eq_mapFinIdx_iff
theorem
{l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h
Full source
theorem mapFinIdx_eq_mapFinIdx_iff {l : List α} {f g : (i : Nat) → α → (h : i < l.length) → β} :
l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h := by
rw [eq_comm, mapFinIdx_eq_iff]
simp [Fin.forall_iff]Informal description
For any list $l$ of elements of type $\alpha$ and any two functions $f, g : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, the following are equivalent:
1. The lists obtained by applying `mapFinIdx` to $l$ with $f$ and $g$ are equal.
2. For every index $i$ and proof $h$ that $i$ is a valid index for $l$, we have $f(i, l[i], h) = g(i, l[i], h)$.
In symbols:
\[
\text{mapFinIdx}\ l\ f = \text{mapFinIdx}\ l\ g \leftrightarrow \forall i < \text{length}(l), f(i, l[i], h) = g(i, l[i], h)
\]
List.mapFinIdx_mapFinIdx
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).length) → γ} :
(l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa))
Informal description
For any list $l$ of elements of type $\alpha$, and functions $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$ and $g : \mathbb{N} \to \beta \to (i < \text{length}(\text{mapFinIdx}\ l\ f)) \to \gamma$, the following equality holds:
\[
\text{mapFinIdx}\ (\text{mapFinIdx}\ l\ f)\ g = \text{mapFinIdx}\ l\ \left(\lambda i\ a\ h, g\ i\ (f\ i\ a\ h)\ h'\right)
\]
where $h'$ is a proof that $i < \text{length}(\text{mapFinIdx}\ l\ f)$, derived from $h$ via simplification.
List.mapFinIdx_eq_replicate_iff
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b
Full source
theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b := by
rw [eq_replicate_iff, length_mapFinIdx]
simp only [mem_mapFinIdx, forall_exists_index, true_and]
constructor
· intro w i h
exact w (f i l[i] h) i h rfl
· rintro w b i h rfl
exact w i hInformal description
For any list $l$ of elements of type $\alpha$, any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$, and any element $b : \beta$, the following are equivalent:
1. The list obtained by applying `mapFinIdx` to $l$ and $f$ is equal to the list `replicate (length l) b` (i.e., a list of length $\text{length}(l)$ where every element is $b$).
2. For every index $i$ of $l$ (with proof $h : i < \text{length}(l)$), the value $f(i, l[i], h)$ equals $b$.
List.mapFinIdx_reverse
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.reverse.length) → β} :
l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (l.length - 1 - i) a (by simp; omega))).reverse
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to (i < \text{length}(l^{\text{reverse}})) \to \beta$, the following equality holds:
\[
\text{mapFinIdx}(l^{\text{reverse}}, f) = \left(\text{mapFinIdx}\left(l, \lambda i\ a\ h.\ f(|l| - 1 - i)\ a\ h'\right)\right)^{\text{reverse}}
\]
where $h'$ is a proof that $|l| - 1 - i < \text{length}(l)$ derived from the assumption $i < \text{length}(l^{\text{reverse}})$ and the fact that $\text{length}(l^{\text{reverse}}) = \text{length}(l)$.
List.mapIdx_nil
theorem
{f : Nat → α → β} : mapIdx f [] = []
Informal description
For any function $f : \mathbb{N} \to \alpha \to \beta$, applying `mapIdx` to $f$ and the empty list `[]` results in the empty list `[]`. That is, $\text{mapIdx}(f, []) = []$.
List.mapIdx_go_length
theorem
{acc : Array β} : length (mapIdx.go f l acc) = length l + acc.size
Full source
theorem mapIdx_go_length {acc : Array β} :
length (mapIdx.go f l acc) = length l + acc.size := by
induction l generalizing acc with
| nil => simp only [mapIdx.go, length_nil, Nat.zero_add]
| cons _ _ ih =>
simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]Informal description
For any list `l` of type `List α`, any function `f : Nat → α → β`, and any accumulator array `acc` of type `Array β`, the length of the list obtained by applying `mapIdx.go` to `f`, `l`, and `acc` is equal to the sum of the length of `l` and the size of `acc`. That is, $\text{length}(\text{mapIdx.go}(f, l, \text{acc})) = \text{length}(l) + \text{size}(\text{acc})$.
List.length_mapIdx_go
theorem
: ∀ {l : List α} {acc : Array β}, (mapIdx.go f l acc).length = l.length + acc.size
Informal description
For any list $l$ of type $\alpha$, any function $f : \mathbb{N} \to \alpha \to \beta$, and any accumulator array $\text{acc}$ of type $\text{Array } \beta$, the length of the list obtained by applying $\text{mapIdx.go}$ to $f$, $l$, and $\text{acc}$ is equal to the sum of the length of $l$ and the size of $\text{acc}$. That is, $\text{length}(\text{mapIdx.go}(f, l, \text{acc})) = \text{length}(l) + \text{size}(\text{acc})$.
List.length_mapIdx
theorem
{l : List α} : (l.mapIdx f).length = l.length
Full source
@[simp] theorem length_mapIdx {l : List α} : (l.mapIdx f).length = l.length := by
simp [mapIdx, length_mapIdx_go]Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the length of the list obtained by applying $\text{mapIdx}$ to $f$ and $l$ is equal to the length of $l$. That is, $\text{length}(l.\text{mapIdx}(f)) = \text{length}(l)$.
List.getElem?_mapIdx_go
theorem
:
∀ {l : List α} {acc : Array β} {i : Nat},
(mapIdx.go f l acc)[i]? = if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
Full source
theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
(mapIdx.go f l acc)[i]? =
if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
| [], acc, i => by
simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
| a :: l, acc, i => by
rw [mapIdx.go, getElem?_mapIdx_go]
simp only [Array.size_push]
split <;> split
· simp only [Option.some.injEq]
rw [← Array.getElem_toList]
simp only [Array.push_toList]
rw [getElem_append_left, ← Array.getElem_toList]
· have : i = acc.size := by omega
simp_all
· omega
· have : i - acc.size = i - (acc.size + 1) + 1 := by omega
simp_allInformal description
For any list `l` of type `List α`, accumulator array `acc` of type `Array β`, and natural number index `i`, the optional indexing operation on the result of `mapIdx.go f l acc` satisfies:
$$(\text{mapIdx.go } f \text{ } l \text{ } acc)[i]? =
\begin{cases}
\text{some } acc[i] & \text{if } i < \text{size}(acc) \\
\text{Option.map } (f i) \text{ } l[i - \text{size}(acc)]? & \text{otherwise}
\end{cases}$$
List.getElem?_mapIdx
theorem
{l : List α} {i : Nat} : (l.mapIdx f)[i]? = Option.map (f i) l[i]?
Full source
@[simp] theorem getElem?_mapIdx {l : List α} {i : Nat} :
(l.mapIdx f)[i]? = Option.map (f i) l[i]? := by
simp [mapIdx, getElem?_mapIdx_go]Informal description
For any list $l$ of elements of type $\alpha$, natural number index $i$, and function $f : \mathbb{N} \to \alpha \to \beta$, the optional indexing operation on the result of mapping $f$ over $l$ with indices satisfies:
$$(l.\text{mapIdx } f)[i]? = \text{Option.map } (f i) \text{ } l[i]?$$
List.getElem_mapIdx
theorem
{l : List α} {f : Nat → α → β} {i : Nat} {h : i < (l.mapIdx f).length} :
(l.mapIdx f)[i] = f i (l[i]'(by simpa using h))
Full source
@[simp] theorem getElem_mapIdx {l : List α} {f : Nat → α → β} {i : Nat} {h : i < (l.mapIdx f).length} :
(l.mapIdx f)[i] = f i (l[i]'(by simpa using h)) := by
apply Option.some_inj.mp
rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]
simpInformal description
For any list $l$ of elements of type $\alpha$, function $f : \mathbb{N} \to \alpha \to \beta$, and natural number index $i$ such that $i < \text{length}(l.\text{mapIdx } f)$, the $i$-th element of the list obtained by applying $\text{mapIdx}$ to $f$ and $l$ is equal to $f$ applied to $i$ and the $i$-th element of $l$. That is,
$$(l.\text{mapIdx } f)[i] = f(i, l[i]).$$
List.mapFinIdx_eq_mapIdx
theorem
{l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : Nat → α → β}
(h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) : l.mapFinIdx f = l.mapIdx g
Informal description
For any list $l$ of elements of type $\alpha$, and functions $f : \mathbb{N} \to \alpha \to (i < \text{length}(l)) \to \beta$ and $g : \mathbb{N} \to \alpha \to \beta$, if for every index $i$ and proof $h$ that $i < \text{length}(l)$, we have $f(i, l[i], h) = g(i, l[i])$, then the list obtained by applying $\text{mapFinIdx}$ to $f$ and $l$ is equal to the list obtained by applying $\text{mapIdx}$ to $g$ and $l$. That is,
$$l.\text{mapFinIdx } f = l.\text{mapIdx } g.$$
List.mapIdx_eq_mapFinIdx
theorem
{l : List α} {f : Nat → α → β} : l.mapIdx f = l.mapFinIdx (fun i a _ => f i a)
Full source
theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
simp [mapFinIdx_eq_mapIdx]Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping operation $\text{mapIdx}$ applied to $f$ and $l$ is equal to the finite indexed mapping operation $\text{mapFinIdx}$ applied to the function $\lambda i\ a\ \_\mapsto f(i, a)$ and $l$. That is,
$$l.\text{mapIdx } f = l.\text{mapFinIdx } (\lambda i\ a\ \_\mapsto f(i, a)).$$
List.mapIdx_eq_zipIdx_map
theorem
{l : List α} {f : Nat → α → β} : l.mapIdx f = l.zipIdx.map (fun ⟨a, i⟩ => f i a)
Full source
theorem mapIdx_eq_zipIdx_map {l : List α} {f : Nat → α → β} :
l.mapIdx f = l.zipIdx.map (fun ⟨a, i⟩ => f i a) := by
ext1 i
simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_zipIdx]
split <;> simpInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the operation of mapping $f$ over $l$ with indices is equivalent to first pairing each element with its index (via `zipIdx`) and then mapping the function $\lambda \langle a, i \rangle \mapsto f(i, a)$ over the resulting list of pairs.
In other words:
$$l.\text{mapIdx } f = l.\text{zipIdx}.\text{map } (\lambda \langle a, i \rangle \mapsto f(i, a))$$
List.mapIdx_eq_enum_map
abbrev
Full source
@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
abbrev mapIdx_eq_enum_map := @mapIdx_eq_zipIdx_mapInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the operation of mapping $f$ over $l$ with indices is equivalent to first enumerating the list (pairing each element with its index) and then mapping the function $\lambda (i, a) \mapsto f(i, a)$ over the resulting list of pairs.
In other words:
$$l.\text{mapIdx } f = l.\text{enum}.\text{map } (\lambda (i, a) \mapsto f(i, a))$$
List.mapIdx_cons
theorem
{l : List α} {a : α} : mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l
Full source
@[simp]
theorem mapIdx_cons {l : List α} {a : α} :
mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l := by
simp [mapIdx_eq_zipIdx_map, List.zipIdx_succ]Informal description
For any list $l$ of elements of type $\alpha$, any element $a \in \alpha$, and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of $f$ over the list $a :: l$ is equal to the list obtained by applying $f$ to index $0$ and element $a$, followed by the indexed mapping of the function $\lambda i \mapsto f (i + 1)$ over the remaining list $l$.
In other words:
$$\text{mapIdx } f (a :: l) = f(0, a) :: \text{mapIdx } (\lambda i \mapsto f(i + 1)) l$$
List.mapIdx_append
theorem
{xs ys : List α} : (xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + xs.length)
Full source
theorem mapIdx_append {xs ys : List α} :
(xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + xs.length) := by
induction xs generalizing f with
| nil => rfl
| cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]Informal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of $f$ over the concatenated list $xs ++ ys$ is equal to the concatenation of the indexed mapping of $f$ over $xs$ and the indexed mapping of the function $\lambda i \mapsto f(i + \text{length}(xs))$ over $ys$.
In other words:
$$\text{mapIdx } f (xs ++ ys) = (\text{mapIdx } f xs) ++ (\text{mapIdx } (\lambda i \mapsto f(i + |xs|)) ys)$$
List.mapIdx_concat
theorem
{l : List α} {e : α} : mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]
Full source
@[simp] theorem mapIdx_concat {l : List α} {e : α} :
mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e] := by
simp [mapIdx_append]Informal description
For any list $l$ of elements of type $\alpha$, any element $e \in \alpha$, and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of $f$ over the concatenated list $l ++ [e]$ is equal to the concatenation of the indexed mapping of $f$ over $l$ and the singleton list containing $f(|l|, e)$.
In other words:
$$\text{mapIdx } f (l ++ [e]) = (\text{mapIdx } f l) ++ [f(|l|, e)]$$
List.mapIdx_singleton
theorem
{a : α} : mapIdx f [a] = [f 0 a]
Full source
theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
simpInformal description
For any element $a$ of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of $f$ over the singleton list $[a]$ is equal to the singleton list $[f(0, a)]$. In other words:
$$\text{mapIdx}\,f\,[a] = [f(0, a)]$$
List.mapIdx_eq_nil_iff
theorem
{l : List α} : List.mapIdx f l = [] ↔ l = []
Full source
@[simp]
theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdxList.mapIdx f l = [] ↔ l = [] := by
rw [List.mapIdx_eq_zipIdx_map, List.map_eq_nil_iff, List.zipIdx_eq_nil_iff]Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by mapping a function $f$ over $l$ with indices is empty if and only if $l$ is empty. In other words, $\text{mapIdx}\,f\,l = [] \leftrightarrow l = []$.
List.mapIdx_ne_nil_iff
theorem
{l : List α} : List.mapIdx f l ≠ [] ↔ l ≠ []
Full source
theorem mapIdx_ne_nil_iff {l : List α} :
List.mapIdxList.mapIdx f l ≠ []List.mapIdx f l ≠ [] ↔ l ≠ [] := by
simpInformal description
For any list $l$ of elements of type $\alpha$, the mapped list $\text{mapIdx}\,f\,l$ is non-empty if and only if $l$ is non-empty. Here, $\text{mapIdx}\,f\,l$ denotes the list obtained by applying the function $f$ to each element of $l$ along with its index.
List.exists_of_mem_mapIdx
theorem
{b : β} {l : List α} (h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.length), f i l[i] = b
Full source
theorem exists_of_mem_mapIdx {b : β} {l : List α}
(h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.length), f i l[i] = b := by
rw [mapIdx_eq_mapFinIdx] at h
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx hInformal description
For any element $b$ of type $\beta$ and any list $l$ of elements of type $\alpha$, if $b$ belongs to the list obtained by applying a function $f : \mathbb{N} \to \alpha \to \beta$ to each element of $l$ along with its index, then there exists an index $i$ such that $i$ is a valid index for $l$ (i.e., $i < \text{length}(l)$) and $f(i, l[i]) = b$.
List.mem_mapIdx
theorem
{b : β} {l : List α} : b ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] = b
Full source
@[simp] theorem mem_mapIdx {b : β} {l : List α} :
b ∈ mapIdx f lb ∈ mapIdx f l ↔ ∃ (i : Nat) (h : i < l.length), f i l[i] = b := by
constructor
· intro h
exact exists_of_mem_mapIdx h
· rintro ⟨i, h, rfl⟩
rw [mem_iff_getElem]
exact ⟨i, by simpa using h, by simp⟩Informal description
For any element $b$ of type $\beta$ and any list $l$ of elements of type $\alpha$, the element $b$ belongs to the list obtained by applying the indexed mapping function $f : \mathbb{N} \to \alpha \to \beta$ to $l$ if and only if there exists an index $i$ such that $i$ is a valid index for $l$ (i.e., $i < \text{length}(l)$) and $f(i, l[i]) = b$.
In symbols:
$$b \in \text{mapIdx } f \text{ } l \leftrightarrow \exists i < \text{length}(l), f(i, l[i]) = b$$
List.mapIdx_eq_cons_iff
theorem
{l : List α} {b : β} :
mapIdx f l = b :: l₂ ↔ ∃ (a : α) (l₁ : List α), l = a :: l₁ ∧ f 0 a = b ∧ mapIdx (fun i => f (i + 1)) l₁ = l₂
Full source
theorem mapIdx_eq_cons_iff {l : List α} {b : β} :
mapIdxmapIdx f l = b :: l₂ ↔
∃ (a : α) (l₁ : List α), l = a :: l₁ ∧ f 0 a = b ∧ mapIdx (fun i => f (i + 1)) l₁ = l₂ := by
cases l <;> simp [and_assoc]Informal description
For any list $l$ of elements of type $\alpha$, a function $f : \mathbb{N} \to \alpha \to \beta$, and an element $b : \beta$, the following are equivalent:
1. The indexed mapping of $f$ over $l$ results in the list $b :: l₂$.
2. There exists an element $a \in \alpha$ and a list $l₁$ such that:
- $l = a :: l₁$,
- $f(0, a) = b$, and
- The indexed mapping of $\lambda i \mapsto f(i + 1)$ over $l₁$ results in $l₂$.
List.mapIdx_eq_cons_iff'
theorem
{l : List α} {b : β} :
mapIdx f l = b :: l₂ ↔ l.head?.map (f 0) = some b ∧ l.tail?.map (mapIdx fun i => f (i + 1)) = some l₂
Full source
theorem mapIdx_eq_cons_iff' {l : List α} {b : β} :
mapIdxmapIdx f l = b :: l₂ ↔
l.head?.map (f 0) = some b ∧ l.tail?.map (mapIdx fun i => f (i + 1)) = some l₂ := by
cases l <;> simpInformal description
For any list $l$ of elements of type $\alpha$, a function $f : \mathbb{N} \to \alpha \to \beta$, an element $b : \beta$, and a list $l_2$ of elements of type $\beta$, the following are equivalent:
1. The indexed mapping of $f$ over $l$ results in the list $b :: l_2$.
2. The head of $l$ (if it exists) satisfies $f(0, \text{head}(l)) = b$, and the tail of $l$ (if it exists) satisfies $\text{mapIdx } (\lambda i \mapsto f(i + 1)) \text{ } \text{tail}(l) = l_2$.
In symbols:
$$\text{mapIdx } f \text{ } l = b :: l_2 \leftrightarrow \text{head?}(l).\text{map } (f \text{ } 0) = \text{some } b \land \text{tail?}(l).\text{map } (\text{mapIdx } (\lambda i \mapsto f(i + 1))) = \text{some } l_2$$
List.mapIdx_eq_singleton_iff
theorem
{l : List α} {f : Nat → α → β} {b : β} : mapIdx f l = [b] ↔ ∃ (a : α), l = [a] ∧ f 0 a = b
Full source
@[simp] theorem mapIdx_eq_singleton_iff {l : List α} {f : Nat → α → β} {b : β} :
mapIdxmapIdx f l = [b] ↔ ∃ (a : α), l = [a] ∧ f 0 a = b := by
simp [mapIdx_eq_cons_iff]Informal description
For any list $l$ of elements of type $\alpha$, a function $f : \mathbb{N} \to \alpha \to \beta$, and an element $b : \beta$, the following are equivalent:
1. Mapping $f$ over $l$ with indices results in the singleton list $[b]$.
2. There exists an element $a : \alpha$ such that $l = [a]$ and $f(0, a) = b$.
List.mapIdx_eq_iff
theorem
{l : List α} : mapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i)
Full source
theorem mapIdx_eq_iff {l : List α} : mapIdxmapIdx f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map (f i) := by
constructor
· intro w i
simpa using congrArg (fun l => l[i]?) w.symm
· intro w
ext1 i
simp [w]Informal description
For any list $l$ of elements of type $\alpha$, a function $f : \mathbb{N} \to \alpha \to \beta$, and a list $l'$ of elements of type $\beta$, the following are equivalent:
1. The result of mapping $f$ over $l$ with indices equals $l'$.
2. For every natural number index $i$, the optional lookup operation on $l'$ at index $i$ equals the result of applying $f(i)$ to the optional lookup of $l$ at index $i$.
In symbols:
$$l.\text{mapIdx } f = l' \leftrightarrow \forall i \in \mathbb{N}, l'[i]? = \text{Option.map } (f i) \text{ } l[i]?$$
List.mapIdx_eq_append_iff
theorem
{l : List α} :
mapIdx f l = l₁ ++ l₂ ↔
∃ (l₁' : List α) (l₂' : List α), l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂
Full source
theorem mapIdx_eq_append_iff {l : List α} :
mapIdxmapIdx f l = l₁ ++ l₂ ↔
∃ (l₁' : List α) (l₂' : List α), l = l₁' ++ l₂' ∧
mapIdx f l₁' = l₁ ∧
mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂ := by
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]
simp only [mapFinIdx_eq_mapIdx, exists_and_left, exists_prop]
constructor
· rintro ⟨l₁, rfl, l₂, rfl, h⟩
refine ⟨l₁, l₂, by simp_all⟩
· rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
refine ⟨l₁, rfl, l₂, by simp_all⟩Informal description
For any list $l$ of elements of type $\alpha$ and function $f : \mathbb{N} \to \alpha \to \beta$, the mapped list $\text{mapIdx}\ f\ l$ equals the concatenation of two lists $l_1$ and $l_2$ if and only if there exist sublists $l_1'$ and $l_2'$ of $l$ such that:
1. $l = l_1' \mathbin{+\kern-1.5ex+} l_2'$,
2. $\text{mapIdx}\ f\ l_1' = l_1$,
3. $\text{mapIdx}\ (\lambda i, f (i + |l_1'|))\ l_2' = l_2$.
In symbols:
\[
\text{mapIdx}\ f\ l = l_1 \mathbin{+\kern-1.5ex+} l_2 \leftrightarrow \exists l_1', l_2', l = l_1' \mathbin{+\kern-1.5ex+} l_2' \land \text{mapIdx}\ f\ l_1' = l_1 \land \text{mapIdx}\ (\lambda i, f (i + |l_1'|))\ l_2' = l_2
\]
List.mapIdx_eq_mapIdx_iff
theorem
{l : List α} : mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.length) → f i l[i] = g i l[i]
Full source
theorem mapIdx_eq_mapIdx_iff {l : List α} :
mapIdxmapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.length) → f i l[i] = g i l[i] := by
constructor
· intro w i h
simpa [h] using congrArg (fun l => l[i]?) w
· intro w
apply ext_getElem
· simp
· intro i h₁ h₂
simp [w]Informal description
For any list $l$ of elements of type $\alpha$ and functions $f, g : \mathbb{N} \to \alpha \to \beta$, the following are equivalent:
1. The indexed mappings of $l$ under $f$ and $g$ are equal, i.e., $l.\text{mapIdx } f = l.\text{mapIdx } g$.
2. For every natural number index $i$ and proof $h : i < \text{length } l$, the functions $f$ and $g$ agree on $i$ and the $i$-th element of $l$, i.e., $f(i, l[i]) = g(i, l[i])$.
In symbols:
$$l.\text{mapIdx } f = l.\text{mapIdx } g \leftrightarrow \forall i \in \mathbb{N}, (h : i < \text{length } l) \to f(i, l[i]) = g(i, l[i])$$
List.mapIdx_set
theorem
{l : List α} {i : Nat} {a : α} : (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a)
Full source
@[simp] theorem mapIdx_set {l : List α} {i : Nat} {a : α} :
(l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) := by
simp only [mapIdx_eq_iff, getElem?_set, length_mapIdx, getElem?_mapIdx]
intro i
split
· split <;> simp_all
· rflInformal description
For any list $l$ of elements of type $\alpha$, index $i \in \mathbb{N}$, element $a \in \alpha$, and function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of the modified list $l.\text{set}(i, a)$ equals the modified indexed mapping of the original list. Specifically:
$$(l.\text{set}(i, a)).\text{mapIdx}(f) = (l.\text{mapIdx}(f)).\text{set}(i, f(i, a))$$
List.head_mapIdx
theorem
{l : List α} {f : Nat → α → β} {w : mapIdx f l ≠ []} : (mapIdx f l).head w = f 0 (l.head (by simpa using w))
Full source
@[simp] theorem head_mapIdx {l : List α} {f : Nat → α → β} {w : mapIdxmapIdx f l ≠ []} :
(mapIdx f l).head w = f 0 (l.head (by simpa using w)) := by
cases l with
| nil => simp at w
| cons _ _ => simpInformal description
For any list $l$ of elements of type $\alpha$ and function $f : \mathbb{N} \to \alpha \to \beta$, if the mapped list $\text{mapIdx } f l$ is non-empty, then its first element equals $f(0, a)$, where $a$ is the first element of $l$.
In symbols:
$$\text{head}(\text{mapIdx } f l) = f(0, \text{head } l)$$
List.head?_mapIdx
theorem
{l : List α} {f : Nat → α → β} : (mapIdx f l).head? = l.head?.map (f 0)
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the first element of the indexed mapping of $f$ over $l$ (wrapped in an `Option` type) is equal to applying $f$ at index $0$ to the first element of $l$ (if it exists), i.e.,
$$(\text{mapIdx } f \, l).\text{head?} = l.\text{head?}.map (f \, 0).$$
List.getLast_mapIdx
theorem
{l : List α} {f : Nat → α → β} {h} : (mapIdx f l).getLast h = f (l.length - 1) (l.getLast (by simpa using h))
Full source
@[simp] theorem getLast_mapIdx {l : List α} {f : Nat → α → β} {h} :
(mapIdx f l).getLast h = f (l.length - 1) (l.getLast (by simpa using h)) := by
cases l with
| nil => simp at h
| cons _ _ =>
simp only [← getElem_cons_length rfl]
simp only [mapIdx_cons]
simp only [← getElem_cons_length rfl]
simp only [← mapIdx_cons, getElem_mapIdx]
simpInformal description
For any list $l$ of elements of type $\alpha$, function $f : \mathbb{N} \to \alpha \to \beta$, and proof $h$ that $\text{mapIdx}\ f\ l$ is non-empty, the last element of the indexed mapping of $f$ over $l$ is equal to $f$ applied to the last index ($\text{length}(l) - 1$) and the last element of $l$. That is,
$$(\text{mapIdx}\ f\ l).\text{getLast}\ h = f(\text{length}(l) - 1, l.\text{getLast}\ h').$$
List.getLast?_mapIdx
theorem
{l : List α} {f : Nat → α → β} : (mapIdx f l).getLast? = (getLast? l).map (f (l.length - 1))
Full source
@[simp] theorem getLast?_mapIdx {l : List α} {f : Nat → α → β} :
(mapIdx f l).getLast? = (getLast? l).map (f (l.length - 1)) := by
cases l
· simp
· rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_mapIdx] <;> simpInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the optional last element of the indexed mapping of $f$ over $l$ is equal to applying $f$ at index $\text{length}(l) - 1$ to the optional last element of $l$. That is,
$$(\text{mapIdx } f \, l).\text{getLast?} = l.\text{getLast?}.map (f (\text{length}(l) - 1)).$$
List.mapIdx_mapIdx
theorem
{l : List α} {f : Nat → α → β} {g : Nat → β → γ} : (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i)
Full source
@[simp] theorem mapIdx_mapIdx {l : List α} {f : Nat → α → β} {g : Nat → β → γ} :
(l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
simp [mapIdx_eq_iff]Informal description
For any list $l$ of elements of type $\alpha$, and functions $f : \mathbb{N} \to \alpha \to \beta$ and $g : \mathbb{N} \to \beta \to \gamma$, the composition of mapping $f$ with indices followed by mapping $g$ with indices is equal to mapping the composition $(g \circ f)$ with indices. That is,
$$(l.\text{mapIdx } f).\text{mapIdx } g = l.\text{mapIdx } (\lambda i, g i \circ f i)$$
List.mapIdx_eq_replicate_iff
theorem
{l : List α} {f : Nat → α → β} {b : β} :
mapIdx f l = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b
Full source
theorem mapIdx_eq_replicate_iff {l : List α} {f : Nat → α → β} {b : β} :
mapIdxmapIdx f l = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = b := by
simp only [eq_replicate_iff, length_mapIdx, mem_mapIdx, forall_exists_index, true_and]
constructor
· intro w i h
apply w _ _ _ rfl
· rintro w _ i h rfl
exact w i hInformal description
For any list $l$ of elements of type $\alpha$, any function $f : \mathbb{N} \to \alpha \to \beta$, and any element $b : \beta$, the following are equivalent:
1. The list obtained by applying $f$ to each element of $l$ along with its index is equal to a list of length $\text{length}(l)$ where every element is $b$.
2. For every natural number index $i$ such that $i < \text{length}(l)$, we have $f(i, l[i]) = b$.
In symbols:
$$
\text{mapIdx}(f, l) = \text{replicate}(\text{length}(l), b) \leftrightarrow \forall i < \text{length}(l), f(i, l[i]) = b
$$
List.mapIdx_reverse
theorem
{l : List α} {f : Nat → α → β} : l.reverse.mapIdx f = (mapIdx (fun i => f (l.length - 1 - i)) l).reverse
Full source
@[simp] theorem mapIdx_reverse {l : List α} {f : Nat → α → β} :
l.reverse.mapIdx f = (mapIdx (fun i => f (l.length - 1 - i)) l).reverse := by
simp [mapIdx_eq_iff]
intro i
by_cases h : i < l.length
· simp [getElem?_reverse, h]
congr
omega
· simp at h
rw [getElem?_eq_none (by simp [h]), getElem?_eq_none (by simp [h])]
simpInformal description
For any list $l$ of elements of type $\alpha$ and any function $f : \mathbb{N} \to \alpha \to \beta$, the indexed mapping of the reversed list $l^{\text{reverse}}$ under $f$ is equal to the reversed list obtained by mapping $l$ under the function $\lambda i, f(|l| - 1 - i)$, where $|l|$ denotes the length of $l$. That is,
$$(l^{\text{reverse}}).\text{mapIdx } f = \left(\text{mapIdx } (\lambda i, f(|l| - 1 - i)) \, l\right)^{\text{reverse}}.$$