Module docstring
{"# Lemmas about List.range and List.enum
","## Ranges and enumeration ","### range' ","### range ","### iota ","### zipIdx ","### enumFrom ","### enum "}
List.mem_range'_1
theorem
: m ∈ range' s n ↔ s ≤ m ∧ m < s + n
Informal description
For any natural numbers $m$, $s$, and $n$, the element $m$ belongs to the list $\text{range'}\ s\ n$ if and only if $s \leq m$ and $m < s + n$.
List.getLast?_range'
theorem
{n : Nat} : (range' s n).getLast? = if n = 0 then none else some (s + n - 1)
Full source
theorem getLast?_range' {n : Nat} : (range' s n).getLast? = if n = 0 then none else some (s + n - 1) := by
induction n generalizing s with
| zero => simp
| succ n ih =>
rw [range'_succ, getLast?_cons, ih]
by_cases h : n = 0
· rw [if_pos h]
simp [h]
· rw [if_neg h]
simp
omegaInformal description
For any natural numbers $s$ and $n$, the last element of the arithmetic sequence `range' s n` (as an optional value) is `none` if $n = 0$, and otherwise is `some (s + n - 1)`.
List.getLast_range'
theorem
{n : Nat} (h) : (range' s n).getLast h = s + n - 1
Full source
@[simp] theorem getLast_range' {n : Nat} (h) : (range' s n).getLast h = s + n - 1 := by
cases n with
| zero => simp at h
| succ n => simp [getLast?_range', getLast_eq_iff_getLast?_eq_some]Informal description
For any natural numbers $s$ and $n$ with $n \neq 0$, the last element of the arithmetic sequence $\text{range'}\ s\ n$ is equal to $s + n - 1$.
List.map_sub_range'
theorem
{a s : Nat} (h : a ≤ s) (n : Nat) : map (· - a) (range' s n step) = range' (s - a) n step
Full source
theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
map (· - a) (range' s n step) = range' (s - a) n step := by
conv => lhs; rw [← Nat.add_sub_cancel' h]
rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]
funext x; apply Nat.add_sub_cancel_leftInformal description
For any natural numbers $a$, $s$, and $n$ such that $a \leq s$, the list obtained by subtracting $a$ from each element of the arithmetic sequence `range' s n step` is equal to the arithmetic sequence `range' (s - a) n step`.
In other words, mapping the function $(\cdot - a)$ over the list $[s, s + \text{step}, \ldots, s + (n - 1) \cdot \text{step}]$ yields the list $[s - a, (s - a) + \text{step}, \ldots, (s - a) + (n - 1) \cdot \text{step}]$.
List.range'_eq_singleton_iff
theorem
{s n a : Nat} : range' s n = [a] ↔ s = a ∧ n = 1
Full source
@[simp] theorem range'_eq_singleton_iff {s n a : Nat} : range'range' s n = [a] ↔ s = a ∧ n = 1 := by
rw [range'_eq_cons_iff]
simp only [nil_eq, range'_eq_nil_iff, and_congr_right_iff]
rintro rfl
omegaInformal description
For any natural numbers $s$, $n$, and $a$, the arithmetic sequence `range' s n` is equal to the singleton list $[a]$ if and only if $s = a$ and $n = 1$.
List.range'_eq_singleton
abbrev
Full source
@[deprecated range'_eq_singleton_iff (since := "2025-01-29")]
abbrev range'_eq_singleton := @range'_eq_singleton_iffInformal description
For any natural numbers $s$ and $n$, the arithmetic sequence $\text{range'}\ s\ n$ is a singleton list if and only if $n = 1$. In this case, the sequence consists of just the starting element $s$.
List.range'_eq_append_iff
theorem
: range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)
Full source
theorem range'_eq_append_iff : range'range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k) := by
induction n generalizing s xs ys with
| zero => simp
| succ n ih =>
simp only [range'_succ]
rw [cons_eq_append_iff]
constructor
· rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
· exact ⟨0, by simp [range'_succ]⟩
· simp only [ih] at h
obtain ⟨k, h, rfl, rfl⟩ := h
refine ⟨k + 1, ?_⟩
simp_all [range'_succ]
omega
· rintro ⟨k, h, rfl, rfl⟩
cases k with
| zero => simp [range'_succ]
| succ k =>
simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
refine ⟨k, ?_⟩
simp_all
omegaInformal description
For any natural numbers $s$ and $n$, and any lists $xs$ and $ys$ of natural numbers, the arithmetic sequence $\text{range'}\ s\ n$ equals the concatenation $xs ++ ys$ if and only if there exists a natural number $k \leq n$ such that $xs = \text{range'}\ s\ k$ and $ys = \text{range'}\ (s + k)\ (n - k)$.
List.find?_range'_eq_some
theorem
{s n : Nat} {i : Nat} {p : Nat → Bool} :
(range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j
Full source
@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
(range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
rw [find?_eq_some_iff_append]
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
and_congr_right_iff]
simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
intro h
constructor
· rintro ⟨as, ⟨_, k, h₁, rfl, rfl, h₂, rfl⟩, h₃⟩
constructor
· omega
· simpa using h₃
· rintro ⟨⟨h₁, h₂⟩, h₃⟩
refine ⟨range' s (i - s), ⟨⟨range' (i + 1) (n - (i - s) - 1), i - s, ?_⟩ , ?_⟩⟩
· simp; omega
· simp only [mem_range'_1, and_imp]
intro a a₁ a₂
exact h₃ a a₁ (by omega)Informal description
For any natural numbers $s$, $n$, and $i$, and any predicate $p : \mathbb{N} \to \text{Bool}$, the following are equivalent:
1. The function `find?` applied to the list `range' s n` and predicate $p$ returns `some i`.
2. The predicate $p(i)$ holds, $i$ belongs to the arithmetic sequence `range' s n` (i.e., $s \leq i < s + n$), and for all $j$ in the range $[s, i)$, the predicate $p(j)$ does not hold.
In other words, `find?` returns `some i` if and only if $i$ is the first element in the sequence `[s, s+1, ..., s+n-1]` that satisfies $p$.
List.find?_range'_eq_none
theorem
{s n : Nat} {p : Nat → Bool} : (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i
Full source
theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
(range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i := by
simpInformal description
For any natural numbers $s$ and $n$, and any predicate $p : \mathbb{N} \to \text{Bool}$, the following are equivalent:
1. The function `find?` applied to the list `range' s n` and predicate $p$ returns `none`.
2. For all natural numbers $i$ such that $s \leq i < s + n$, the predicate $p(i)$ evaluates to `false`.
In other words, `find?` returns `none` if and only if no element in the arithmetic sequence `[s, s+1, ..., s+n-1]` satisfies $p$.
List.erase_range'
theorem
: (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))
Full source
theorem erase_range' :
(range' s n).erase i =
range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1)) := by
by_cases h : i ∈ range' s n
· obtain ⟨as, bs, h₁, h₂⟩ := eq_append_cons_of_mem h
rw [h₁, erase_append_right _ h₂, erase_cons_head]
rw [range'_eq_append_iff] at h₁
obtain ⟨k, -, rfl, hbs⟩ := h₁
rw [eq_comm, range'_eq_cons_iff] at hbs
obtain ⟨rfl, -, rfl⟩ := hbs
simp at h
congr 2 <;> omega
· rw [erase_of_not_mem h]
simp only [mem_range'_1, not_and, Nat.not_lt] at h
by_cases h' : s ≤ i
· have p : min s (i + 1) + n - (i + 1) = 0 := by omega
simp [p]
omega
· have p : i - s = 0 := by omega
simp [p]
omegaInformal description
For any natural numbers $s$, $n$, and $i$, the result of removing the first occurrence of $i$ from the arithmetic sequence $\text{range'}\ s\ n$ (which is $[s, s+1, \dots, s+n-1]$) is equal to the concatenation of:
1. The subsequence from $s$ of length $\min(n, i - s)$, and
2. The subsequence starting at $\max(s, i + 1)$ of length $\min(s, i + 1) + n - (i + 1)$.
In other words:
$$ \text{erase}(\text{range'}\ s\ n, i) = \text{range'}\ s\ (\min(n, i - s)) \mathbin{+\kern-0.5em+} \text{range'}\ (\max(s, i + 1))\ (\min(s, i + 1) + n - (i + 1)) $$
List.reverse_range'
theorem
: ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
Full source
theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
| _, 0 => rfl
| s, n + 1 => by
rw [range'_1_concat, reverse_append, range_succ_eq_map,
show s + (n + 1) - 1 = s + n from rfl, map, map_map]
simp [reverse_range', Nat.sub_right_comm, Nat.sub_sub]Informal description
For any natural numbers $s$ and $n$, the reverse of the arithmetic sequence `range' s n` (which is $[s, s+1, \dots, s+n-1]$) is equal to the list obtained by mapping each element $k$ in `range n` (which is $[0, 1, \dots, n-1]$) to $s + n - 1 - k$.
In other words, $\text{reverse}(\text{range'}\ s\ n) = \text{map}\ (\lambda k \mapsto s + n - 1 - k)\ (\text{range}\ n)$.
List.mem_range
theorem
{m n : Nat} : m ∈ range n ↔ m < n
Full source
@[simp]
theorem mem_range {m n : Nat} : m ∈ range nm ∈ range n ↔ m < n := by
simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]Informal description
For any natural numbers $m$ and $n$, the number $m$ belongs to the list `range n` (which contains all natural numbers from $0$ to $n-1$) if and only if $m < n$.
In other words, $m \in [0, 1, \dots, n-1] \leftrightarrow m < n$.
List.not_mem_range_self
theorem
{n : Nat} : n ∉ range n
Full source
theorem not_mem_range_self {n : Nat} : n ∉ range n := by simpInformal description
For any natural number $n$, the number $n$ does not belong to the list `range n` (which contains all natural numbers from $0$ to $n-1$).
In other words, $n \notin [0, 1, \dots, n-1]$.
List.self_mem_range_succ
theorem
{n : Nat} : n ∈ range (n + 1)
Full source
theorem self_mem_range_succ {n : Nat} : n ∈ range (n + 1) := by simpInformal description
For any natural number $n$, the number $n$ is an element of the list `range (n + 1)`, which is the list of natural numbers from $0$ to $n$.
List.pairwise_lt_range
theorem
{n : Nat} : Pairwise (· < ·) (range n)
Full source
theorem pairwise_lt_range {n : Nat} : Pairwise (· < ·) (range n) := by
simp +decide only [range_eq_range', pairwise_lt_range']Informal description
For any natural number $n$, the list `range n` (which contains the natural numbers from $0$ to $n-1$) is strictly increasing. That is, for any two elements $a$ and $b$ in the list where $a$ appears before $b$, we have $a < b$.
List.pairwise_le_range
theorem
{n : Nat} : Pairwise (· ≤ ·) (range n)
Full source
theorem pairwise_le_range {n : Nat} : Pairwise (· ≤ ·) (range n) :=
Pairwise.imp Nat.le_of_lt pairwise_lt_rangeInformal description
For any natural number $n$, the list `range n` (which contains the natural numbers from $0$ to $n-1$) is non-decreasing. That is, for any two elements $a$ and $b$ in the list where $a$ appears before $b$, we have $a \leq b$.
List.take_range
theorem
{i n : Nat} : take i (range n) = range (min i n)
Full source
@[simp] theorem take_range {i n : Nat} : take i (range n) = range (min i n) := by
apply List.ext_getElem
· simp
· simp +contextual [getElem_take, Nat.lt_min]Informal description
For any natural numbers $i$ and $n$, taking the first $i$ elements of the list $[0, 1, \ldots, n-1]$ is equal to the list $[0, 1, \ldots, \min(i, n) - 1]$. That is,
$$\text{take}(i, \text{range}(n)) = \text{range}(\min(i, n)).$$
List.nodup_range
theorem
{n : Nat} : Nodup (range n)
Full source
theorem nodup_range {n : Nat} : Nodup (range n) := by
simp +decide only [range_eq_range', nodup_range']Informal description
For any natural number $n$, the list $[0, 1, \ldots, n-1]$ contains no duplicate elements.
List.find?_range_eq_some
theorem
{n : Nat} {i : Nat} {p : Nat → Bool} : (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j
Full source
@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
(range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
simp [range_eq_range']Informal description
For any natural numbers $n$ and $i$, and any predicate $p : \mathbb{N} \to \{\text{true}, \text{false}\}$, the function `find?` applied to the list `range n` and predicate $p$ returns `some i` if and only if:
1. $p(i)$ holds,
2. $i$ belongs to the list `[0, 1, ..., n-1]`, and
3. For all $j < i$, the predicate $p(j)$ does not hold.
List.find?_range_eq_none
theorem
{n : Nat} {p : Nat → Bool} : (range n).find? p = none ↔ ∀ i, i < n → !p i
Full source
theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
(range n).find? p = none ↔ ∀ i, i < n → !p i := by
simpInformal description
For any natural number $n$ and predicate $p : \mathbb{N} \to \{\text{true}, \text{false}\}$, the function `find?` applied to the list `range n` and predicate $p$ returns `none` if and only if for every natural number $i < n$, the predicate $p(i)$ evaluates to `false`.
List.erase_range
theorem
: (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1))
Full source
theorem erase_range : (range n).erase i = range (min n i) ++ range' (i + 1) (n - (i + 1)) := by
simp [range_eq_range', erase_range']Informal description
For any natural numbers $n$ and $i$, removing the first occurrence of $i$ from the list $[0, 1, \dots, n-1]$ results in the concatenation of:
1. The list $[0, 1, \dots, \min(n, i) - 1]$, and
2. The list $[i+1, i+2, \dots, n-1]$ (which is empty if $i+1 \geq n$).
In other words:
$$ \text{erase}([0, \dots, n-1], i) = [0, \dots, \min(n, i) - 1] \mathbin{+\kern-0.5em+} [i+1, \dots, n-1] $$
List.iota_eq_reverse_range'
theorem
: ∀ n : Nat, iota n = reverse (range' 1 n)
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
| 0 => rfl
| n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]Informal description
For any natural number $n$, the list $\text{iota}(n)$ (which contains the numbers from $n$ down to $1$) is equal to the reverse of the list $\text{range'}(1, n)$ (which contains the numbers from $1$ to $n$ in increasing order).
List.length_iota
theorem
(n : Nat) : length (iota n) = n
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']Informal description
For any natural number $n$, the length of the list $\operatorname{iota}(n)$ (which contains the numbers from $n$ down to $1$) is equal to $n$.
List.iota_eq_nil
theorem
{n : Nat} : iota n = [] ↔ n = 0
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem iota_eq_nil {n : Nat} : iotaiota n = [] ↔ n = 0 := by
cases n <;> simpInformal description
For any natural number $n$, the list `iota n` (which contains the numbers from $n$ down to $1$) is empty if and only if $n = 0$.
List.iota_ne_nil
theorem
{n : Nat} : iota n ≠ [] ↔ n ≠ 0
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem iota_ne_nil {n : Nat} : iotaiota n ≠ []iota n ≠ [] ↔ n ≠ 0 := by
cases n <;> simpInformal description
For any natural number $n$, the list $\operatorname{iota}(n)$ is non-empty if and only if $n$ is non-zero. In other words, $\operatorname{iota}(n) \neq [] \leftrightarrow n \neq 0$.
List.mem_iota
theorem
{m n : Nat} : m ∈ iota n ↔ 0 < m ∧ m ≤ n
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem mem_iota {m n : Nat} : m ∈ iota nm ∈ iota n ↔ 0 < m ∧ m ≤ n := by
simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]
omegaInformal description
For any natural numbers $m$ and $n$, the element $m$ belongs to the list $\operatorname{iota}(n)$ (which contains the numbers from $n$ down to $1$) if and only if $0 < m$ and $m \leq n$.
List.iota_inj
theorem
: iota n = iota n' ↔ n = n'
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem iota_inj : iotaiota n = iota n' ↔ n = n' := by
constructor
· intro h
have h' := congrArg List.length h
simp at h'
exact h'
· rintro rfl
simpInformal description
For any natural numbers $n$ and $n'$, the list $\operatorname{iota}(n)$ is equal to $\operatorname{iota}(n')$ if and only if $n = n'$.
List.iota_eq_cons_iff
theorem
: iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1)
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem iota_eq_cons_iff : iotaiota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1) := by
simp [iota_eq_reverse_range']
simp [range'_eq_append_iff, reverse_eq_iff]
constructor
· rintro ⟨k, h, rfl, h'⟩
rw [eq_comm, range'_eq_singleton] at h'
simp only [reverse_inj, range'_inj, or_true, and_true]
omega
· rintro ⟨rfl, h, rfl⟩
refine ⟨n - 1, by simp, rfl, ?_⟩
rw [eq_comm, range'_eq_singleton]
omegaInformal description
For any natural number $n$, the list $\operatorname{iota}(n) = [n, n-1, \dots, 1]$ is equal to the cons list $a :: xs$ if and only if $n = a$, $n > 0$, and $xs = \operatorname{iota}(n - 1)$.
List.iota_eq_append_iff
theorem
: iota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = iota k
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem iota_eq_append_iff : iotaiota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = iota k := by
simp only [iota_eq_reverse_range']
rw [reverse_eq_append_iff]
rw [range'_eq_append_iff]
simp only [reverse_eq_iff]
constructor
· rintro ⟨k, h, rfl, rfl⟩
simp; omega
· rintro ⟨k, h, rfl, rfl⟩
exact ⟨k, by simp; omega⟩Informal description
For any natural number $n$ and lists $xs, ys$ of natural numbers, the decreasing sequence $\operatorname{iota}(n) = [n, n-1, \ldots, 1]$ can be written as the concatenation $xs \mathbin{+\!\!+} ys$ if and only if there exists a natural number $k \leq n$ such that:
1. $xs$ is the reverse of the arithmetic sequence $\operatorname{range'}(k+1, n-k) = [k+1, k+2, \ldots, n]$, and
2. $ys$ is the decreasing sequence $\operatorname{iota}(k) = [k, k-1, \ldots, 1]$.
List.pairwise_gt_iota
theorem
(n : Nat) : Pairwise (· > ·) (iota n)
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n) := by
simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range'Informal description
For any natural number $n$, the list $\text{iota}(n) = [n, n-1, \dots, 1]$ satisfies the pairwise relation $>$ (i.e., every element is greater than all subsequent elements in the list).
List.nodup_iota
theorem
(n : Nat) : Nodup (iota n)
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem nodup_iota (n : Nat) : Nodup (iota n) :=
(pairwise_gt_iota n).imp Nat.ne_of_gtInformal description
For any natural number $n$, the list $\operatorname{iota}(n) = [n, n-1, \dots, 1]$ has no duplicate elements.
List.head?_iota
theorem
(n : Nat) : (iota n).head? = if n = 0 then none else some n
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n := by
cases n <;> simpInformal description
For any natural number $n$, the first element of the list $\text{iota}(n)$ (which contains the numbers from $n$ down to $1$) is $\text{some }n$ if $n \neq 0$, and $\text{none}$ if $n = 0$.
List.head_iota
theorem
(n : Nat) (h) : (iota n).head h = n
Informal description
For any natural number $n$ and proof $h$ that the list $\text{iota}(n)$ is non-empty, the head of $\text{iota}(n)$ is equal to $n$.
List.tail_iota
theorem
(n : Nat) : (iota n).tail = iota (n - 1)
Informal description
For any natural number $n$, the tail of the list $\text{iota}(n)$ (which contains the numbers from $n$ down to $1$) is equal to the list $\text{iota}(n-1)$.
List.reverse_iota
theorem
: reverse (iota n) = range' 1 n
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem reverse_iota : reverse (iota n) = range' 1 n := by
induction n with
| zero => simp
| succ n ih =>
rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]Informal description
For any natural number $n$, the reverse of the list $\mathrm{iota}(n) = [n, n-1, \dots, 1]$ is equal to the arithmetic sequence $\mathrm{range'}(1, n) = [1, 2, \dots, n]$.
List.getLast?_iota
theorem
(n : Nat) : (iota n).getLast? = if n = 0 then none else some 1
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1 := by
rw [getLast?_eq_head?_reverse]
simp [head?_range']Informal description
For any natural number $n$, the last element of the list $\mathrm{iota}(n) = [n, n-1, \dots, 1]$ is `none` if $n = 0$ and `some 1` otherwise.
More formally, $\mathrm{getLast?}(\mathrm{iota}(n)) = \begin{cases}
\text{none} & \text{if } n = 0 \\
\text{some } 1 & \text{otherwise}
\end{cases}$.
List.getLast_iota
theorem
(n : Nat) (h) : (iota n).getLast h = 1
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem getLast_iota (n : Nat) (h) : (iota n).getLast h = 1 := by
rw [getLast_eq_head_reverse]
simpInformal description
For any natural number $n$ and proof $h$ that the list $\mathrm{iota}(n) = [n, n-1, \dots, 1]$ is non-empty, the last element of $\mathrm{iota}(n)$ is $1$.
List.find?_iota_eq_none
theorem
{n : Nat} {p : Nat → Bool} : (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
(iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by
simpInformal description
For any natural number $n$ and predicate $p : \mathbb{N} \to \text{Bool}$, the function `find?` applied to the decreasing list `iota n` and predicate $p$ returns `none` if and only if for all natural numbers $i$ such that $0 < i \leq n$, the negation of $p(i)$ holds, i.e., $\neg p(i) = \texttt{true}$.
List.find?_iota_eq_some
theorem
{n : Nat} {i : Nat} {p : Nat → Bool} : (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j
Full source
@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
(iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
rw [find?_eq_some_iff_append]
simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
and_congr_right_iff]
intro h
constructor
· rintro ⟨as, ⟨xs, h⟩, h'⟩
constructor
· replace h : i ∈ range' 1 n := by
rw [h]
exact mem_append_cons_self
simpa using h
· rw [range'_eq_append_iff] at h
simp [reverse_eq_iff] at h
obtain ⟨k, h₁, rfl, h₂⟩ := h
rw [eq_comm, range'_eq_cons_iff, reverse_eq_iff] at h₂
obtain ⟨rfl, -, rfl⟩ := h₂
intro j j₁ j₂
apply h'
simp; omega
· rintro ⟨⟨i₁, i₂⟩, h⟩
refine ⟨(range' (i+1) (n-i)).reverse, ⟨(range' 1 (i-1)).reverse, ?_⟩, ?_⟩
· simp [← range'_succ]
rw [range'_eq_append_iff]
refine ⟨i-1, ?_⟩
constructor
· omega
· simp
omega
· simp
intros a a₁ a₂
apply h
· omega
· omegaInformal description
For any natural numbers $n$ and $i$, and any predicate $p : \mathbb{N} \to \text{Bool}$, the following are equivalent:
1. The function `find?` applied to the decreasing list $\text{iota}(n) = [n, n-1, \dots, 1]$ and predicate $p$ returns $\text{some } i$.
2. The predicate $p$ holds at $i$, $i$ is an element of $\text{iota}(n)$, and for all $j$ such that $i < j \leq n$, the predicate $p$ does not hold at $j$.
In other words, $\text{find?}(\text{iota}(n), p) = \text{some } i$ if and only if $i$ is the largest number in $\{1, \dots, n\}$ satisfying $p(i)$.
List.zipIdx_singleton
theorem
{x : α} {k : Nat} : zipIdx [x] k = [(x, k)]
Informal description
For any element $x$ of type $\alpha$ and any natural number $k$, the function `zipIdx` applied to the singleton list $[x]$ with starting index $k$ yields the list $[(x, k)]$.
List.head?_zipIdx
theorem
{l : List α} {k : Nat} : (zipIdx l k).head? = l.head?.map fun a => (a, k)
Full source
@[simp] theorem head?_zipIdx {l : List α} {k : Nat} :
(zipIdx l k).head? = l.head?.map fun a => (a, k) := by
simp [head?_eq_getElem?]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $k$, the optional head of the list obtained by pairing each element of $l$ with its index starting from $k$ (via `zipIdx l k`) is equal to the optional head of $l$ mapped to a pair with $k$. That is, if $l$ is non-empty with head $a$, then $\text{head?}(\text{zipIdx } l k) = \text{some } (a, k)$, otherwise both sides are $\text{none}$.
List.getLast?_zipIdx
theorem
{l : List α} {k : Nat} : (zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1)
Full source
@[simp] theorem getLast?_zipIdx {l : List α} {k : Nat} :
(zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1) := by
simp [getLast?_eq_getElem?]
cases l <;> simp; omegaInformal description
For any list $l$ of elements of type $\alpha$ and any natural number $k$, the optional last element of the list obtained by pairing each element of $l$ with its index starting from $k$ (via $\mathrm{zipIdx}\ l\ k$) is equal to the optional last element of $l$ mapped to a pair with $k + \mathrm{length}(l) - 1$. That is, if $l$ is non-empty with last element $a$, then $\mathrm{getLast?}(\mathrm{zipIdx}\ l\ k) = \mathrm{some}\ (a, k + \mathrm{length}(l) - 1)$, otherwise both sides are $\mathrm{none}$.
List.mk_add_mem_zipIdx_iff_getElem?
theorem
{k i : Nat} {x : α} {l : List α} : (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x
Full source
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : List α} :
(x, k + i)(x, k + i) ∈ zipIdx l k(x, k + i) ∈ zipIdx l k ↔ l[i]? = some x := by
simp [mem_iff_getElem?, and_left_comm]Informal description
For any natural numbers $k$ and $i$, any element $x$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the pair $(x, k + i)$ belongs to the list obtained by `zipIdx l k` if and only if the $i$-th element of $l$ (with 0-based indexing) is equal to $\text{some } x$.
List.mk_mem_zipIdx_iff_le_and_getElem?_sub
theorem
{k i : Nat} {x : α} {l : List α} : (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x
Full source
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : List α} :
(x, i)(x, i) ∈ zipIdx l k(x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x := by
if h : k ≤ i then
rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
simp [mk_add_mem_zipIdx_iff_getElem?, Nat.add_sub_cancel_left]
else
have : ∀ m, k + m ≠ i := by rintro _ rfl; simp at h
simp [h, mem_iff_getElem?, this]Informal description
For any natural numbers $k$ and $i$, any element $x$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the pair $(x, i)$ belongs to the list obtained by `zipIdx l k` if and only if $k \leq i$ and the optional element at index $i - k$ in $l$ is equal to $\text{some } x$.
In other words, $(x, i) \in \mathrm{zipIdx}(l, k) \leftrightarrow k \leq i \land l[i - k] = x$.
List.mk_mem_zipIdx_iff_getElem?
theorem
{i : Nat} {x : α} {l : List α} : (x, i) ∈ zipIdx l ↔ l[i]? = x
Full source
/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction. -/
theorem mk_mem_zipIdx_iff_getElem? {i : Nat} {x : α} {l : List α} : (x, i)(x, i) ∈ zipIdx l(x, i) ∈ zipIdx l ↔ l[i]? = x := by
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]Informal description
For any natural number index $i$, element $x$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the pair $(x, i)$ belongs to the list obtained by `zipIdx l` if and only if the optional element at index $i$ in $l$ is equal to $x$.
List.mem_zipIdx_iff_le_and_getElem?_sub
theorem
{x : α × Nat} {l : List α} {k : Nat} : x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1
Full source
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : List α} {k : Nat} :
x ∈ zipIdx l kx ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
cases x
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]Informal description
For any pair $(x, i)$ where $x$ is of type $\alpha$ and $i$ is a natural number, and for any list $l$ of elements of type $\alpha$ and natural number $k$, the pair $(x, i)$ is an element of the list obtained by `zipIdx l k` if and only if $k \leq i$ and the $(i - k)$-th element of $l$ (if it exists) is equal to $x$.
In other words, $(x, i) \in \mathrm{zipIdx}(l, k) \leftrightarrow k \leq i \land l[i - k] = x$.
List.mem_zipIdx_iff_getElem?
theorem
{x : α × Nat} {l : List α} : x ∈ zipIdx l ↔ l[x.2]? = some x.1
Full source
/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction. -/
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : List α} : x ∈ zipIdx lx ∈ zipIdx l ↔ l[x.2]? = some x.1 := by
cases x
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]Informal description
For any pair $(x, i)$ where $x$ is an element of type $\alpha$ and $i$ is a natural number, and for any list $l$ of elements of type $\alpha$, the pair $(x, i)$ belongs to the list obtained by `zipIdx l` if and only if the $i$-th element of $l$ (if it exists) is equal to $x$.
In other words, $(x, i) \in \mathrm{zipIdx}(l) \leftrightarrow l[i] = x$ (where $l[i]$ is the optional $i$-th element of $l$).
List.le_snd_of_mem_zipIdx
theorem
{x : α × Nat} {k : Nat} {l : List α} (h : x ∈ zipIdx l k) : k ≤ x.2
Full source
theorem le_snd_of_mem_zipIdx {x : α × Nat} {k : Nat} {l : List α} (h : x ∈ zipIdx l k) :
k ≤ x.2 :=
(mk_mem_zipIdx_iff_le_and_getElem?_sub.1 h).1Informal description
For any pair $(x, i)$ where $x$ is an element of type $\alpha$ and $i$ is a natural number, and for any list $l$ of elements of type $\alpha$ and starting index $k$, if $(x, i)$ belongs to the list obtained by `zipIdx l k`, then $k \leq i$.
List.snd_lt_add_of_mem_zipIdx
theorem
{x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) : x.2 < k + length l
Full source
theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
x.2 < k + length l := by
rcases mem_iff_get.1 h with ⟨i, rfl⟩
simpa using i.isLtInformal description
For any pair $(x, i)$ where $x$ is an element of type $\alpha$ and $i$ is a natural number, and for any list $l$ of elements of type $\alpha$ and starting index $k$, if $(x, i)$ belongs to the list obtained by `zipIdx l k`, then $i < k + \text{length}(l)$.
List.snd_lt_of_mem_zipIdx
theorem
{x : α × Nat} {l : List α} {k : Nat} (h : x ∈ l.zipIdx k) : x.2 < l.length + k
Full source
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ l.zipIdx k) : x.2 < l.length + k := by
simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx hInformal description
For any pair $(x, i)$ where $x$ is an element of type $\alpha$ and $i$ is a natural number, and for any list $l$ of elements of type $\alpha$ with starting index $k$, if $(x, i)$ belongs to the list obtained by `zipIdx l k`, then $i$ is strictly less than the sum of the length of $l$ and $k$, i.e., $i < \text{length}(l) + k$.
List.map_zipIdx
theorem
{f : α → β} {l : List α} {k : Nat} : map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k
Informal description
For any function $f : \alpha \to \beta$, list $l$ of type $\text{List}\ \alpha$, and natural number $k$, the following equality holds:
\[
\text{map}\ (\text{Prod.map}\ f\ \text{id})\ (\text{zipIdx}\ l\ k) = \text{zipIdx}\ (\text{map}\ f\ l)\ k
\]
Here, $\text{Prod.map}\ f\ \text{id}$ applies $f$ to the first component of each pair while leaving the second component unchanged, and $\text{zipIdx}\ l\ k$ pairs each element of $l$ with its index starting from $k$.
List.fst_mem_of_mem_zipIdx
theorem
{x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) : x.1 ∈ l
Full source
theorem fst_mem_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) : x.1 ∈ l :=
zipIdx_map_fst k l ▸ mem_map_of_mem hInformal description
For any pair $(x, i)$ in the list obtained by pairing elements of $l$ with indices starting from $k$ (i.e., $(x, i) \in \mathrm{zipIdx}\, l\, k$), the first component $x$ is an element of the original list $l$.
List.fst_eq_of_mem_zipIdx
theorem
{x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)
Full source
theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) := by
induction l generalizing k with
| nil => cases h
| cons hd tl ih =>
cases h with
| head _ => simp
| tail h m =>
specialize ih m
have : x.2 - k = x.2 - (k + 1) + 1 := by
have := le_snd_of_mem_zipIdx m
omega
simp [this, ih]Informal description
For any pair $(x, i)$ in the list obtained by pairing elements of $l$ with indices starting from $k$ (i.e., $(x, i) \in \mathrm{zipIdx}\, l\, k$), the first component $x$ equals the element of $l$ at position $i - k$.
More precisely, if $(x, i) \in \mathrm{zipIdx}\, l\, k$, then $x = l[i - k]$, where $i - k$ is a valid index for $l$ (i.e., $0 \leq i - k < \mathrm{length}(l)$).
List.mem_zipIdx
theorem
{x : α} {i : Nat} {xs : List α} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
k ≤ i ∧
i < k + xs.length ∧ x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)
Full source
theorem mem_zipIdx {x : α} {i : Nat} {xs : List α} {k : Nat} (h : (x, i)(x, i) ∈ xs.zipIdx k) :
k ≤ i ∧ i < k + xs.length ∧
x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
⟨le_snd_of_mem_zipIdx h, snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩Informal description
For any element $x$ of type $\alpha$, natural number $i$, list $xs$ of elements of type $\alpha$, and starting index $k$, if the pair $(x, i)$ belongs to the list obtained by pairing elements of $xs$ with indices starting from $k$ (i.e., $(x, i) \in \mathrm{zipIdx}\, xs\, k$), then the following conditions hold:
1. $k \leq i$,
2. $i < k + \mathrm{length}(xs)$, and
3. $x = xs[i - k]$, where $i - k$ is a valid index for $xs$.
List.mem_zipIdx'
theorem
{x : α} {i : Nat} {xs : List α} (h : (x, i) ∈ xs.zipIdx) :
i < xs.length ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega)
Full source
/-- Variant of `mem_zipIdx` specialized at `k = 0`. -/
theorem mem_zipIdx' {x : α} {i : Nat} {xs : List α} (h : (x, i)(x, i) ∈ xs.zipIdx) :
i < xs.length ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩Informal description
For any element $x$ of type $\alpha$, natural number $i$, and list $xs$ of elements of type $\alpha$, if the pair $(x, i)$ belongs to the list obtained by pairing elements of $xs$ with their indices (i.e., $(x, i) \in \mathrm{zipIdx}\, xs$), then $i$ is a valid index for $xs$ (i.e., $i < \mathrm{length}(xs)$) and $x$ is equal to the element of $xs$ at position $i$ (i.e., $x = xs[i]$).
List.zipIdx_map
theorem
{l : List α} {k : Nat} {f : α → β} : zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id)
Informal description
For any list $l$ of elements of type $\alpha$, any natural number $k$, and any function $f : \alpha \to \beta$, the indexed pairing of the mapped list $\mathrm{zipIdx}(\mathrm{map}\ f\ l, k)$ is equal to the mapped indexed pairing $(\mathrm{zipIdx}\ l\ k).\mathrm{map}\ (\mathrm{Prod.map}\ f\ \mathrm{id})$. In other words, mapping a function over a list and then pairing with indices is equivalent to first pairing with indices and then mapping the function over the first component of each pair.
List.zipIdx_append
theorem
{xs ys : List α} {k : Nat} : zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.length)
Full source
theorem zipIdx_append {xs ys : List α} {k : Nat} :
zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.length) := by
induction xs generalizing ys k with
| nil => simp
| cons x xs IH =>
rw [cons_append, zipIdx_cons, IH, ← cons_append, ← zipIdx_cons, length, Nat.add_right_comm,
Nat.add_assoc]Informal description
For any lists $xs$ and $ys$ of elements of type $\alpha$ and any natural number $k$, the indexed pairing of the concatenated list $\mathrm{zipIdx}(xs ++ ys, k)$ is equal to the concatenation of the indexed pairing of $xs$ starting at $k$ and the indexed pairing of $ys$ starting at $k + \mathrm{length}(xs)$. In other words:
$$ \mathrm{zipIdx}(xs \mathbin{+\!\!+} ys, k) = \mathrm{zipIdx}(xs, k) \mathbin{+\!\!+} \mathrm{zipIdx}(ys, k + |xs|) $$
List.zipIdx_eq_cons_iff
theorem
{l : List α} {k : Nat} : zipIdx l k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = zipIdx as (k + 1)
Full source
theorem zipIdx_eq_cons_iff {l : List α} {k : Nat} :
zipIdxzipIdx l k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = zipIdx as (k + 1) := by
rw [zipIdx_eq_zip_range', zip_eq_cons_iff]
constructor
· rintro ⟨l₁, l₂, rfl, h, rfl⟩
rw [range'_eq_cons_iff] at h
obtain ⟨rfl, -, rfl⟩ := h
exact ⟨x.1, l₁, by simp [zipIdx_eq_zip_range']⟩
· rintro ⟨a, as, rfl, rfl, rfl⟩
refine ⟨as, range' (k+1) as.length, ?_⟩
simp [zipIdx_eq_zip_range', range'_succ]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $k$, the indexed pairing $\mathrm{zipIdx}(l, k)$ equals a cons pair $x :: l'$ if and only if there exists an element $a$ and a sublist $as$ such that $l = a :: as$, $x = (a, k)$, and $l' = \mathrm{zipIdx}(as, k + 1)$.
List.zipIdx_eq_append_iff
theorem
{l : List α} {k : Nat} :
zipIdx l k = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + l₁'.length)
Full source
theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
zipIdxzipIdx l k = l₁ ++ l₂ ↔
∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + l₁'.length) := by
rw [zipIdx_eq_zip_range', zip_eq_append_iff]
constructor
· rintro ⟨ws, xs, ys, zs, h, rfl, h', rfl, rfl⟩
rw [range'_eq_append_iff] at h'
obtain ⟨k, -, rfl, rfl⟩ := h'
simp only [length_range'] at h
obtain rfl := h
refine ⟨ws, xs, rfl, ?_⟩
simp only [zipIdx_eq_zip_range', length_append, true_and]
congr
omega
· rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
simp only [zipIdx_eq_zip_range']
refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩
simp [Nat.add_comm]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number $k$, the indexed pairing $\mathrm{zipIdx}(l, k)$ equals the concatenation of two lists $l_1$ and $l_2$ if and only if there exist sublists $l_1'$ and $l_2'$ such that:
1. $l = l_1' \mathbin{+\!\!+} l_2'$,
2. $l_1 = \mathrm{zipIdx}(l_1', k)$,
3. $l_2 = \mathrm{zipIdx}(l_2', k + |l_1'|)$.
List.enumFrom_singleton
theorem
(x : α) (n : Nat) : enumFrom n [x] = [(n, x)]
Full source
@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
theorem enumFrom_singleton (x : α) (n : Nat) : enumFrom n [x] = [(n, x)] :=
rflInformal description
For any element $x$ of type $\alpha$ and any natural number $n$, the enumeration of the singleton list $[x]$ starting from index $n$ results in the list $[(n, x)]$.
List.head?_enumFrom
theorem
(n : Nat) (l : List α) : (enumFrom n l).head? = l.head?.map fun a => (n, a)
Full source
@[deprecated head?_zipIdx (since := "2025-01-21"), simp]
theorem head?_enumFrom (n : Nat) (l : List α) :
(enumFrom n l).head? = l.head?.map fun a => (n, a) := by
simp [head?_eq_getElem?]Informal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, the first element of the enumerated list (with indices starting from $n$) is equal to the first element of $l$ paired with $n$, if it exists. That is, $\text{head?}(\text{enumFrom } n l) = \text{map } (\lambda a \mapsto (n, a)) (\text{head? } l)$.
List.getLast?_enumFrom
theorem
(n : Nat) (l : List α) : (enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a)
Full source
@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
theorem getLast?_enumFrom (n : Nat) (l : List α) :
(enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a) := by
simp [getLast?_eq_getElem?]
cases l <;> simp; omegaInformal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, the last element of the enumerated list (with indices starting from $n$) is equal to the last element of $l$ paired with $n + \text{length}(l) - 1$, if it exists. That is, $\text{getLast?}(\text{enumFrom } n l) = \text{map } (\lambda a \mapsto (n + \text{length}(l) - 1, a)) (\text{getLast? } l)$.
List.mk_add_mem_enumFrom_iff_getElem?
theorem
{n i : Nat} {x : α} {l : List α} : (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x
Full source
@[deprecated mk_add_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
(n + i, x)(n + i, x) ∈ enumFrom n l(n + i, x) ∈ enumFrom n l ↔ l[i]? = some x := by
simp [mem_iff_get?]Informal description
For any natural numbers $n$ and $i$, any element $x$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the pair $(n + i, x)$ belongs to the enumerated list $\text{enumFrom } n l$ if and only if the $i$-th element of $l$ (using zero-based indexing) is equal to $\text{some } x$.
List.mk_mem_enumFrom_iff_le_and_getElem?_sub
theorem
{n i : Nat} {x : α} {l : List α} : (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = x
Full source
@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-21")]
theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List α} :
(i, x)(i, x) ∈ enumFrom n l(i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = x := by
if h : n ≤ i then
rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
simp [mk_add_mem_enumFrom_iff_getElem?, Nat.add_sub_cancel_left]
else
have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h
simp [h, mem_iff_get?, this]Informal description
For any natural numbers $n$ and $i$, any element $x$ of type $\alpha$, and any list $l$ of elements of type $\alpha$, the pair $(i, x)$ belongs to the enumerated list $\text{enumFrom } n l$ if and only if $n \leq i$ and the $(i - n)$-th element of $l$ (using zero-based indexing) is equal to $x$.
List.le_fst_of_mem_enumFrom
theorem
{x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : n ≤ x.1
Full source
@[deprecated le_snd_of_mem_zipIdx (since := "2025-01-21")]
theorem le_fst_of_mem_enumFrom {x : NatNat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
n ≤ x.1 :=
(mk_mem_enumFrom_iff_le_and_getElem?_sub.1 h).1Informal description
For any pair $(i, a)$ in the enumerated list `enumFrom n l`, where $n$ is a starting index and $l$ is a list of elements of type $\alpha$, the first component $i$ satisfies $n \leq i$.
List.fst_lt_add_of_mem_enumFrom
theorem
{x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.1 < n + length l
Full source
@[deprecated snd_lt_add_of_mem_zipIdx (since := "2025-01-21")]
theorem fst_lt_add_of_mem_enumFrom {x : NatNat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
x.1 < n + length l := by
rcases mem_iff_get.1 h with ⟨i, rfl⟩
simpa using i.isLtInformal description
For any pair $(i, a)$ in the enumerated list `enumFrom n l`, where $n$ is a starting index and $l$ is a list of elements of type $\alpha$, the first component $i$ satisfies $i < n + \text{length}(l)$.
List.map_enumFrom
theorem
(f : α → β) (n : Nat) (l : List α) : map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l)
Full source
@[deprecated map_zipIdx (since := "2025-01-21")]
theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
induction l generalizing n <;> simp_allInformal description
For any function $f : \alpha \to \beta$, natural number $n$, and list $l$ of elements of type $\alpha$, mapping $f$ over the second component of each pair in the enumerated list `enumFrom n l` is equivalent to enumerating the list obtained by mapping $f$ over $l$ starting from index $n$.
In symbols:
$$\text{map}\ (\text{id} \times f)\ (\text{enumFrom}\ n\ l) = \text{enumFrom}\ n\ (\text{map}\ f\ l)$$
where $\text{id} \times f$ denotes the function that applies $\text{id}$ to the first component and $f$ to the second component of a pair.
List.snd_mem_of_mem_enumFrom
theorem
{x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l
Full source
@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
theorem snd_mem_of_mem_enumFrom {x : NatNat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
enumFrom_map_snd n l ▸ mem_map_of_mem hInformal description
For any pair $x = (i, a)$ where $i$ is a natural number and $a$ is an element of type $\alpha$, if $x$ is in the list obtained by enumerating $l$ starting from index $n$ (i.e., $x \in \text{enumFrom}\, n\, l$), then the second component $a$ is an element of the original list $l$.
List.snd_eq_of_mem_enumFrom
theorem
{x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega)
Full source
@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
theorem snd_eq_of_mem_enumFrom {x : NatNat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) := by
induction l generalizing n with
| nil => cases h
| cons hd tl ih =>
cases h with
| head _ => simp
| tail h m =>
specialize ih m
have : x.1 - n = x.1 - (n + 1) + 1 := by
have := le_fst_of_mem_enumFrom m
omega
simp [this, ih]Informal description
For any pair $x = (i, a)$ in the enumerated list `enumFrom n l`, where $n$ is a starting index and $l$ is a list of elements of type $\alpha$, the second component $a$ is equal to the element of $l$ at index $i - n$. That is, $a = l[i - n]$.
List.mem_enumFrom
theorem
{x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enumFrom j) :
j ≤ i ∧
i < j + xs.length ∧ x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega)
Full source
@[deprecated mem_zipIdx (since := "2025-01-21")]
theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x)(i, x) ∈ xs.enumFrom j) :
j ≤ i ∧ i < j + xs.length ∧
x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩Informal description
For any element $x$ of type $\alpha$, natural numbers $i$ and $j$, and list $xs$ of elements of type $\alpha$, if the pair $(i, x)$ is in the enumerated list `xs.enumFrom j`, then the following conditions hold:
1. The starting index $j$ is less than or equal to $i$: $j \leq i$.
2. The index $i$ is strictly less than $j$ plus the length of $xs$: $i < j + \text{length}(xs)$.
3. The element $x$ is equal to the element of $xs$ at index $i - j$: $x = xs[i - j]$.
List.enumFrom_map
theorem
(n : Nat) (l : List α) (f : α → β) : enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f)
Full source
@[deprecated zipIdx_map (since := "2025-01-21")]
theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
induction l with
| nil => rfl
| cons hd tl IH =>
rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]
rflInformal description
For any natural number $n$, list $l$ of elements of type $\alpha$, and function $f : \alpha \to \beta$, enumerating the list $l.map\ f$ starting from index $n$ is equivalent to enumerating $l$ starting from $n$ and then mapping the function $\text{Prod.map}\ \text{id}\ f$ over the resulting list of pairs. In other words:
\[ \text{enumFrom}\ n\ (l.map\ f) = (\text{enumFrom}\ n\ l).map\ (\text{Prod.map}\ \text{id}\ f) \]
List.enumFrom_append
theorem
(xs ys : List α) (n : Nat) : enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys
Full source
@[deprecated zipIdx_append (since := "2025-01-21")]
theorem enumFrom_append (xs ys : List α) (n : Nat) :
enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys := by
induction xs generalizing ys n with
| nil => simp
| cons x xs IH =>
rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
Nat.add_assoc]Informal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$ and any natural number $n$, the enumeration of the concatenated list $xs ++ ys$ starting from index $n$ is equal to the concatenation of the enumeration of $xs$ starting from $n$ and the enumeration of $ys$ starting from $n + \text{length}(xs)$. That is,
\[ \text{enumFrom}\ n\ (xs ++ ys) = (\text{enumFrom}\ n\ xs) ++ (\text{enumFrom}\ (n + \text{length}(xs))\ ys). \]
List.enumFrom_eq_cons_iff
theorem
{l : List α} {n : Nat} : l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as
Full source
@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as := by
rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
constructor
· rintro ⟨l₁, l₂, h, rfl, rfl⟩
rw [range'_eq_cons_iff] at h
obtain ⟨rfl, -, rfl⟩ := h
exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩
· rintro ⟨a, as, rfl, rfl, rfl⟩
refine ⟨range' (n+1) as.length, as, ?_⟩
simp [enumFrom_eq_zip_range', range'_succ]Informal description
For a list $l$ of elements of type $\alpha$ and a natural number $n$, the enumeration of $l$ starting from index $n$ is equal to a pair $(x, l')$ if and only if there exists an element $a$ and a list $as$ such that $l = a :: as$, $x = (n, a)$, and $l'$ is the enumeration of $as$ starting from index $n + 1$.
List.enumFrom_eq_append_iff
theorem
{l : List α} {n : Nat} :
l.enumFrom n = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length)
Full source
@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
l.enumFrom n = l₁ ++ l₂ ↔
∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length) := by
rw [enumFrom_eq_zip_range', zip_eq_append_iff]
constructor
· rintro ⟨ws, xs, ys, zs, h, h', rfl, rfl, rfl⟩
rw [range'_eq_append_iff] at h'
obtain ⟨k, -, rfl, rfl⟩ := h'
simp only [length_range'] at h
obtain rfl := h
refine ⟨ys, zs, rfl, ?_⟩
simp only [enumFrom_eq_zip_range', length_append, true_and]
congr
omega
· rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
simp only [enumFrom_eq_zip_range']
refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
simp [Nat.add_comm]Informal description
For a list $l$ of elements of type $\alpha$ and a natural number $n$, the enumeration of $l$ starting from index $n$ (which pairs each element with its index starting from $n$) can be written as the concatenation of two lists $l_1$ and $l_2$ if and only if there exist sublists $l_1'$ and $l_2'$ such that:
1. $l = l_1' ++ l_2'$,
2. $l_1$ is the enumeration of $l_1'$ starting from $n$,
3. $l_2$ is the enumeration of $l_2'$ starting from $n + \text{length}(l_1')$.
In other words:
\[ \text{enumFrom}\ n\ l = l_1 ++ l_2 \leftrightarrow \exists l_1'\ l_2',\ l = l_1' ++ l_2' \land l_1 = \text{enumFrom}\ n\ l_1' \land l_2 = \text{enumFrom}\ (n + \text{length}(l_1'))\ l_2'. \]
List.enum_eq_nil_iff
theorem
{l : List α} : List.enum l = [] ↔ l = []
Full source
@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
theorem enum_eq_nil_iff {l : List α} : List.enumList.enum l = [] ↔ l = [] := enumFrom_eq_nilInformal description
For any list $l$ of elements of type $\alpha$, the enumeration of $l$ (which pairs each element with its index) is the empty list if and only if $l$ itself is the empty list. In other words, $\text{enum}(l) = [] \leftrightarrow l = []$.
List.enum_eq_nil
theorem
{l : List α} : List.enum l = [] ↔ l = []
Full source
@[deprecated zipIdx_eq_nil_iff (since := "2024-11-04")]
theorem enum_eq_nil {l : List α} : List.enumList.enum l = [] ↔ l = [] := enum_eq_nil_iffInformal description
For any list $l$ of elements of type $\alpha$, the enumeration of $l$ (which pairs each element with its index) is the empty list if and only if $l$ itself is the empty list. In other words, $\text{enum}(l) = [] \leftrightarrow l = []$.
List.enum_singleton
theorem
(x : α) : enum [x] = [(0, x)]
Full source
@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rflInformal description
For any element $x$ of type $\alpha$, the enumeration of the singleton list $[x]$ is equal to the list $[(0, x)]$.
List.enum_length
theorem
: (enum l).length = l.length
Full source
@[deprecated length_zipIdx (since := "2025-01-21"), simp]
theorem enum_length : (enum l).length = l.length :=
enumFrom_lengthInformal description
For any list $l$ of elements of type $\alpha$, the length of the enumerated list $\text{enum}(l)$ is equal to the length of $l$. That is, $|\text{enum}(l)| = |l|$.
List.getElem?_enum
theorem
(l : List α) (i : Nat) : (enum l)[i]? = l[i]?.map fun a => (i, a)
Full source
@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
theorem getElem?_enum (l : List α) (i : Nat) : (enum l)[i]? = l[i]?.map fun a => (i, a) := by
rw [enum, getElem?_enumFrom, Nat.zero_add]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number index $i$, the optional lookup operation on the enumerated list $\text{enum}\ l$ at index $i$ is equal to the optional lookup operation on $l$ at index $i$ mapped to a pair $(i, a)$, where $a$ is the element at index $i$ in $l$ (if it exists).
In other words, if $l[i]?$ returns $\text{some}\ a$, then $(\text{enum}\ l)[i]?$ returns $\text{some}\ (i, a)$; otherwise, both operations return $\text{none}$.
List.getElem_enum
theorem
(l : List α) (i : Nat) (h : i < l.enum.length) : l.enum[i] = (i, l[i]'(by simpa [enum_length] using h))
Full source
@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
l.enum[i] = (i, l[i]'(by simpa [enum_length] using h)) := by
simp [enum]Informal description
For any list $l$ of elements of type $\alpha$ and any natural number index $i$ such that $i < \text{length}(\text{enum}(l))$, the $i$-th element of the enumerated list $\text{enum}(l)$ is equal to the pair $(i, l[i])$, where $l[i]$ is the $i$-th element of $l$.
List.head?_enum
theorem
(l : List α) : l.enum.head? = l.head?.map fun a => (0, a)
Full source
@[deprecated head?_zipIdx (since := "2025-01-21"), simp] theorem head?_enum (l : List α) :
l.enum.head? = l.head?.map fun a => (0, a) := by
simp [head?_eq_getElem?]Informal description
For any list $l$ of elements of type $\alpha$, the optional head of the enumerated list $\text{enum}(l)$ is equal to the optional head of $l$ mapped to a pair $(0, a)$, where $a$ is the head element of $l$ (if it exists).
In other words, if $l.\text{head?}$ returns $\text{some}\ a$, then $\text{enum}(l).\text{head?}$ returns $\text{some}\ (0, a)$; otherwise, both operations return $\text{none}$.
List.getLast?_enum
theorem
(l : List α) : l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a)
Full source
@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
theorem getLast?_enum (l : List α) :
l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
simp [getLast?_eq_getElem?]Informal description
For any list $l$ of elements of type $\alpha$, the optional last element of the enumerated list $\text{enum}(l)$ is equal to the optional last element of $l$ mapped to a pair $(|l| - 1, a)$, where $a$ is the last element of $l$ (if it exists).
In other words, if $l.\text{getLast?}$ returns $\text{some}\ a$, then $\text{enum}(l).\text{getLast?}$ returns $\text{some}\ (|l| - 1, a)$; otherwise, both operations return $\text{none}$.
List.tail_enum
theorem
(l : List α) : (enum l).tail = enumFrom 1 l.tail
Informal description
For any list $l$ of elements of type $\alpha$, the tail of the enumerated list $\text{enum}(l)$ is equal to the enumeration of the tail of $l$ starting from index $1$. That is, $(\text{enum}(l)).\text{tail} = \text{enumFrom}(1, l.\text{tail})$.
List.mk_mem_enum_iff_getElem?
theorem
{i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x
Full source
@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x)(i, x) ∈ enum l(i, x) ∈ enum l ↔ l[i]? = x := by
simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]Informal description
For any natural number $i$, element $x$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the pair $(i, x)$ belongs to the enumerated version of $l$ (i.e., the list of pairs $(0, l_0), (1, l_1), \dots$) if and only if the optional lookup of the $i$-th element of $l$ equals $x$.
List.mem_enum_iff_getElem?
theorem
{x : Nat × α} {l : List α} : x ∈ enum l ↔ l[x.1]? = some x.2
Full source
@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
theorem mem_enum_iff_getElem? {x : NatNat × α} {l : List α} : x ∈ enum lx ∈ enum l ↔ l[x.1]? = some x.2 :=
mk_mem_enum_iff_getElem?Informal description
For any pair $(i, a)$ where $i$ is a natural number and $a$ is an element of type $\alpha$, and for any list $l$ of elements of type $\alpha$, the pair $(i, a)$ belongs to the enumerated list $\text{enum}\, l$ if and only if the optional lookup of the $i$-th element of $l$ returns $\text{some}\, a$.
List.fst_lt_of_mem_enum
theorem
{x : Nat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l
Full source
@[deprecated snd_lt_of_mem_zipIdx (since := "2025-01-21")]
theorem fst_lt_of_mem_enum {x : NatNat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l := by
simpa using fst_lt_add_of_mem_enumFrom hInformal description
For any pair $(i, a)$ in the enumerated list $\text{enum}\, l$, where $l$ is a list of elements of type $\alpha$, the index $i$ satisfies $i < \text{length}(l)$.
List.snd_mem_of_mem_enum
theorem
{x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l
Full source
@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
theorem snd_mem_of_mem_enum {x : NatNat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l :=
snd_mem_of_mem_enumFrom hInformal description
For any pair $(i, a)$ where $i$ is a natural number and $a$ is an element of type $\alpha$, if $(i, a)$ belongs to the enumerated list $\text{enum}\, l$, then $a$ is an element of the original list $l$.
List.snd_eq_of_mem_enum
theorem
{x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 = l[x.1]'(fst_lt_of_mem_enum h)
Full source
@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
theorem snd_eq_of_mem_enum {x : NatNat × α} {l : List α} (h : x ∈ enum l) :
x.2 = l[x.1]'(fst_lt_of_mem_enum h) :=
snd_eq_of_mem_enumFrom hInformal description
For any pair $(i, a)$ in the enumerated list $\text{enum}\, l$, where $l$ is a list of elements of type $\alpha$, the second component $a$ is equal to the element of $l$ at index $i$. That is, $a = l[i]$.
List.mem_enum
theorem
{x : α} {i : Nat} {xs : List α} (h : (i, x) ∈ xs.enum) : i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h)
Full source
@[deprecated mem_zipIdx (since := "2025-01-21")]
theorem mem_enum {x : α} {i : Nat} {xs : List α} (h : (i, x)(i, x) ∈ xs.enum) :
i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h) :=
by simpa using mem_enumFrom hInformal description
For any element $x$ of type $\alpha$, natural number $i$, and list $xs$ of elements of type $\alpha$, if the pair $(i, x)$ belongs to the enumerated list $\text{enum}(xs)$, then:
1. The index $i$ is less than the length of $xs$: $i < \text{length}(xs)$.
2. The element $x$ equals the $i$-th element of $xs$: $x = xs[i]$.
List.map_enum
theorem
(f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l)
Full source
@[deprecated map_zipIdx (since := "2025-01-21")]
theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) :=
map_enumFrom f 0 lInformal description
For any function $f : \alpha \to \beta$ and list $l$ of elements of type $\alpha$, mapping $f$ over the second component of each pair in the enumerated list $\text{enum}(l)$ is equivalent to enumerating the list obtained by mapping $f$ over $l$.
In symbols:
$$\text{map}\ (\text{id} \times f)\ (\text{enum}\ l) = \text{enum}\ (\text{map}\ f\ l)$$
where $\text{id} \times f$ denotes the function that applies $\text{id}$ to the first component and $f$ to the second component of a pair.
List.enum_map_fst
theorem
(l : List α) : map Prod.fst (enum l) = range l.length
Full source
@[deprecated zipIdx_map_snd (since := "2025-01-21"), simp]
theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by
simp only [enum, enumFrom_map_fst, range_eq_range']Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by mapping the first projection function (extracting the index) over the enumerated pairs of $l$ is equal to the list of natural numbers from $0$ to $\text{length}(l) - 1$.
In other words, if we enumerate the elements of $l$ as $(0, x_0), (1, x_1), \ldots, (n-1, x_{n-1})$ where $n = \text{length}(l)$, then extracting just the indices gives us the list $[0, 1, \ldots, n-1] = \text{range}(n)$.
List.enum_map_snd
theorem
(l : List α) : map Prod.snd (enum l) = l
Full source
@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
theorem enum_map_snd (l : List α) : map Prod.snd (enum l) = l :=
enumFrom_map_snd _ _Informal description
For any list $l$ of elements of type $\alpha$, the list obtained by mapping the second projection function $\text{snd}$ over the enumerated pairs of $l$ is equal to $l$ itself. In other words, if we enumerate $l$ to get pairs of indices and elements, and then extract just the elements, we recover the original list $l$.
List.enum_map
theorem
(l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Prod.map id f)
Full source
@[deprecated zipIdx_map (since := "2025-01-21")]
theorem enum_map (l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Prod.map id f) :=
enumFrom_map _ _ _Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \beta$, the enumeration of the mapped list $l.map\ f$ is equal to the enumeration of $l$ with the function $\text{id} \times f$ applied to each pair. In other words:
\[ \text{enum}(l.map\ f) = \text{enum}(l).map (\text{id} \times f) \]
List.enum_append
theorem
(xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys
Full source
@[deprecated zipIdx_append (since := "2025-01-21")]
theorem enum_append (xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys := by
simp [enum, enumFrom_append]Informal description
For any two lists $xs$ and $ys$ of elements of type $\alpha$, the enumeration of the concatenated list $xs ++ ys$ is equal to the concatenation of the enumeration of $xs$ and the enumeration of $ys$ starting from index $\text{length}(xs)$.
In other words:
\[ \text{enum}(xs ++ ys) = \text{enum}(xs) ++ \text{enumFrom}(\text{length}(xs), ys) \]
List.enum_eq_zip_range
theorem
(l : List α) : l.enum = (range l.length).zip l
Full source
@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
theorem enum_eq_zip_range (l : List α) : l.enum = (range l.length).zip l :=
zip_of_prod (enum_map_fst _) (enum_map_snd _)Informal description
For any list $l$ of elements of type $\alpha$, the enumeration of $l$ (a list of pairs $(i, x_i)$ where $i$ is the index and $x_i$ is the $i$-th element of $l$) is equal to the zip of the list $[0, 1, \ldots, \text{length}(l) - 1]$ with $l$ itself.
In other words, if $l = [x_0, x_1, \ldots, x_{n-1}]$, then:
\[ \text{enum}(l) = [(0, x_0), (1, x_1), \ldots, (n-1, x_{n-1})] = \text{zip}\ ([0, \ldots, n-1])\ l \]
List.unzip_enum_eq_prod
theorem
(l : List α) : l.enum.unzip = (range l.length, l)
Full source
@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), simp]
theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l) := by
simp only [enum_eq_zip_range, unzip_zip, length_range]Informal description
For any list $l$ of elements of type $\alpha$, the unzipping of the enumeration of $l$ (a list of pairs $(i, x_i)$ where $i$ is the index and $x_i$ is the $i$-th element of $l$) equals the pair consisting of the list $[0, 1, \ldots, \text{length}(l) - 1]$ and the original list $l$.
In other words, if $l = [x_0, x_1, \ldots, x_{n-1}]$, then:
\[ \text{unzip}(\text{enum}(l)) = ([0, \ldots, n-1], l) \]
List.enum_eq_cons_iff
theorem
{l : List α} : l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as
Full source
@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
theorem enum_eq_cons_iff {l : List α} :
l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as := by
rw [enum, enumFrom_eq_cons_iff]Informal description
For a list $l$ of elements of type $\alpha$, the enumeration of $l$ is equal to a pair $(x, l')$ if and only if there exists an element $a$ and a list $as$ such that $l = a :: as$, $x = (0, a)$, and $l'$ is the enumeration of $as$ starting from index $1$.
List.enum_eq_append_iff
theorem
{l : List α} : l.enum = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = l₂'.enumFrom l₁'.length
Full source
@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
theorem enum_eq_append_iff {l : List α} :
l.enum = l₁ ++ l₂ ↔
∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = l₂'.enumFrom l₁'.length := by
simp [enum, enumFrom_eq_append_iff]Informal description
For any list $l$ of elements of type $\alpha$, the enumeration of $l$ (a list of pairs $(i, x_i)$ where $i$ is the index and $x_i$ is the $i$-th element of $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{+\!\!+} l_2'$ (where $\mathbin{+\!\!+}$ denotes list concatenation),
2. $l_1$ is the enumeration of $l_1'$ (with indices starting at 0), and
3. $l_2$ is the enumeration of $l_2'$ with indices starting at the length of $l_1'$.