data.list.zip

# zip & unzip #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides results about list.zip_with, list.zip and list.unzip (definitions are in core Lean). zip_with 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, zip_with f [0, 1, 2] [6.28, 31] = [f 0 6.28, f 1 31]. zip is zip_with 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_with_cons_cons {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
(a :: l₁) (b :: l₂) = f a b :: l₁ l₂
@[simp]
theorem list.zip_cons_cons {α : Type u} {β : Type u_1} (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
(a :: l₁).zip (b :: l₂) = (a, b) :: l₁.zip l₂
@[simp]
theorem list.zip_with_nil_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list β) :
@[simp]
theorem list.zip_with_nil_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) :
@[simp]
theorem list.zip_with_eq_nil_iff {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α β γ} {l : list α} {l' : list β} :
@[simp]
theorem list.zip_nil_left {α : Type u} {β : Type u_1} (l : list α) :
@[simp]
theorem list.zip_nil_right {α : Type u} {β : Type u_1} (l : list α) :
@[simp]
theorem list.zip_swap {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
(l₁.zip l₂) = l₂.zip l₁
@[simp]
theorem list.length_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l₁ : list α) (l₂ : list β) :
l₁ l₂).length = l₂.length
@[simp]
theorem list.length_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
(l₁.zip l₂).length = l₂.length
theorem list.all₂_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α β γ} {p : γ Prop} {l₁ : list α} {l₂ : list β} (h : l₁.length = l₂.length) :
l₁ l₂) list.forall₂ (λ (x : α) (y : β), p (f x y)) l₁ l₂
theorem list.lt_length_left_of_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α β γ} {i : } {l : list α} {l' : list β} (h : i < l l').length) :
i < l.length
theorem list.lt_length_right_of_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α β γ} {i : } {l : list α} {l' : list β} (h : i < 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.zip_append {α : Type u} {β : Type u_1} {l₁ r₁ : list α} {l₂ r₂ : list β} (h : l₁.length = l₂.length) :
(l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
theorem list.zip_map {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α γ) (g : β δ) (l₁ : list α) (l₂ : list β) :
(list.map f l₁).zip (list.map g l₂) = list.map (prod.map f g) (l₁.zip l₂)
theorem list.zip_map_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α γ) (l₁ : list α) (l₂ : list β) :
(list.map f l₁).zip l₂ = list.map (prod.map f id) (l₁.zip l₂)
theorem list.zip_map_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : β γ) (l₁ : list α) (l₂ : list β) :
l₁.zip (list.map f l₂) = list.map f) (l₁.zip l₂)
@[simp]
theorem list.zip_with_map {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {μ : Type u_4} (f : γ δ μ) (g : α γ) (h : β δ) (as : list α) (bs : list β) :
(list.map g as) (list.map h bs) = list.zip_with (λ (a : α) (b : β), f (g a) (h b)) as bs
theorem list.zip_with_map_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α β γ) (g : δ α) (l : list δ) (l' : list β) :
(list.map g l) l' = list.zip_with (f g) l l'
theorem list.zip_with_map_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α β γ) (l : list α) (g : δ β) (l' : list δ) :
(list.map g l') = list.zip_with (λ (x : α), f x g) l l'
theorem list.zip_map' {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β) (g : α γ) (l : list α) :
(list.map f l).zip (list.map g l) = list.map (λ (a : α), (f a, g a)) l
theorem list.map_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α β) (g : γ δ α) (l : list γ) (l' : list δ) :
l l') = list.zip_with (λ (x : γ) (y : δ), f (g x y)) l l'
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.map_fst_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
l₁.length l₂.length (l₁.zip l₂) = l₁
theorem list.map_snd_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
l₂.length l₁.length (l₁.zip l₂) = l₂
@[simp]
theorem list.unzip_nil {α : Type u} {β : Type u_1} :
@[simp]
theorem list.unzip_cons {α : Type u} {β : Type u_1} (a : α) (b : β) (l : list × β)) :
((a, b) :: l).unzip = (a :: l.unzip.fst, b :: l.unzip.snd)
theorem list.unzip_eq_map {α : Type u} {β : Type u_1} (l : list × β)) :
l.unzip = ,
theorem list.unzip_left {α : Type u} {β : Type u_1} (l : list × β)) :
theorem list.unzip_right {α : Type u} {β : Type u_1} (l : list × β)) :
theorem list.unzip_swap {α : Type u} {β : Type u_1} (l : list × β)) :
theorem list.zip_unzip {α : Type u} {β : Type u_1} (l : list × β)) :
theorem list.unzip_zip_left {α : Type u} {β : Type u_1} {l₁ : list α} {l₂ : list β} :
l₁.length l₂.length (l₁.zip l₂).unzip.fst = l₁
theorem list.unzip_zip_right {α : Type u} {β : Type u_1} {l₁ : list α} {l₂ : list β} (h : l₂.length l₁.length) :
(l₁.zip l₂).unzip.snd = 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 : = l) (hr : = l') :
lp = l.zip l'
theorem list.map_prod_left_eq_zip {α : Type u} {β : Type u_1} {l : list α} (f : α β) :
list.map (λ (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 (λ (x : α), (f x, x)) l = (list.map f l).zip l
theorem list.zip_with_comm {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (la : list α) (lb : list β) :
la lb = list.zip_with (λ (b : β) (a : α), f a b) lb la
theorem list.zip_with_congr {α : Type u} {β : Type u_1} {γ : Type u_2} (f g : α β γ) (la : list α) (lb : list β) (h : list.forall₂ (λ (a : α) (b : β), f a b = g a b) la lb) :
la lb = la lb
theorem list.zip_with_comm_of_comm {α : Type u} {β : Type u_1} (f : α α β) (comm : (x y : α), f x y = f y x) (l l' : list α) :
l' = l' l
@[simp]
theorem list.zip_with_same {α : Type u} {δ : Type u_3} (f : α α δ) (l : list α) :
l = list.map (λ (a : α), f a a) l
theorem list.zip_with_zip_with_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : δ γ ε) (g : α β δ) (la : list α) (lb : list β) (lc : list γ) :
la lb) lc = list.zip_with3 (λ (a : α) (b : β) (c : γ), f (g a b) c) la lb lc
theorem list.zip_with_zip_with_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : α δ ε) (g : β γ δ) (la : list α) (lb : list β) (lc : list γ) :
la lb lc) = list.zip_with3 (λ (a : α) (b : β) (c : γ), f a (g b c)) la lb lc
@[simp]
theorem list.zip_with3_same_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α α β γ) (la : list α) (lb : list β) :
la la lb = list.zip_with (λ (a : α) (b : β), f a a b) la lb
@[simp]
theorem list.zip_with3_same_mid {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β α γ) (la : list α) (lb : list β) :
la lb la = list.zip_with (λ (a : α) (b : β), f a b a) la lb
@[simp]
theorem list.zip_with3_same_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β β γ) (la : list α) (lb : list β) :
la lb lb = list.zip_with (λ (a : α) (b : β), f a b b) la lb
@[protected, instance]
def list.zip_with.is_symm_op {α : Type u} {β : Type u_1} (f : α α β) [ β f] :
is_symm_op (list α) (list β)
@[simp]
theorem list.length_revzip {α : Type u} (l : list α) :
@[simp]
theorem list.unzip_revzip {α : Type u} (l : list α) :
@[simp]
theorem list.revzip_map_fst {α : Type u} (l : list α) :
@[simp]
theorem list.revzip_map_snd {α : Type u} (l : list α) :
theorem list.reverse_revzip {α : Type u} (l : list α) :
theorem list.revzip_swap {α : Type u} (l : list α) :
theorem list.nth_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l₁ : list α) (l₂ : list β) (i : ) :
l₁ l₂).nth i = (l₁.nth i)).bind (λ (g : β γ), (l₂.nth i))
theorem list.nth_zip_with_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β γ) (l₁ : list α) (l₂ : list β) (z : γ) (i : ) :
l₁ l₂).nth i = (x : α) (y : β), l₁.nth i = l₂.nth i = f x y = z
theorem list.nth_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) (z : α × β) (i : ) :
(l₁.zip l₂).nth i = l₁.nth i = l₂.nth i =
@[simp]
theorem list.nth_le_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α β γ} {l : list α} {l' : list β} {i : } {h : i < l l').length} :
l l').nth_le i h = f (l.nth_le i _) (l'.nth_le i _)
@[simp]
theorem list.nth_le_zip {α : Type u} {β : Type u_1} {l : list α} {l' : list β} {i : } {h : i < (l.zip l').length} :
(l.zip l').nth_le i h = (l.nth_le i _, l'.nth_le i _)
theorem list.mem_zip_inits_tails {α : Type u} {l init tail : list α} :
(init, tail) l.inits.zip l.tails init ++ tail = l
theorem list.map_uncurry_zip_eq_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) (l' : list β) :
(l.zip l') = l'
@[simp]
theorem list.sum_zip_with_distrib_left {α : Type u} {β : Type u_1} {γ : Type u_2} [semiring γ] (f : α β γ) (n : γ) (l : list α) (l' : list β) :
(list.zip_with (λ (x : α) (y : β), n * f x y) l l').sum = n * l l').sum

### Operations that can be applied before or after a zip_with#

theorem list.zip_with_distrib_take {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) (l' : list β) (n : ) :
l l') = l) l')
theorem list.zip_with_distrib_drop {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) (l' : list β) (n : ) :
l l') = l) l')
theorem list.zip_with_distrib_tail {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) (l' : list β) :
l l').tail = l'.tail
theorem list.zip_with_append {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l la : list α) (l' lb : list β) (h : l.length = l'.length) :
(l ++ la) (l' ++ lb) = l' ++ la lb
theorem list.zip_with_distrib_reverse {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α β γ) (l : list α) (l' : list β) (h : l.length = l'.length) :
l l').reverse = l'.reverse
theorem list.sum_add_sum_eq_sum_zip_with_add_sum_drop {α : Type u} (L L' : list α) :
L.sum + L'.sum = L').sum + (list.drop L'.length L).sum + L').sum
theorem list.prod_mul_prod_eq_prod_zip_with_of_length_eq {α : Type u} [comm_monoid α] (L L' : list α) (h : L.length = L'.length) :
L.prod * L'.prod = L').prod
theorem list.sum_add_sum_eq_sum_zip_with_of_length_eq {α : Type u} (L L' : list α) (h : L.length = L'.length) :
L.sum + L'.sum = L').sum