scilib documentation

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₂]).

source
@[simp]
theorem list.zip_with_cons_cons {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (a : α) (b : β) (l₁ : list α) (l₂ : list β) :
list.zip_with f (a :: l₁) (b :: l₂) = f a b :: list.zip_with f l₁ l₂
source
@[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₂
source
@[simp]
theorem list.zip_with_nil_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list β) :
list.zip_with f list.nil l = list.nil
source
@[simp]
theorem list.zip_with_nil_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) :
list.zip_with f l list.nil = list.nil
source
@[simp]
theorem list.zip_with_eq_nil_iff {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : list α} {l' : list β} :
list.zip_with f l l' = list.nil ↔ l = list.nil ∨ l' = list.nil
source
@[simp]
theorem list.zip_nil_left {α : Type u} {β : Type u_1} (l : list α) :
list.nil.zip l = list.nil
source
@[simp]
theorem list.zip_nil_right {α : Type u} {β : Type u_1} (l : list α) :
l.zip list.nil = list.nil
source
@[simp]
theorem list.zip_swap {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
list.map prod.swap (l₁.zip l₂) = l₂.zip l₁
source
@[simp]
theorem list.length_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l₁ : list α) (l₂ : list β) :
(list.zip_with f l₁ l₂).length = linear_order.min l₁.length l₂.length
source
@[simp]
theorem list.length_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
(l₁.zip l₂).length = linear_order.min l₁.length l₂.length
source
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) :
list.all₂ p (list.zip_with f l₁ l₂) ↔ list.forall₂ (λ (x : α) (y : β), p (f x y)) l₁ l₂
source
theorem list.lt_length_left_of_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : list α} {l' : list β} (h : i < (list.zip_with f l l').length) :
i < l.length
source
theorem list.lt_length_right_of_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : list α} {l' : list β} (h : i < (list.zip_with f l l').length) :
i < l'.length
source
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
source
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
source
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₂
source
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₂)
source
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₂)
source
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 (prod.map id f) (l₁.zip l₂)
source
@[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.zip_with f (list.map g as) (list.map h bs) = list.zip_with (λ (a : α) (b : β), f (g a) (h b)) as bs
source
theorem list.zip_with_map_left {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α → β → γ) (g : δ → α) (l : list δ) (l' : list β) :
list.zip_with f (list.map g l) l' = list.zip_with (f ∘ g) l l'
source
theorem list.zip_with_map_right {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α → β → γ) (l : list α) (g : δ → β) (l' : list δ) :
list.zip_with f l (list.map g l') = list.zip_with (λ (x : α), f x ∘ g) l l'
source
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
source
theorem list.map_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} (f : α → β) (g : γ → δ → α) (l : list γ) (l' : list δ) :
list.map f (list.zip_with g l l') = list.zip_with (λ (x : γ) (y : δ), f (g x y)) l l'
source
theorem list.mem_zip {α : Type u} {β : Type u_1} {a : α} {b : β} {l₁ : list α} {l₂ : list β} :
(a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂
source
theorem list.map_fst_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
l₁.length ≤ l₂.length → list.map prod.fst (l₁.zip l₂) = l₁
source
theorem list.map_snd_zip {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) :
l₂.length ≤ l₁.length → list.map prod.snd (l₁.zip l₂) = l₂
source
@[simp]
theorem list.unzip_nil {α : Type u} {β : Type u_1} :
list.nil.unzip = (list.nil α, list.nil β)
source
@[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)
source
theorem list.unzip_eq_map {α : Type u} {β : Type u_1} (l : list (α × β)) :
l.unzip = (list.map prod.fst l, list.map prod.snd l)
source
theorem list.unzip_left {α : Type u} {β : Type u_1} (l : list (α × β)) :
l.unzip.fst = list.map prod.fst l
source
theorem list.unzip_right {α : Type u} {β : Type u_1} (l : list (α × β)) :
l.unzip.snd = list.map prod.snd l
source
theorem list.unzip_swap {α : Type u} {β : Type u_1} (l : list (α × β)) :
(list.map prod.swap l).unzip = l.unzip.swap
source
theorem list.zip_unzip {α : Type u} {β : Type u_1} (l : list (α × β)) :
l.unzip.fst.zip l.unzip.snd = l
source
theorem list.unzip_zip_left {α : Type u} {β : Type u_1} {l₁ : list α} {l₂ : list β} :
l₁.length ≤ l₂.length → (l₁.zip l₂).unzip.fst = l₁
source
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₂
source
theorem list.unzip_zip {α : Type u} {β : Type u_1} {l₁ : list α} {l₂ : list β} (h : l₁.length = l₂.length) :
(l₁.zip l₂).unzip = (l₁, l₂)
source
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'
source
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)
source
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
source
theorem list.zip_with_comm {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (la : list α) (lb : list β) :
list.zip_with f la lb = list.zip_with (λ (b : β) (a : α), f a b) lb la
source
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) :
list.zip_with f la lb = list.zip_with g la lb
source
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 α) :
list.zip_with f l l' = list.zip_with f l' l
source
@[simp]
theorem list.zip_with_same {α : Type u} {δ : Type u_3} (f : α → α → δ) (l : list α) :
list.zip_with f l l = list.map (λ (a : α), f a a) l
source
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 γ) :
list.zip_with f (list.zip_with g la lb) lc = list.zip_with3 (λ (a : α) (b : β) (c : γ), f (g a b) c) la lb lc
source
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 γ) :
list.zip_with f la (list.zip_with g lb lc) = list.zip_with3 (λ (a : α) (b : β) (c : γ), f a (g b c)) la lb lc
source
@[simp]
theorem list.zip_with3_same_left {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → α → β → γ) (la : list α) (lb : list β) :
list.zip_with3 f la la lb = list.zip_with (λ (a : α) (b : β), f a a b) la lb
source
@[simp]
theorem list.zip_with3_same_mid {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → α → γ) (la : list α) (lb : list β) :
list.zip_with3 f la lb la = list.zip_with (λ (a : α) (b : β), f a b a) la lb
source
@[simp]
theorem list.zip_with3_same_right {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → β → γ) (la : list α) (lb : list β) :
list.zip_with3 f la lb lb = list.zip_with (λ (a : α) (b : β), f a b b) la lb
source
@[protected, instance]
def list.zip_with.is_symm_op {α : Type u} {β : Type u_1} (f : α → α → β) [is_symm_op α β f] :
is_symm_op (list α) (list β) (list.zip_with f)
source
@[simp]
theorem list.length_revzip {α : Type u} (l : list α) :
l.revzip.length = l.length
source
@[simp]
theorem list.unzip_revzip {α : Type u} (l : list α) :
l.revzip.unzip = (l, l.reverse)
source
@[simp]
theorem list.revzip_map_fst {α : Type u} (l : list α) :
list.map prod.fst l.revzip = l
source
@[simp]
theorem list.revzip_map_snd {α : Type u} (l : list α) :
list.map prod.snd l.revzip = l.reverse
source
theorem list.reverse_revzip {α : Type u} (l : list α) :
l.revzip.reverse = l.reverse.revzip
source
theorem list.revzip_swap {α : Type u} (l : list α) :
list.map prod.swap l.revzip = l.reverse.revzip
source
theorem list.nth_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (i : ℕ) :
(list.zip_with f l₁ l₂).nth i = (option.map f (l₁.nth i)).bind (λ (g : β → γ), option.map g (l₂.nth i))
source
theorem list.nth_zip_with_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (z : γ) (i : ℕ) :
(list.zip_with f l₁ l₂).nth i = option.some z ↔ ∃ (x : α) (y : β), l₁.nth i = option.some x ∧ l₂.nth i = option.some y ∧ f x y = z
source
theorem list.nth_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : list α) (l₂ : list β) (z : α × β) (i : ℕ) :
(l₁.zip l₂).nth i = option.some z ↔ l₁.nth i = option.some z.fst ∧ l₂.nth i = option.some z.snd
source
@[simp]
theorem list.nth_le_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : list α} {l' : list β} {i : ℕ} {h : i < (list.zip_with f l l').length} :
(list.zip_with f l l').nth_le i h = f (l.nth_le i _) (l'.nth_le i _)
source
@[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 _)
source
theorem list.mem_zip_inits_tails {α : Type u} {l init tail : list α} :
(init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
source
theorem list.map_uncurry_zip_eq_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) (l' : list β) :
list.map (function.uncurry f) (l.zip l') = list.zip_with f l l'
source
@[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 * (list.zip_with f l l').sum

Operations that can be applied before or after a zip_with #

source
theorem list.zip_with_distrib_take {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) (l' : list β) (n : ℕ) :
list.take n (list.zip_with f l l') = list.zip_with f (list.take n l) (list.take n l')
source
theorem list.zip_with_distrib_drop {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) (l' : list β) (n : ℕ) :
list.drop n (list.zip_with f l l') = list.zip_with f (list.drop n l) (list.drop n l')
source
theorem list.zip_with_distrib_tail {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) (l' : list β) :
(list.zip_with f l l').tail = list.zip_with f l.tail l'.tail
source
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) :
list.zip_with f (l ++ la) (l' ++ lb) = list.zip_with f l l' ++ list.zip_with f la lb
source
theorem list.zip_with_distrib_reverse {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : list α) (l' : list β) (h : l.length = l'.length) :
(list.zip_with f l l').reverse = list.zip_with f l.reverse l'.reverse
source
theorem list.sum_add_sum_eq_sum_zip_with_add_sum_drop {α : Type u} [add_comm_monoid α] (L L' : list α) :
L.sum + L'.sum = (list.zip_with has_add.add L L').sum + (list.drop L'.length L).sum + (list.drop L.length L').sum
source
theorem list.prod_mul_prod_eq_prod_zip_with_mul_prod_drop {α : Type u} [comm_monoid α] (L L' : list α) :
L.prod * L'.prod = (list.zip_with has_mul.mul L L').prod * (list.drop L'.length L).prod * (list.drop L.length L').prod
source
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 = (list.zip_with has_mul.mul L L').prod
source
theorem list.sum_add_sum_eq_sum_zip_with_of_length_eq {α : Type u} [add_comm_monoid α] (L L' : list α) (h : L.length = L'.length) :
L.sum + L'.sum = (list.zip_with has_add.add L L').sum