# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`. #

## Zippers #

### zipWith #

source
theorem List.zipWith_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : List α} {bs : List β} :
zipWith f as bs = zipWith (fun (b : β) (a : α) => f a b) bs as
source
theorem List.zipWith_comm_of_comm {α : Type u_1} {β : Type u_2} {f : α → α → β} (comm : ∀ (x y : α), f x y = f y x) {l l' : List α} :
zipWith f l l' = zipWith f l' l
source
@[simp]
theorem List.zipWith_self {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {l : List α} :
zipWith f l l = map (fun (a : α) => f a a) l
source
theorem List.getElem?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} {i : Nat} :
(zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | x, x_1 => none

See also `getElem?_zipWith'` for a variant using `Option.map` and `Option.bind` rather than a `match`.

source
theorem List.getElem?_zipWith' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : Nat} :
(zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun (g : β → γ) => Option.map g l₂[i]?

Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`.

source
theorem List.getElem?_zipWith_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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
source
theorem List.getElem?_zip_eq_some {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} :
(l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.fst ∧ l₂[i]? = some z.snd
source
theorem List.head?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} :
(zipWith f as bs).head? = match as.head?, bs.head? with | some a, some b => some (f a b) | x, x_1 => none
source
theorem List.head_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} (h : zipWith f as bs ≠ []) :
(zipWith f as bs).head h = f (as.head ⋯) (bs.head ⋯)
source
@[simp]
theorem List.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
zipWith f (map g l₁) (map h l₂) = zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂
source
theorem List.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → α'} {g : α' → β → γ} :
zipWith g (map f l₁) l₂ = zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂
source
theorem List.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : β → β'} {g : α → β' → γ} :
zipWith g l₁ (map f l₂) = zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂
source
theorem List.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : δ} {g : γ → δ → δ} :
foldr g i (zipWith f l₁ l₂) = foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (l₁.zip l₂)
source
theorem List.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : δ} {g : δ → γ → δ} :
foldl g i (zipWith f l₁ l₂) = foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (l₁.zip l₂)
source
@[simp]
theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} :
zipWith f l l' = [] ↔ l = [] ∨ l' = []
source
@[simp]
theorem List.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {l : List γ} {l' : List δ} :
map f (zipWith g l l') = zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'
source
theorem List.take_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} {i : Nat} :
take i (zipWith f l l') = zipWith f (take i l) (take i l')
source
theorem List.drop_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} {i : Nat} :
drop i (zipWith f l l') = zipWith f (drop i l) (drop i l')
source
@[simp]
theorem List.tail_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} :
(zipWith f l l').tail = zipWith f l.tail l'.tail
source
theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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₂'
source
theorem List.zipWith_eq_cons_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {l : List γ} {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = g :: l ↔ ∃ (a : α), ∃ (l₁' : List α), ∃ (b : β), ∃ (l₂' : List β), l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂'
source
theorem List.zipWith_eq_append_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁' l₂' : List γ} {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
zipWith f l₁ l₂ = l₁' ++ l₂' ↔ ∃ (ws : List α), ∃ (xs : List α), ∃ (ys : List β), ∃ (zs : List β), ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = zipWith f ws ys ∧ l₂' = zipWith f xs zs
source
@[simp]
theorem List.zipWith_replicate' {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {a : α} {b : β} {n : Nat} :
zipWith f (replicate n a) (replicate n b) = replicate n (f a b)

See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths.

source
theorem List.map_uncurry_zip_eq_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β} :
map (Function.uncurry f) (l.zip l') = zipWith f l l'
source
theorem List.map_zip_eq_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {l : List α} {l' : List β} :
map f (l.zip l') = zipWith (Function.curry f) l l'

### zip #

source
theorem List.zip_eq_zipWith {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₁.zip l₂ = zipWith Prod.mk l₁ l₂
source
theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {l₁ : List α} {l₂ : List β} :
(map f l₁).zip (map g l₂) = map (Prod.map f g) (l₁.zip l₂)
source
theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {l₁ : List α} {l₂ : List β} :
(map f l₁).zip l₂ = map (Prod.map f id) (l₁.zip l₂)
source
theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {l₁ : List α} {l₂ : List β} :
l₁.zip (map f l₂) = map (Prod.map id f) (l₁.zip l₂)
source
@[simp]
theorem List.tail_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
(l₁.zip l₂).tail = l₁.tail.zip l₂.tail
source
theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : l₁.length = l₂.length) :
(l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
source
theorem List.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {l : List α} :
(map f l).zip (map g l) = map (fun (a : α) => (f a, g a)) l
source
theorem List.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂
source
theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₁.length ≤ l₂.length → map Prod.fst (l₁.zip l₂) = l₁
source
theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₂.length ≤ l₁.length → map Prod.snd (l₁.zip l₂) = l₂
source
theorem List.map_prod_left_eq_zip {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} :
map (fun (x : α) => (x, f x)) l = l.zip (map f l)
source
theorem List.map_prod_right_eq_zip {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} :
map (fun (x : α) => (f x, x)) l = (map f l).zip l
source
@[simp]
theorem List.zip_eq_nil_iff {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₁.zip l₂ = [] ↔ l₁ = [] ∨ l₂ = []
source
theorem List.zip_eq_cons_iff {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l : List (α × β)} {l₁ : List α} {l₂ : List β} :
l₁.zip l₂ = (a, b) :: l ↔ ∃ (l₁' : List α), ∃ (l₂' : List β), l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = l₁'.zip l₂'
source
theorem List.zip_eq_append_iff {α : Type u_1} {β : Type u_2} {l₁' l₂' : List (α × β)} {l₁ : List α} {l₂ : List β} :
l₁.zip l₂ = l₁' ++ l₂' ↔ ∃ (ws : List α), ∃ (xs : List α), ∃ (ys : List β), ∃ (zs : List β), ws.length = ys.length ∧ l₁ = ws ++ xs ∧ l₂ = ys ++ zs ∧ l₁' = ws.zip ys ∧ l₂' = xs.zip zs
source
@[simp]
theorem List.zip_replicate' {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} :
(replicate n a).zip (replicate n b) = replicate n (a, b)

See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths.

### zipWithAll #

source
theorem List.getElem?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {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?)
source
theorem List.head?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} :
(zipWithAll f as bs).head? = match as.head?, bs.head? with | none, none => none | a?, b? => some (f a? b?)
source
@[simp]
theorem List.head_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} (h : zipWithAll f as bs ≠ []) :
(zipWithAll f as bs).head h = f as.head? bs.head?
source
@[simp]
theorem List.tail_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} :
(zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail
source
theorem List.zipWithAll_map {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
zipWithAll f (map g l₁) (map h l₂) = zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) l₁ l₂
source
theorem List.zipWithAll_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → α'} {g : Option α' → Option β → γ} :
zipWithAll g (map f l₁) l₂ = zipWithAll (fun (a : Option α) (b : Option β) => g (f <$> a) b) l₁ l₂
source
theorem List.zipWithAll_map_right {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : β → β'} {g : Option α → Option β' → γ} :
zipWithAll g l₁ (map f l₂) = zipWithAll (fun (a : Option α) (b : Option β) => g a (f <$> b)) l₁ l₂
source
theorem List.map_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {l : List γ} {l' : List δ} :
map f (zipWithAll g l l') = zipWithAll (fun (x : Option γ) (y : Option δ) => f (g x y)) l l'
source
@[simp]
theorem List.zipWithAll_replicate {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : Option α → Option β → α✝} {a : α} {b : β} {n : Nat} :
zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b))

### unzip #

source
@[simp]
theorem List.unzip_fst {α✝ : Type u_1} {β✝ : Type u_2} {l : List (α✝ × β✝)} :
l.unzip.fst = map Prod.fst l
source
@[simp]
theorem List.unzip_snd {α✝ : Type u_1} {β✝ : Type u_2} {l : List (α✝ × β✝)} :
l.unzip.snd = map Prod.snd l
source
theorem List.unzip_eq_map {α : Type u_1} {β : Type u_2} {l : List (α × β)} :
l.unzip = (map Prod.fst l, map Prod.snd l)
source
theorem List.zip_unzip {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
l.unzip.fst.zip l.unzip.snd = l
source
theorem List.unzip_zip_left {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₁.length ≤ l₂.length → (l₁.zip l₂).unzip.fst = l₁
source
theorem List.unzip_zip_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
l₂.length ≤ l₁.length → (l₁.zip l₂).unzip.snd = l₂
source
theorem List.unzip_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} (h : l₁.length = l₂.length) :
(l₁.zip l₂).unzip = (l₁, l₂)
source
theorem List.zip_of_prod {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {xs : List (α × β)} (hl : map Prod.fst xs = l) (hr : map Prod.snd xs = l') :
xs = l.zip l'
source
theorem List.tail_zip_fst {α : Type u_1} {β : Type u_2} {l : List (α × β)} :
l.unzip.fst.tail = l.tail.unzip.fst
source
theorem List.tail_zip_snd {α : Type u_1} {β : Type u_2} {l : List (α × β)} :
l.unzip.snd.tail = l.tail.unzip.snd
source
@[simp]
theorem List.unzip_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {b : β} :
(replicate n (a, b)).unzip = (replicate n a, replicate n b)