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 β) :
list.zip_with f (a :: l₁) (b :: l₂) = f a b :: list.zip_with f l₁ l₂
@[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
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'
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
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
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
@[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
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
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
@[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
@[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
@[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
@[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)
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))
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'
Operations that can be applied before or after a zip_with #
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
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
theorem
list.sum_add_sum_eq_sum_zip_with_add_sum_drop
{α : Type u}
[add_comm_monoid α]
(L L' : list α) :
theorem
list.prod_mul_prod_eq_prod_zip_with_mul_prod_drop
{α : Type u}
[comm_monoid α]
(L L' : list α) :
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
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