Documentation

Mathlib.Data.List.Zip

zip & unzip #

This file provides results about List.zipWith, List.zip and List.unzip (definitions are in core Lean). zipWith f l₁ l₂ applies f : α → β → γ pointwise to a list l₁ : List α and l₂ : List β. It applies, until one of the lists is exhausted. For example, zipWith f [0, 1, 2] [6.28, 31] = [f 0 6.28, f 1 31]. zip is zipWith applied to Prod.mk. For example, zip [a₁, a₂] [b₁, b₂, b₃] = [(a₁, b₁), (a₂, b₂)]. unzip undoes zip. For example, unzip [(a₁, b₁), (a₂, b₂)] = ([a₁, a₂], [b₁, b₂]).

@[simp]
theorem List.zip_swap {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) :
List.map Prod.swap (l₁.zip l₂) = l₂.zip l₁
theorem List.forall_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {p : γProp} {l₁ : List α} {l₂ : List β} :
l₁.length = l₂.length(List.Forall p (List.zipWith f l₁ l₂) List.Forall₂ (fun (x : α) (y : β) => p (f x y)) l₁ l₂)
theorem List.lt_length_left_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {i : } {l : List α} {l' : List β} (h : i < (List.zipWith f l l').length) :
i < l.length
theorem List.lt_length_right_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {i : } {l : List α} {l' : List β} (h : i < (List.zipWith f l l').length) :
i < l'.length
theorem List.lt_length_left_of_zip {α : Type u} {β : Type u_1} {i : } {l : List α} {l' : List β} (h : i < (l.zip l').length) :
i < l.length
theorem List.lt_length_right_of_zip {α : Type u} {β : Type u_1} {i : } {l : List α} {l' : List β} (h : i < (l.zip l').length) :
i < l'.length
theorem List.mem_zip {α : Type u} {β : Type u_1} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
(a, b) l₁.zip l₂a l₁ b l₂
theorem List.unzip_eq_map {α : Type u} {β : Type u_1} (l : List (α × β)) :
l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
theorem List.unzip_left {α : Type u} {β : Type u_1} (l : List (α × β)) :
l.unzip.1 = List.map Prod.fst l
theorem List.unzip_right {α : Type u} {β : Type u_1} (l : List (α × β)) :
l.unzip.2 = List.map Prod.snd l
theorem List.unzip_swap {α : Type u} {β : Type u_1} (l : List (α × β)) :
(List.map Prod.swap l).unzip = l.unzip.swap
theorem List.zip_unzip {α : Type u} {β : Type u_1} (l : List (α × β)) :
l.unzip.1.zip l.unzip.2 = l
theorem List.unzip_zip_left {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} :
l₁.length l₂.length(l₁.zip l₂).unzip.1 = l₁
theorem List.unzip_zip_right {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : l₂.length l₁.length) :
(l₁.zip l₂).unzip.2 = l₂
theorem List.unzip_zip {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : l₁.length = l₂.length) :
(l₁.zip l₂).unzip = (l₁, l₂)
theorem List.zip_of_prod {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {lp : List (α × β)} (hl : List.map Prod.fst lp = l) (hr : List.map Prod.snd lp = l') :
lp = l.zip l'
theorem List.map_prod_left_eq_zip {α : Type u} {β : Type u_1} {l : List α} (f : αβ) :
List.map (fun (x : α) => (x, f x)) l = l.zip (List.map f l)
theorem List.map_prod_right_eq_zip {α : Type u} {β : Type u_1} {l : List α} (f : αβ) :
List.map (fun (x : α) => (f x, x)) l = (List.map f l).zip l
theorem List.zipWith_comm {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (la : List α) (lb : List β) :
List.zipWith f la lb = List.zipWith (fun (b : β) (a : α) => f a b) lb la
theorem List.zipWith_congr {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (g : αβγ) (la : List α) (lb : List β) (h : List.Forall₂ (fun (a : α) (b : β) => f a b = g a b) la lb) :
List.zipWith f la lb = List.zipWith g la lb
theorem List.zipWith_comm_of_comm {α : Type u} {β : Type u_1} (f : ααβ) (comm : ∀ (x y : α), f x y = f y x) (l : List α) (l' : List α) :
@[simp]
theorem List.zipWith_same {α : Type u} {δ : Type u_3} (f : ααδ) (l : List α) :
List.zipWith f l l = List.map (fun (a : α) => f a a) l
theorem List.zipWith_zipWith_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : δγε) (g : αβδ) (la : List α) (lb : List β) (lc : List γ) :
List.zipWith f (List.zipWith g la lb) lc = List.zipWith3 (fun (a : α) (b : β) (c : γ) => f (g a b) c) la lb lc
theorem List.zipWith_zipWith_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : αδε) (g : βγδ) (la : List α) (lb : List β) (lc : List γ) :
List.zipWith f la (List.zipWith g lb lc) = List.zipWith3 (fun (a : α) (b : β) (c : γ) => f a (g b c)) la lb lc
@[simp]
theorem List.zipWith3_same_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : ααβγ) (la : List α) (lb : List β) :
List.zipWith3 f la la lb = List.zipWith (fun (a : α) (b : β) => f a a b) la lb
@[simp]
theorem List.zipWith3_same_mid {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβαγ) (la : List α) (lb : List β) :
List.zipWith3 f la lb la = List.zipWith (fun (a : α) (b : β) => f a b a) la lb
@[simp]
theorem List.zipWith3_same_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αββγ) (la : List α) (lb : List β) :
List.zipWith3 f la lb lb = List.zipWith (fun (a : α) (b : β) => f a b b) la lb
instance List.instIsSymmOpZipWith {α : Type u} {β : Type u_1} (f : ααβ) [IsSymmOp α β f] :
Equations
  • =
@[simp]
theorem List.length_revzip {α : Type u} (l : List α) :
l.revzip.length = l.length
@[simp]
theorem List.unzip_revzip {α : Type u} (l : List α) :
l.revzip.unzip = (l, l.reverse)
@[simp]
theorem List.revzip_map_fst {α : Type u} (l : List α) :
List.map Prod.fst l.revzip = l
@[simp]
theorem List.revzip_map_snd {α : Type u} (l : List α) :
List.map Prod.snd l.revzip = l.reverse
theorem List.reverse_revzip {α : Type u} (l : List α) :
l.revzip.reverse = l.reverse.revzip
theorem List.revzip_swap {α : Type u} (l : List α) :
List.map Prod.swap l.revzip = l.reverse.revzip
theorem List.getElem?_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l₁ : List α) (l₂ : List β) (i : ) :
(List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun (g : βγ) => Option.map g l₂[i]?
theorem List.get?_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l₁ : List α) (l₂ : List β) (i : ) :
(List.zipWith f l₁ l₂).get? i = (Option.map f (l₁.get? i)).bind fun (g : βγ) => Option.map g (l₂.get? i)
theorem List.getElem?_zip_with_eq_some {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l₁ : List α) (l₂ : List β) (z : γ) (i : ) :
(List.zipWith f l₁ l₂)[i]? = some z ∃ (x : α), ∃ (y : β), l₁[i]? = some x l₂[i]? = some y f x y = z
theorem List.get?_zip_with_eq_some {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l₁ : List α) (l₂ : List β) (z : γ) (i : ) :
(List.zipWith f l₁ l₂).get? i = some z ∃ (x : α), ∃ (y : β), l₁.get? i = some x l₂.get? i = some y f x y = z
theorem List.getElem?_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) (z : α × β) (i : ) :
(l₁.zip l₂)[i]? = some z l₁[i]? = some z.1 l₂[i]? = some z.2
theorem List.get?_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) (z : α × β) (i : ) :
(l₁.zip l₂).get? i = some z l₁.get? i = some z.1 l₂.get? i = some z.2
@[simp]
theorem List.getElem_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} {i : } {h : i < (List.zipWith f l l').length} :
(List.zipWith f l l')[i] = f l[i] l'[i]
@[deprecated List.getElem_zipWith]
theorem List.get_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} {i : Fin (List.zipWith f l l').length} :
(List.zipWith f l l').get i = f (l.get i, ) (l'.get i, )
@[simp, deprecated List.get_zipWith]
theorem List.nthLe_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : αβγ} {l : List α} {l' : List β} {i : } {h : i < (List.zipWith f l l').length} :
(List.zipWith f l l').nthLe i h = f (l.nthLe i ) (l'.nthLe i )
@[simp]
theorem List.getElem_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : } {h : i < (l.zip l').length} :
(l.zip l')[i] = (l[i], l'[i])
@[deprecated List.getElem_zip]
theorem List.get_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (l.zip l').length} :
(l.zip l').get i = (l.get i, , l'.get i, )
@[simp, deprecated List.get_zip]
theorem List.nthLe_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : } {h : i < (l.zip l').length} :
(l.zip l').nthLe i h = (l.nthLe i , l'.nthLe i )
theorem List.mem_zip_inits_tails {α : Type u} {l : List α} {init : List α} {tail : List α} :
(init, tail) l.inits.zip l.tails init ++ tail = l
theorem List.map_uncurry_zip_eq_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (l' : List β) :
List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'

Operations that can be applied before or after a zip_with #

theorem List.zipWith_distrib_reverse {α : Type u} {β : Type u_1} {γ : Type u_2} (f : αβγ) (l : List α) (l' : List β) (h : l.length = l'.length) :
(List.zipWith f l l').reverse = List.zipWith f l.reverse l'.reverse