Module docstring
{"# Lemmas about List.zip, List.zipWith, List.zipWithAll, and List.unzip.
","## Zippers ","### zipWith ","### zip ","### zipWithAll ","### unzip "}
List.zipWith_comm
theorem
{f : α → β → γ} : ∀ {as : List α} {bs : List β}, zipWith f as bs = zipWith (fun b a => f a b) bs as
Informal description
For any function $f : \alpha \to \beta \to \gamma$ and any lists $as : \text{List } \alpha$, $bs : \text{List } \beta$, the zip of $as$ and $bs$ with $f$ is equal to the zip of $bs$ and $as$ with the arguments of $f$ reversed. That is,
\[ \text{zipWith } f \ as \ bs = \text{zipWith } (\lambda b \ a, f \ a \ b) \ bs \ as. \]
List.zipWith_comm_of_comm
theorem
{f : α → α → β} (comm : ∀ x y : α, f x y = f y x) {l l' : List α} : zipWith f l l' = zipWith f l' l
Full source
theorem zipWith_comm_of_comm {f : α → α → β} (comm : ∀ x y : α, f x y = f y x) {l l' : List α} :
zipWith f l l' = zipWith f l' l := by
rw [zipWith_comm]
simp only [comm]Informal description
For any commutative function $f : \alpha \to \alpha \to \beta$ (i.e., $f(x, y) = f(y, x)$ for all $x, y \in \alpha$) and any lists $l, l'$ of elements of type $\alpha$, the zip of $l$ and $l'$ with $f$ is equal to the zip of $l'$ and $l$ with $f$. That is,
\[ \text{zipWith } f \ l \ l' = \text{zipWith } f \ l' \ l. \]
List.zipWith_self
theorem
{f : α → α → δ} : ∀ {l : List α}, zipWith f l l = l.map fun a => f a a
Informal description
For any function $f : \alpha \to \alpha \to \delta$ and any list $l$ of elements of type $\alpha$, the list obtained by applying $f$ pairwise to elements of $l$ with itself (via `zipWith`) is equal to the list obtained by mapping each element $a$ of $l$ to $f(a,a)$. In other words:
$$\text{zipWith}(f, l, l) = \text{map} (\lambda a, f(a,a)) l$$
List.zipWith_same
abbrev
Full source
@[deprecated zipWith_self (since := "2025-01-29")] abbrev zipWith_same := @zipWith_selfInformal description
For any function $f : \alpha \to \alpha \to \delta$ and any list $l$ of elements of type $\alpha$, the list obtained by applying $f$ pairwise to elements of $l$ with itself (via `zipWith`) is equal to the list obtained by mapping each element $a$ of $l$ to $f(a,a)$. In other words:
$$\text{zipWith}(f, l, l) = \text{map} (\lambda a, f(a,a)) l$$
List.getElem?_zipWith
theorem
{f : α → β → γ} {i : Nat} :
(zipWith f as bs)[i]? =
match as[i]?, bs[i]? with
| some a, some b => some (f a b)
| _, _ => none
Full source
/--
See also `getElem?_zipWith'` for a variant
using `Option.map` and `Option.bind` rather than a `match`.
-/
theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
(zipWith f as bs)[i]? = match as[i]?, bs[i]? with
| some a, some b => some (f a b) | _, _ => none := by
induction as generalizing bs i with
| nil => cases bs with
| nil => simp
| cons b bs => simp
| cons a as aih => cases bs with
| nil => simp
| cons b bs => cases i <;> simp_allInformal description
For any function $f : \alpha \to \beta \to \gamma$, natural number index $i$, and lists `as` and `bs` of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, the optional indexing operation on the list obtained by applying $f$ pairwise to elements of `as` and `bs` (via `zipWith`) satisfies:
$$(\text{zipWith}(f, \text{as}, \text{bs}))[i]? =
\begin{cases}
\text{some}(f(a, b)) & \text{if } \text{as}[i]? = \text{some}(a) \text{ and } \text{bs}[i]? = \text{some}(b), \\
\text{none} & \text{otherwise.}
\end{cases}$$
List.getElem?_zipWith'
theorem
{f : α → β → γ} {i : Nat} : (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g
Full source
/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`. -/
theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
(zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g := by
induction l₁ generalizing l₂ i with
| nil => rw [zipWith] <;> simp
| cons _ _ =>
cases l₂
· simp
· cases i <;> simp_allInformal description
For any function $f : \alpha \to \beta \to \gamma$ and natural number index $i$, the optional indexing operation on the list obtained by applying $f$ pairwise to elements of lists $l_1$ and $l_2$ (via `zipWith`) is equal to first mapping $f$ over the $i$-th element of $l_1$ (if it exists) and then binding this with mapping over the $i$-th element of $l_2$ (if it exists).
In symbols:
$$(\text{zipWith}\,f\,l_1\,l_2)[i]? = (l_1[i]?.map\,f).bind\,(\lambda g, l_2[i]?.map\,g)$$
List.getElem?_zipWith_eq_some
theorem
{f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : Nat} :
(zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
Full source
theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : Nat} :
(zipWith f l₁ l₂)[i]?(zipWith f l₁ l₂)[i]? = some z ↔
∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z := by
induction l₁ generalizing l₂ i
· simp
· cases l₂ <;> cases i <;> simp_allInformal description
For any function $f : \alpha \to \beta \to \gamma$, lists $l_1$ of type $\text{List}\,\alpha$ and $l_2$ of type $\text{List}\,\beta$, element $z : \gamma$, and natural number index $i$, the optional indexing operation $\text{zipWith}\,f\,l_1\,l_2[i]?$ returns $\text{some}\,z$ if and only if there exist elements $x \in \alpha$ and $y \in \beta$ such that $l_1[i]? = \text{some}\,x$, $l_2[i]? = \text{some}\,y$, and $f\,x\,y = z$.
List.getElem?_zip_eq_some
theorem
{l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} : (zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2
Full source
theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} :
(zip l₁ l₂)[i]?(zip l₁ l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2 := by
cases z
rw [zip, getElem?_zipWith_eq_some]; constructor
· rintro ⟨x, y, h₀, h₁, h₂⟩
simpa [h₀, h₁] using h₂
· rintro ⟨h₀, h₁⟩
exact ⟨_, _, h₀, h₁, rfl⟩Informal description
For any lists $l_1$ of type $\text{List}\,\alpha$ and $l_2$ of type $\text{List}\,\beta$, element $z \in \alpha \times \beta$, and natural number index $i$, the optional indexing operation $\text{zip}\,l_1\,l_2[i]?$ returns $\text{some}\,z$ if and only if $l_1[i]? = \text{some}\,z.1$ and $l_2[i]? = \text{some}\,z.2$, where $z.1$ and $z.2$ are the first and second components of $z$ respectively.
List.head?_zipWith
theorem
{f : α → β → γ} :
(List.zipWith f as bs).head? =
match as.head?, bs.head? with
| some a, some b => some (f a b)
| _, _ => none
Full source
theorem head?_zipWith {f : α → β → γ} :
(List.zipWith f as bs).head? = match as.head?, bs.head? with
| some a, some b => some (f a b) | _, _ => none := by
simp [head?_eq_getElem?, getElem?_zipWith]Informal description
For any function $f : \alpha \to \beta \to \gamma$ and lists $\text{as}$ and $\text{bs}$ of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, the optional head of the list obtained by applying $f$ pairwise to elements of $\text{as}$ and $\text{bs}$ (via $\text{zipWith}$) satisfies:
\[
(\text{zipWith}\,f\,\text{as}\,\text{bs}).\text{head?} =
\begin{cases}
\text{some}(f\,a\,b) & \text{if } \text{as}.\text{head?} = \text{some}\,a \text{ and } \text{bs}.\text{head?} = \text{some}\,b, \\
\text{none} & \text{otherwise.}
\end{cases}
\]
List.head_zipWith
theorem
{f : α → β → γ} (h) :
(List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all))
Full source
theorem head_zipWith {f : α → β → γ} (h):
(List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all)) := by
apply Option.some.inj
rw [← head?_eq_head, head?_zipWith, head?_eq_head, head?_eq_head]Informal description
For any function $f : \alpha \to \beta \to \gamma$ and nonempty lists `as` and `bs` of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, the head of the list obtained by applying $f$ pairwise to elements of `as` and `bs` (via $\text{zipWith}$) satisfies:
\[
(\text{zipWith}\,f\,\text{as}\,\text{bs}).\text{head} = f\,(\text{as}.\text{head})\,(\text{bs}.\text{head})
\]
where the nonemptiness of `as` and `bs` is ensured by the proof `h`.
List.zipWith_map
theorem
{μ} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂
Informal description
For any types $\alpha, \beta, \gamma, \delta, \mu$, any functions $f : \gamma \to \delta \to \mu$, $g : \alpha \to \gamma$, $h : \beta \to \delta$, and any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the following equality holds:
\[
\text{zipWith } f \ (l_1.\text{map } g) \ (l_2.\text{map } h) = \text{zipWith } (\lambda a\ b,\ f\ (g\ a)\ (h\ b)) \ l_1 \ l_2
\]
where $\text{zipWith}$ combines two lists element-wise using a given function, and $\text{map}$ applies a function to each element of a list.
List.zipWith_map_left
theorem
{l₁ : List α} {l₂ : List β} {f : α → α'} {g : α' → β → γ} :
zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂
Informal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, and any functions $f : \alpha \to \alpha'$ and $g : \alpha' \to \beta \to \gamma$, the following equality holds:
\[
\text{zipWith } g \ (l_1.\text{map } f) \ l_2 = \text{zipWith } (\lambda a\ b,\ g\ (f\ a)\ b) \ l_1 \ l_2
\]
Here, $\text{zipWith}$ combines two lists element-wise using a given function, and $\text{map}$ applies a function to each element of a list.
List.zipWith_map_right
theorem
{l₁ : List α} {l₂ : List β} {f : β → β'} {g : α → β' → γ} :
zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂
Informal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, and any functions $f : \beta \to \beta'$ and $g : \alpha \to \beta' \to \gamma$, the following equality holds:
\[
\text{zipWith } g \ l_1 \ (l_2.\text{map } f) = \text{zipWith } (\lambda a\ b,\ g\ a\ (f\ b)) \ l_1 \ l_2
\]
Here, $\text{zipWith}$ combines two lists element-wise using a given function, and $\text{map}$ applies a function to each element of a list.
List.zipWith_foldr_eq_zip_foldr
theorem
{f : α → β → γ} {i : δ} {g : γ → δ → δ} :
(zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i
Informal description
For any function $f : \alpha \to \beta \to \gamma$, initial value $i : \delta$, and combining function $g : \gamma \to \delta \to \delta$, the right fold over the list obtained by zipping two lists $l_1$ and $l_2$ with $f$ is equal to the right fold over the list of pairs obtained by zipping $l_1$ and $l_2$, where each pair $(a, b)$ is first transformed by $f(a, b)$ before being combined with the accumulator using $g$.
More precisely, for any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, we have:
\[
\text{foldr } g \ i \ (\text{zipWith } f \ l_1 \ l_2) = \text{foldr } (\lambda (a, b) \ r,\ g (f \ a \ b) \ r) \ i \ (\text{zip } l_1 \ l_2)
\]
List.zipWith_foldl_eq_zip_foldl
theorem
{f : α → β → γ} {i : δ} {g : δ → γ → δ} :
(zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i
Informal description
For any function $f : \alpha \to \beta \to \gamma$, initial value $i : \delta$, and combining function $g : \delta \to \gamma \to \delta$, the left fold over the list obtained by zipping two lists $l_1$ and $l_2$ with $f$ is equal to the left fold over the list of pairs obtained by zipping $l_1$ and $l_2$, where each pair $(a, b)$ is first transformed by $f(a, b)$ before being combined with the accumulator using $g$.
More precisely, for any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, we have:
\[
\text{foldl } g \ i \ (\text{zipWith } f \ l_1 \ l_2) = \text{foldl } (\lambda r \ (a, b),\ g \ r \ (f \ a \ b)) \ i \ (\text{zip } l_1 \ l_2)
\]
List.zipWith_eq_nil_iff
theorem
{f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = []
Full source
@[simp]
theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWithzipWith f l l' = [] ↔ l = [] ∨ l' = [] := by
cases l <;> cases l' <;> simpInformal description
For any function $f : \alpha \to \beta \to \gamma$ and any lists $l$ of type $\alpha$ and $l'$ of type $\beta$, the list obtained by applying $f$ pairwise to elements of $l$ and $l'$ is empty if and only if either $l$ is empty or $l'$ is empty. In other words:
\[
\text{zipWith } f\ l\ l' = [] \leftrightarrow l = [] \lor l' = []
\]
List.map_zipWith
theorem
{δ : Type _} {f : α → β} {g : γ → δ → α} {l : List γ} {l' : List δ} :
map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'
Informal description
For any types $\alpha, \beta, \gamma, \delta$, any function $f : \alpha \to \beta$, any function $g : \gamma \to \delta \to \alpha$, and any lists $l : \text{List } \gamma$ and $l' : \text{List } \delta$, the following equality holds:
\[ \text{map } f (\text{zipWith } g\ l\ l') = \text{zipWith } (\lambda x\ y, f (g\ x\ y))\ l\ l' \]
List.take_zipWith
theorem
: (zipWith f l l').take i = zipWith f (l.take i) (l'.take i)
Informal description
For any function $f : \alpha \to \beta \to \gamma$, lists $l : \text{List } \alpha$ and $l' : \text{List } \beta$, and natural number $i$, the first $i$ elements of the list obtained by applying $f$ pairwise to elements of $l$ and $l'$ is equal to the list obtained by applying $f$ pairwise to the first $i$ elements of $l$ and the first $i$ elements of $l'$. In other words:
\[
\text{take } i\ (\text{zipWith } f\ l\ l') = \text{zipWith } f\ (\text{take } i\ l)\ (\text{take } i\ l')
\]
List.drop_zipWith
theorem
: (zipWith f l l').drop i = zipWith f (l.drop i) (l'.drop i)
Informal description
For any function $f : \alpha \to \beta \to \gamma$ and any lists $l : \text{List } \alpha$ and $l' : \text{List } \beta$, dropping the first $i$ elements from the list obtained by applying $\text{zipWith}$ to $f$, $l$, and $l'$ is equivalent to applying $\text{zipWith}$ to $f$ and the lists obtained by dropping the first $i$ elements from $l$ and $l'$ respectively. That is:
\[ \text{drop } i (\text{zipWith } f\ l\ l') = \text{zipWith } f (\text{drop } i\ l) (\text{drop } i\ l') \]
List.tail_zipWith
theorem
: (zipWith f l l').tail = zipWith f l.tail l'.tail
Full source
@[simp]
theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by
rw [← drop_one]; simp [drop_zipWith]Informal description
For any function $f : \alpha \to \beta \to \gamma$ and any lists $l : \text{List } \alpha$ and $l' : \text{List } \beta$, the tail of the list obtained by applying $\text{zipWith}$ to $f$, $l$, and $l'$ is equal to the list obtained by applying $\text{zipWith}$ to $f$ and the tails of $l$ and $l'$. That is:
\[ \text{tail } (\text{zipWith } f\ l\ l') = \text{zipWith } f\ (\text{tail } l)\ (\text{tail } l') \]
List.zipWith_append
theorem
{f : α → β → γ} {l₁ l₁' : List α} {l₂ l₂' : List β} (h : l₁.length = l₂.length) :
zipWith f (l₁ ++ l₁') (l₂ ++ l₂') = zipWith f l₁ l₂ ++ zipWith f l₁' l₂'
Full source
theorem zipWith_append {f : α → β → γ} {l₁ l₁' : List α} {l₂ l₂' : List β}
(h : l₁.length = l₂.length) :
zipWith f (l₁ ++ l₁') (l₂ ++ l₂') = zipWith f l₁ l₂ ++ zipWith f l₁' l₂' := by
induction l₁ generalizing l₂ with
| nil =>
have : l₂ = [] := eq_nil_of_length_eq_zero (by simpa using h.symm)
simp [this]
| cons hl tl ih =>
cases l₂ with
| nil => simp at h
| cons _ _ =>
simp only [length_cons, Nat.succ.injEq] at h
simp [ih h]Informal description
For any function $f : \alpha \to \beta \to \gamma$ and lists $l_1, l_1'$ of type $\alpha$ and $l_2, l_2'$ of type $\beta$ such that $\text{length}(l_1) = \text{length}(l_2)$, the following equality holds:
\[
\text{zipWith}\ f\ (l_1 \mathbin{+\!\!+} l_1')\ (l_2 \mathbin{+\!\!+} l_2') = \text{zipWith}\ f\ l_1\ l_2 \mathbin{+\!\!+} \text{zipWith}\ f\ l_1'\ l_2'
\]
where $\mathbin{+\!\!+}$ denotes list concatenation.
List.zipWith_eq_cons_iff
theorem
{f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = g :: l ↔ ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂'
Full source
theorem zipWith_eq_cons_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWithzipWith f l₁ l₂ = g :: l ↔
∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂' := by
match l₁, l₂ with
| [], [] => simp
| [], b :: l₂ => simp
| a :: l₁, [] => simp
| a' :: l₁, b' :: l₂ =>
simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]
constructor
· rintro ⟨⟨rfl, rfl⟩, rfl⟩
refine ⟨a', l₁, b', l₂, by simp⟩
· rintro ⟨a, l₁, b, l₂, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl, rfl⟩
simpInformal description
For any function $f : \alpha \to \beta \to \gamma$ and lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the zipped list $\text{zipWith}\ f\ l_1\ l_2$ equals a cons list $g :: l$ if and only if there exist elements $a \in \alpha$, $b \in \beta$ and sublists $l_1'$ of $l_1$, $l_2'$ of $l_2$ such that:
1. $l_1 = a :: l_1'$
2. $l_2 = b :: l_2'$
3. $g = f\ a\ b$
4. $l = \text{zipWith}\ f\ l_1'\ l_2'$
List.zipWith_eq_append_iff
theorem
{f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = l₁' ++ l₂' ↔
∃ ws xs ys zs, ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = zipWith f ws ys ∧ l₂' = zipWith f xs zs
Full source
theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWithzipWith f l₁ l₂ = l₁' ++ l₂' ↔
∃ ws xs ys zs, ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = zipWith f ws ys ∧ l₂' = zipWith f xs zs := by
induction l₁ generalizing l₂ l₁' with
| nil =>
simp
constructor
· rintro ⟨rfl, rfl⟩
exact ⟨[], [], [], by simp⟩
· rintro ⟨_, _, _, -, ⟨rfl, rfl⟩, _, rfl, rfl, rfl⟩
simp
| cons x₁ l₁ ih₁ =>
cases l₂ with
| nil =>
constructor
· simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp]
rintro rfl rfl
exact ⟨[], x₁ :: l₁, [], by simp⟩
· rintro ⟨_, _, _, _, h₁, _, h₃, rfl, rfl⟩
simp only [nil_eq, append_eq_nil_iff] at h₃
obtain ⟨rfl, rfl⟩ := h₃
simp
| cons x₂ l₂ =>
simp only [zipWith_cons_cons]
rw [cons_eq_append_iff]
constructor
· rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
· exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩
· rw [ih₁] at h
obtain ⟨ws, xs, ys, zs, h, rfl, rfl, h', rfl⟩ := h
refine ⟨x₁ :: ws, xs, x₂ :: ys, zs, by simp [h, h']⟩
· rintro ⟨_, _, _, _, h₁, h₂, h₃, rfl, rfl⟩
rw [cons_eq_append_iff] at h₂
rw [cons_eq_append_iff] at h₃
obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₂
· simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
or_false]
obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₃
· simp
· simp_all
· obtain (⟨rfl, rfl⟩ | ⟨_, rfl, rfl⟩) := h₃
· simp_all
· simp_all [zipWith_append, Nat.succ_inj']Informal description
For any function $f : \alpha \to \beta \to \gamma$ and lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the following equivalence holds:
\[
\text{zipWith}\ f\ l_1\ l_2 = l_1' \mathbin{+\!\!+} l_2' \leftrightarrow \exists ws\ xs\ ys\ zs, \text{length}(ws) = \text{length}(ys) \land l_1 = ws \mathbin{+\!\!+} xs \land l_2 = ys \mathbin{+\!\!+} zs \land l_1' = \text{zipWith}\ f\ ws\ ys \land l_2' = \text{zipWith}\ f\ xs\ zs
\]
where $\mathbin{+\!\!+}$ denotes list concatenation.
List.zipWith_replicate'
theorem
{a : α} {b : β} {n : Nat} : zipWith f (replicate n a) (replicate n b) = replicate n (f a b)
Full source
/-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
@[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]Informal description
For any elements $a \in \alpha$, $b \in \beta$, and natural number $n$, the `zipWith` operation applied to function $f$ and two lists each consisting of $n$ copies of $a$ and $b$ respectively, yields a list of $n$ copies of $f(a,b)$. That is:
\[ \text{zipWith } f (\text{replicate } n\ a) (\text{replicate } n\ b) = \text{replicate } n (f\ a\ b) \]
List.map_uncurry_zip_eq_zipWith
theorem
{f : α → β → γ} {l : List α} {l' : List β} : map (Function.uncurry f) (l.zip l') = zipWith f l l'
Full source
theorem map_uncurry_zip_eq_zipWith {f : α → β → γ} {l : List α} {l' : List β} :
map (Function.uncurry f) (l.zip l') = zipWith f l l' := by
rw [zip]
induction l generalizing l' with
| nil => simp
| cons hl tl ih =>
cases l' <;> simp [ih]Informal description
For any function $f : \alpha \to \beta \to \gamma$ and lists $l$ of type $\text{List } \alpha$ and $l'$ of type $\text{List } \beta$, the map of the uncurried function $f$ over the zip of $l$ and $l'$ is equal to the zip of $l$ and $l'$ with $f$ applied pairwise. In other words:
\[ \text{map } (\text{Function.uncurry } f) (l \text{ zip } l') = \text{zipWith } f\ l\ l' \]
List.map_zip_eq_zipWith
theorem
{f : α × β → γ} {l : List α} {l' : List β} : map f (l.zip l') = zipWith (Function.curry f) l l'
Informal description
For any function $f : \alpha \times \beta \to \gamma$ and lists $l : \text{List } \alpha$, $l' : \text{List } \beta$, the map of $f$ over the zip of $l$ and $l'$ is equal to the zipWith of the curried version of $f$ applied to $l$ and $l'$. That is,
$$\text{map } f (l \text{ zip } l') = \text{zipWith } (\text{curry } f) l l'$$
List.zip_eq_zipWith
theorem
: ∀ {l₁ : List α} {l₂ : List β}, zip l₁ l₂ = zipWith Prod.mk l₁ l₂
Informal description
For any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the zip operation on $l_1$ and $l_2$ is equal to the zipWith operation applied to the pair constructor $\text{Prod.mk}$ and the lists $l_1$ and $l_2$. In other words, $\text{zip}(l_1, l_2) = \text{zipWith}(\text{Prod.mk}, l_1, l_2)$.
List.zip_map
theorem
{f : α → γ} {g : β → δ} : ∀ {l₁ : List α} {l₂ : List β}, zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
Informal description
For any functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, and any lists $l_1 : \text{List } \alpha$ and $l_2 : \text{List } \beta$, the zip of the mapped lists $l_1.\text{map } f$ and $l_2.\text{map } g$ is equal to the mapped zip of the original lists, where the mapping is applied component-wise to each pair in the zipped list. That is,
\[
\text{zip } (l_1.\text{map } f) (l_2.\text{map } g) = (\text{zip } l_1 l_2).\text{map } (f \times g)
\]
where $(f \times g)(a, b) = (f(a), g(b))$.
List.zip_map_left
theorem
{f : α → γ} {l₁ : List α} {l₂ : List β} : zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id)
Informal description
For any function $f : \alpha \to \gamma$ and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the zip of the mapped list $l_1.\text{map } f$ with $l_2$ is equal to the mapped zip of $l_1$ and $l_2$, where the mapping applies $f$ to the first component and leaves the second component unchanged. That is,
\[
\text{zip } (l_1.\text{map } f) l_2 = (\text{zip } l_1 l_2).\text{map } (f \times \text{id})
\]
where $(f \times \text{id})(a, b) = (f(a), b)$.
List.zip_map_right
theorem
{f : β → γ} {l₁ : List α} {l₂ : List β} : zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f)
Informal description
For any function $f : \beta \to \gamma$ and any lists $l_1 : \text{List } \alpha$ and $l_2 : \text{List } \beta$, the zip of $l_1$ with the mapped list $l_2.\text{map } f$ is equal to the mapped zip of $l_1$ and $l_2$, where the mapping applies the identity function to the first component and $f$ to the second component of each pair. That is,
\[
\text{zip } l_1 (l_2.\text{map } f) = (\text{zip } l_1 l_2).\text{map } (\text{id} \times f)
\]
where $(\text{id} \times f)(a, b) = (a, f(b))$.
List.tail_zip
theorem
{l₁ : List α} {l₂ : List β} : (zip l₁ l₂).tail = zip l₁.tail l₂.tail
Informal description
For any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the tail of the list obtained by zipping $l_1$ and $l_2$ is equal to the list obtained by zipping the tails of $l_1$ and $l_2$. That is, $(\text{zip } l_1 l_2).\text{tail} = \text{zip } (l_1.\text{tail}) (l_2.\text{tail})$.
List.zip_append
theorem
: ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂), zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
Full source
theorem zip_append :
∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
| [], _, _, _, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
| _, _, [], _, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
| _ :: _, _, _ :: _, _, h => by
simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]Informal description
For any lists $l_1, r_1$ of type $\alpha$ and $l_2, r_2$ of type $\beta$, if the lengths of $l_1$ and $l_2$ are equal, then the zip of the concatenated lists $l_1 \mathbin{+\!\!+} r_1$ and $l_2 \mathbin{+\!\!+} r_2$ is equal to the concatenation of the zips of $l_1$ with $l_2$ and $r_1$ with $r_2$. That is,
\[
\text{zip } (l_1 \mathbin{+\!\!+} r_1) (l_2 \mathbin{+\!\!+} r_2) = \text{zip } l_1 l_2 \mathbin{+\!\!+} \text{zip } r_1 r_2.
\]
List.zip_map'
theorem
{f : α → β} {g : α → γ} : ∀ {l : List α}, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
Informal description
For any list $l$ of elements of type $\alpha$ and any functions $f : \alpha \to \beta$ and $g : \alpha \to \gamma$, the zip of the mapped lists $f \circ l$ and $g \circ l$ is equal to the list obtained by mapping each element $a \in l$ to the pair $(f(a), g(a))$. That is,
$$\text{zip } (l \map f) (l \map g) = l \map \lambda a, (f(a), g(a)).$$
List.of_mem_zip
theorem
{a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
Full source
theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b)(a, b) ∈ zip l₁ l₂ → a ∈ l₁a ∈ l₁ ∧ b ∈ l₂
| _ :: l₁, _ :: l₂, h => by
cases h
case head => simp
case tail h =>
· have := of_mem_zip h
exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩Informal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, if a pair $(a, b)$ is an element of the zipped list $\text{zip } l_1 l_2$, then $a$ is an element of $l_1$ and $b$ is an element of $l_2$.
List.map_fst_zip
theorem
: ∀ {l₁ : List α} {l₂ : List β}, l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
Full source
theorem map_fst_zip :
∀ {l₁ : List α} {l₂ : List β}, l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
| [], _, _ => rfl
| _ :: as, _ :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.fst (zip as bs) = _ :: as
rw [map_fst_zip (l₁ := as) h]
| _ :: _, [], h => by simp at hInformal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, if the length of $l_1$ is less than or equal to the length of $l_2$, then mapping the first projection function over the zipped list $\text{zip}(l_1, l_2)$ yields $l_1$ itself. In other words,
$$\text{map}\ \pi_1\ (\text{zip}\ l_1\ l_2) = l_1.$$
List.map_snd_zip
theorem
: ∀ {l₁ : List α} {l₂ : List β}, l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
Full source
theorem map_snd_zip :
∀ {l₁ : List α} {l₂ : List β}, l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
| _, [], _ => by
rw [zip_nil_right]
rfl
| [], b :: bs, h => by simp at h
| a :: as, b :: bs, h => by
simp [Nat.succ_le_succ_iff] at h
show _ :: map Prod.snd (zip as bs) = _ :: bs
rw [map_snd_zip (l₂ := bs) h]Informal description
For any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, if the length of $l_2$ is less than or equal to the length of $l_1$, then mapping the second projection function over the zipped list $\text{zip}\ l_1\ l_2$ yields $l_2$. In other words, $\text{map}\ \text{snd}\ (\text{zip}\ l_1\ l_2) = l_2$.
List.map_prod_left_eq_zip
theorem
{l : List α} {f : α → β} : (l.map fun x => (x, f x)) = l.zip (l.map f)
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \beta$, the list obtained by mapping each element $x \in l$ to the pair $(x, f(x))$ is equal to the zip of $l$ with the list obtained by mapping $f$ over $l$. That is,
$$\text{map}\ (\lambda x, (x, f(x)))\ l = \text{zip}\ l\ (\text{map}\ f\ l).$$
List.map_prod_right_eq_zip
theorem
{l : List α} {f : α → β} : (l.map fun x => (f x, x)) = (l.map f).zip l
Informal description
For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \beta$, the list obtained by mapping each element $x \in l$ to the pair $(f(x), x)$ is equal to the zip of the list $l \map f$ with $l$ itself. That is,
$$l \map \lambda x, (f(x), x) = (l \map f) \zip l.$$
List.zip_eq_nil_iff
theorem
{l₁ : List α} {l₂ : List β} : zip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = []
Full source
@[simp] theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
zipzip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = [] := by
simp [zip_eq_zipWith]Informal description
For any two lists $l_1$ (of type $\alpha$) and $l_2$ (of type $\beta$), the zip operation on $l_1$ and $l_2$ results in an empty list if and only if either $l_1$ is empty or $l_2$ is empty. In other words, $\text{zip}(l_1, l_2) = [] \leftrightarrow l_1 = [] \lor l_2 = []$.
List.zip_eq_cons_iff
theorem
{l₁ : List α} {l₂ : List β} : zip l₁ l₂ = (a, b) :: l ↔ ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂'
Full source
theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
zipzip l₁ l₂ = (a, b) :: l ↔
∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂' := by
simp only [zip_eq_zipWith, zipWith_eq_cons_iff]
constructor
· rintro ⟨a, l₁, b, l₂, rfl, rfl, h, rfl, rfl⟩
simp only [Prod.mk.injEq] at h
obtain ⟨rfl, rfl⟩ := h
simp
· rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
refine ⟨a, l₁', b, l₂', by simp⟩Informal description
For any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, the zip operation on $l_1$ and $l_2$ results in a list with head $(a, b)$ and tail $l$ if and only if there exist lists $l_1'$ and $l_2'$ such that $l_1 = a :: l_1'$, $l_2 = b :: l_2'$, and $l = \text{zip}(l_1', l_2')$.
List.zip_eq_append_iff
theorem
{l₁ : List α} {l₂ : List β} :
zip l₁ l₂ = l₁' ++ l₂' ↔
∃ ws xs ys zs, ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = zip ws ys ∧ l₂' = zip xs zs
Full source
theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
zipzip l₁ l₂ = l₁' ++ l₂' ↔
∃ ws xs ys zs, ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = zip ws ys ∧ l₂' = zip xs zs := by
simp [zip_eq_zipWith, zipWith_eq_append_iff]Informal description
For any two lists $l_1$ (of type $\alpha$) and $l₂$ (of type $\beta$), the zip operation $\text{zip}(l₁, l₂)$ equals the concatenation of two lists $l₁'$ and $l₂'$ if and only if there exist sublists $ws$, $xs$, $ys$, $zs$ such that:
1. The lengths of $ws$ and $ys$ are equal,
2. $l₁ = ws ++ xs$,
3. $l₂ = ys ++ zs$,
4. $l₁' = \text{zip}(ws, ys)$,
5. $l₂' = \text{zip}(xs, zs)$.
In other words, $\text{zip}(l₁, l₂) = l₁' ++ l₂' \leftrightarrow \exists ws\ xs\ ys\ zs, \text{length}(ws) = \text{length}(ys) \land l₁ = ws ++ xs \land l₂ = ys ++ zs \land l₁' = \text{zip}(ws, ys) \land l₂' = \text{zip}(xs, zs)$.
List.zip_replicate'
theorem
{a : α} {b : β} {n : Nat} : zip (replicate n a) (replicate n b) = replicate n (a, b)
Full source
/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
zip (replicate n a) (replicate n b) = replicate n (a, b) := by
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]Informal description
For any elements $a$ of type $\alpha$ and $b$ of type $\beta$, and any natural number $n$, the zip of the list containing $n$ copies of $a$ with the list containing $n$ copies of $b$ is equal to the list containing $n$ copies of the pair $(a, b)$. In other words, $\text{zip}(\text{replicate}(n, a), \text{replicate}(n, b)) = \text{replicate}(n, (a, b))$.
List.getElem?_zipWithAll
theorem
{f : Option α → Option β → γ} {i : Nat} :
(zipWithAll f as bs)[i]? =
match as[i]?, bs[i]? with
| none, none => .none
| a?, b? => some (f a? b?)
Full source
theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
(zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
| none, none => .none | a?, b? => some (f a? b?) := by
induction as generalizing bs i with
| nil => induction bs generalizing i with
| nil => simp
| cons b bs bih => cases i <;> simp_all
| cons a as aih => cases bs with
| nil =>
specialize @aih []
cases i <;> simp_all
| cons b bs => cases i <;> simp_allInformal description
For any function $f : \text{Option}\,\alpha \to \text{Option}\,\beta \to \gamma$, natural number index $i$, and lists $as$ and $bs$ of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, the optional indexing operation on the list $\text{zipWithAll}\,f\,as\,bs$ at position $i$ satisfies:
\[
(\text{zipWithAll}\,f\,as\,bs)[i]? =
\begin{cases}
\text{none} & \text{if } as[i]? = \text{none} \text{ and } bs[i]? = \text{none}, \\
\text{some}\,(f\,a\,b) & \text{otherwise, where } a = as[i]? \text{ and } b = bs[i]?.
\end{cases}
\]
List.head?_zipWithAll
theorem
{f : Option α → Option β → γ} :
(zipWithAll f as bs).head? =
match as.head?, bs.head? with
| none, none => .none
| a?, b? => some (f a? b?)
Full source
theorem head?_zipWithAll {f : Option α → Option β → γ} :
(zipWithAll f as bs).head? = match as.head?, bs.head? with
| none, none => .none | a?, b? => some (f a? b?) := by
simp [head?_eq_getElem?, getElem?_zipWithAll]Informal description
For any function $f : \text{Option}\,\alpha \to \text{Option}\,\beta \to \gamma$ and lists $as$ and $bs$ of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, the optional head of the list $\text{zipWithAll}\,f\,as\,bs$ satisfies:
\[
(\text{zipWithAll}\,f\,as\,bs).\text{head}? =
\begin{cases}
\text{none} & \text{if } as.\text{head}? = \text{none} \text{ and } bs.\text{head}? = \text{none}, \\
\text{some}\,(f\,a\,b) & \text{otherwise, where } a = as.\text{head}? \text{ and } b = bs.\text{head}?.
\end{cases}
\]
List.head_zipWithAll
theorem
{f : Option α → Option β → γ} (h) : (zipWithAll f as bs).head h = f as.head? bs.head?
Full source
@[simp] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
(zipWithAll f as bs).head h = f as.head? bs.head? := by
apply Option.some.inj
rw [← head?_eq_head, head?_zipWithAll]
split <;> simp_allInformal description
For any function $f : \text{Option}\,\alpha \to \text{Option}\,\beta \to \gamma$ and lists $as$ and $bs$ of types $\text{List}\,\alpha$ and $\text{List}\,\beta$ respectively, if the list $\text{zipWithAll}\,f\,as\,bs$ is nonempty (with proof $h$), then its head satisfies:
\[
(\text{zipWithAll}\,f\,as\,bs).\text{head} = f\,(as.\text{head}?)\,(bs.\text{head}?).
\]
List.tail_zipWithAll
theorem
{f : Option α → Option β → γ} : (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail
Full source
@[simp] theorem tail_zipWithAll {f : Option α → Option β → γ} :
(zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by
cases as <;> cases bs <;> simpInformal description
For any function $f : \text{Option } \alpha \to \text{Option } \beta \to \gamma$ and lists `as` and `bs`, the tail of the list obtained by applying `zipWithAll f as bs` is equal to the list obtained by applying `zipWithAll f` to the tails of `as` and `bs`. That is,
$$(\text{zipWithAll } f \text{ as bs}).\text{tail} = \text{zipWithAll } f \text{ as.tail bs.tail}.$$
List.zipWithAll_map
theorem
{μ} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂
Full source
theorem zipWithAll_map {μ} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_allInformal description
For any types $\alpha, \beta, \gamma, \delta, \mu$, functions $g : \alpha \to \gamma$, $h : \beta \to \delta$, and $f : \text{Option } \gamma \to \text{Option } \delta \to \mu$, and lists $l_1 : \text{List } \alpha$, $l_2 : \text{List } \beta$, the following equality holds:
$$\text{zipWithAll } f \text{ } (l_1.\text{map } g) \text{ } (l_2.\text{map } h) = \text{zipWithAll } (\lambda a b, f (g <$> a) (h <$> b)) \text{ } l_1 \text{ } l_2.$$
Here, $\text{zipWithAll}$ combines two lists element-wise using $f$, extending them with $\text{none}$ if they have different lengths, and $<$ denotes the functorial action of $\text{Option}$.
List.zipWithAll_map_left
theorem
{l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} :
zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂
Full source
theorem zipWithAll_map_left {l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} :
zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_allInformal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, any function $f : \alpha \to \alpha'$, and any function $g : \text{Option } \alpha' \to \text{Option } \beta \to \gamma$, the following equality holds:
$$\text{zipWithAll } g \text{ } (l_1.\text{map } f) \text{ } l_2 = \text{zipWithAll } (\lambda a b, g (f <$> a) b) \text{ } l_1 \text{ } l_2.$$
Here, $\text{zipWithAll}$ combines two lists element-wise using the function $g$, padding with $\text{none}$ when one list is longer than the other, and $f <$ denotes the functorial action of $\text{Option}$ applied to $f$.
List.zipWithAll_map_right
theorem
{l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} :
zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂
Full source
theorem zipWithAll_map_right {l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} :
zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_allInformal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, any function $f : \beta \to \beta'$, and any function $g : \text{Option } \alpha \to \text{Option } \beta' \to \gamma$, the following equality holds:
\[
\text{zipWithAll}\ g\ l_1\ (l_2.\text{map}\ f) = \text{zipWithAll}\ (\lambda a\ b,\ g\ a\ (f <$> b))\ l_1\ l_2
\]
Here, $\text{zipWithAll}$ combines two lists element-wise using $g$, and $f <$>$ b$ applies $f$ to the value inside the optional $b$ if it exists.
List.map_zipWithAll
theorem
{δ : Type _} {f : α → β} {g : Option γ → Option δ → α} {l : List γ} {l' : List δ} :
map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l'
Full source
theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option δ → α} {l : List γ} {l' : List δ} :
map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by
induction l generalizing l' with
| nil => simp
| cons hd tl hl =>
cases l' <;> simp_allInformal description
For any types $\alpha$, $\beta$, $\gamma$, and $\delta$, and any functions $f : \alpha \to \beta$ and $g : \text{Option } \gamma \to \text{Option } \delta \to \alpha$, and any lists $l : \text{List } \gamma$ and $l' : \text{List } \delta$, the following equality holds:
\[
\text{map } f (\text{zipWithAll } g\ l\ l') = \text{zipWithAll } (\lambda x\ y, f (g\ x\ y))\ l\ l'
\]
Here, $\text{zipWithAll}$ combines two lists by applying a function $g$ to pairs of elements (or `none` if one list is shorter), and $\text{map}$ applies a function $f$ to each element of a list.
List.zipWithAll_replicate
theorem
{a : α} {b : β} {n : Nat} : zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b)
Full source
@[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
induction n with
| zero => rfl
| succ n ih => simp [replicate_succ, ih]Informal description
For any elements $a \in \alpha$ and $b \in \beta$, and any natural number $n$, the `zipWithAll` operation applied to two lists each consisting of $n$ copies of $a$ and $b$ respectively, using a function $f : \alpha \to \beta \to \gamma$, results in a list of $n$ copies of $f(a, b)$.
In symbols:
\[
\text{zipWithAll } f (\text{replicate } n\ a) (\text{replicate } n\ b) = \text{replicate } n (f\ a\ b)
\]
List.unzip_fst
theorem
: (unzip l).fst = l.map Prod.fst
Informal description
For any list $l$ of ordered pairs $(a, b) \in \alpha \times \beta$, the first component of the unzipped list $\text{unzip}(l)$ is equal to the list obtained by mapping the first projection function $\text{Prod.fst}$ over $l$. In other words, if $\text{unzip}(l) = (L_1, L_2)$, then $L_1 = \text{map} (\lambda (a, b). a) l$.
List.unzip_snd
theorem
: (unzip l).snd = l.map Prod.snd
Informal description
For any list $l$ of ordered pairs $(a, b) \in \alpha \times \beta$, the second component of the unzipped list $\text{unzip}(l)$ is equal to the list obtained by mapping the second projection function $\text{Prod.snd}$ over $l$. In other words, if $\text{unzip}(l) = (L_1, L_2)$, then $L_2 = \text{map} (\lambda (a, b). b) l$.
List.unzip_eq_map
theorem
: ∀ {l : List (α × β)}, unzip l = (l.map Prod.fst, l.map Prod.snd)
Full source
theorem unzip_eq_map : ∀ {l : List (α × β)}, unzip l = (l.map Prod.fst, l.map Prod.snd)
| [] => rfl
| (a, b)(a, b) :: l => by simp only [unzip_cons, map_cons, unzip_eq_map (l := l)]Informal description
For any list $l$ of ordered pairs $(a, b) \in \alpha \times \beta$, the unzipped list $\text{unzip}(l)$ is equal to the pair of lists obtained by mapping the first projection function over $l$ and the second projection function over $l$, i.e., $\text{unzip}(l) = (\text{map} \ \text{fst} \ l, \text{map} \ \text{snd} \ l)$.
List.zip_unzip
theorem
: ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l
Full source
theorem zip_unzip : ∀ l : List (α × β), zip (unzip l).1 (unzip l).2 = l
| [] => rfl
| (a, b)(a, b) :: l => by simp only [unzip_cons, zip_cons_cons, zip_unzip l]Informal description
For any list $l$ of ordered pairs of type $\alpha \times \beta$, the zip of the first components and second components obtained from unzipping $l$ equals $l$ itself. In other words, if $(xs, ys) = \text{unzip}(l)$, then $\text{zip}(xs, ys) = l$.
List.unzip_zip_left
theorem
: ∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁
Full source
theorem unzip_zip_left :
∀ {l₁ : List α} {l₂ : List β}, length l₁ ≤ length l₂ → (unzip (zip l₁ l₂)).1 = l₁
| [], _, _ => rfl
| _, [], h => by rw [eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero h)]; rfl
| _ :: _, _ :: _, h => by
simp only [zip_cons_cons, unzip_cons, unzip_zip_left (le_of_succ_le_succ h)]Informal description
For any two lists $l₁$ of type $\alpha$ and $l₂$ of type $\beta$, if the length of $l₁$ is less than or equal to the length of $l₂$, then the first component of the unzipped result of zipping $l₁$ and $l₂$ equals $l₁$.
List.unzip_zip_right
theorem
: ∀ {l₁ : List α} {l₂ : List β}, length l₂ ≤ length l₁ → (unzip (zip l₁ l₂)).2 = l₂
Full source
theorem unzip_zip_right :
∀ {l₁ : List α} {l₂ : List β}, length l₂ ≤ length l₁ → (unzip (zip l₁ l₂)).2 = l₂
| [], l₂, _ => by simp_all
| l₁, [], _ => by simp
| a :: l₁, b :: l₂, h => by
simp only [zip_cons_cons, unzip_cons, unzip_zip_right (le_of_succ_le_succ h)]Informal description
For any lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$, if the length of $l_2$ is less than or equal to the length of $l_1$, then the second component of the unzipped result of $\text{zip}(l_1, l_2)$ equals $l_2$.
List.unzip_zip
theorem
{l₁ : List α} {l₂ : List β} (h : length l₁ = length l₂) : unzip (zip l₁ l₂) = (l₁, l₂)
Full source
theorem unzip_zip {l₁ : List α} {l₂ : List β} (h : length l₁ = length l₂) :
unzip (zip l₁ l₂) = (l₁, l₂) := by
ext
· rw [unzip_zip_left (Nat.le_of_eq h)]
· rw [unzip_zip_right (Nat.le_of_eq h.symm)]Informal description
For any two lists $l_1$ of type $\alpha$ and $l_2$ of type $\beta$ with equal lengths, the unzipping of their zipped pair equals the original pair of lists, i.e., $\text{unzip}(\text{zip}(l_1, l_2)) = (l_1, l_2)$.
List.zip_of_prod
theorem
{l : List α} {l' : List β} {xs : List (α × β)} (hl : xs.map Prod.fst = l) (hr : xs.map Prod.snd = l') : xs = l.zip l'
Informal description
For any lists $l$ of type $\alpha$, $l'$ of type $\beta$, and $xs$ of type $\alpha \times \beta$, if the list obtained by mapping the first projection over $xs$ equals $l$ and the list obtained by mapping the second projection over $xs$ equals $l'$, then $xs$ is equal to the zip of $l$ and $l'$.
List.tail_zip_fst
theorem
{l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1
Informal description
For any list $l$ of ordered pairs $(a, b) \in \alpha \times \beta$, the tail of the first component of the unzipped list $\text{unzip}(l)$ is equal to the first component of the unzipped tail of $l$. In other words, if $\text{unzip}(l) = (L_1, L_2)$, then $\text{tail}(L_1) = \text{unzip}(\text{tail}(l)).1$.
List.tail_zip_snd
theorem
{l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2
Informal description
For any list $l$ of ordered pairs $(a, b) \in \alpha \times \beta$, the tail of the second component of the unzipped list $\text{unzip}(l)$ is equal to the second component of the unzipped tail of $l$. In other words, if $\text{unzip}(l) = (L_1, L_2)$, then $\text{tail}(L_2) = \text{unzip}(\text{tail}(l)).2$.
List.unzip_replicate
theorem
{n : Nat} {a : α} {b : β} : unzip (replicate n (a, b)) = (replicate n a, replicate n b)
Full source
@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
ext1 <;> simpInformal description
For any natural number $n$ and any elements $a \in \alpha$, $b \in \beta$, the unzipping of a list consisting of $n$ copies of the pair $(a, b)$ is equal to the pair of lists where each list consists of $n$ copies of $a$ and $n$ copies of $b$ respectively. That is,
$$\text{unzip}(\text{replicate}(n, (a, b))) = (\text{replicate}(n, a), \text{replicate}(n, b))$$