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₂])
.
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.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 α)
:
List.zipWith f l l' = List.zipWith f l' l
@[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]
:
IsSymmOp (List α) (List β) (List.zipWith f)
Equations
- ⋯ = ⋯
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)
@[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 ⋯)
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