Lemmas about List.zip
, List.zipWith
, List.zipWithAll
, and List.unzip
. #
Zippers #
zipWith #
theorem
List.zipWith_comm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(la : List α)
(lb : List β)
:
List.zipWith f la lb = List.zipWith (fun (b : β) (a : α) => f a b) lb la
theorem
List.zipWith_comm_of_comm
{α : Type u_1}
{β : Type u_2}
(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_1}
{δ : Type u_2}
(f : α → α → δ)
(l : List α)
:
List.zipWith f l l = List.map (fun (a : α) => f a a) l
theorem
List.getElem?_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{f : α → β → γ}
{i : Nat}
:
(List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with
| some a, some b => some (f a b)
| x, x_1 => none
See also getElem?_zipWith'
for a variant
using Option.map
and Option.bind
rather than a match
.
theorem
List.getElem?_zipWith'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{l₁ : List α}
{l₂ : List β}
{f : α → β → γ}
{i : Nat}
:
(List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun (g : β → γ) => Option.map g l₂[i]?
Variant of getElem?_zipWith
using Option.map
and Option.bind
rather than a match
.
@[reducible, inline, deprecated List.getElem?_zipWith]
abbrev
List.zipWith_get?
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{i : Nat}
{f : α → β → γ}
:
(List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
| some a, some b => some (f a b)
| x, x_1 => none
Equations
Instances For
theorem
List.head_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{f : α → β → γ}
(h : List.zipWith f as bs ≠ [])
:
(List.zipWith f as bs).head h = f (as.head ⋯) (bs.head ⋯)
@[simp]
theorem
List.zipWith_map
{γ : Type u_1}
{δ : Type u_2}
{α : Type u_3}
{β : Type u_4}
{μ : Type u_5}
(f : γ → δ → μ)
(g : α → γ)
(h : β → δ)
(l₁ : List α)
(l₂ : List β)
:
List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂
theorem
List.zipWith_map_left
{α : Type u_1}
{β : Type u_2}
{α' : Type u_3}
{γ : Type u_4}
(l₁ : List α)
(l₂ : List β)
(f : α → α')
(g : α' → β → γ)
:
List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂
theorem
List.zipWith_map_right
{α : Type u_1}
{β : Type u_2}
{β' : Type u_3}
{γ : Type u_4}
(l₁ : List α)
(l₂ : List β)
(f : β → β')
(g : α → β' → γ)
:
List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂
theorem
List.zipWith_foldr_eq_zip_foldr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{l₁ : List α}
{l₂ : List β}
{g : γ → δ → δ}
{f : α → β → γ}
(i : δ)
:
List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (l₁.zip l₂)
theorem
List.zipWith_foldl_eq_zip_foldl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{l₁ : List α}
{l₂ : List β}
{g : δ → γ → δ}
{f : α → β → γ}
(i : δ)
:
List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (l₁.zip l₂)
theorem
List.map_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
(f : α → β)
(g : γ → δ → α)
(l : List γ)
(l' : List δ)
:
List.map f (List.zipWith g l l') = List.zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'
@[simp]
theorem
List.tail_zipWith :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1},
(List.zipWith f l l').tail = List.zipWith f l.tail l'.tail
@[reducible, inline, deprecated List.tail_zipWith]
abbrev
List.zipWith_distrib_tail :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1},
(List.zipWith f l l').tail = List.zipWith f l.tail l'.tail
Instances For
theorem
List.zipWith_append
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(l : List α)
(la : List α)
(l' : List β)
(lb : List β)
(h : l.length = l'.length)
:
List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb
@[simp]
theorem
List.zipWith_replicate'
{α : Type u_1}
{β : Type u_2}
:
∀ {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {n : Nat},
List.zipWith f (List.replicate n a) (List.replicate n b) = List.replicate n (f a b)
See also List.zipWith_replicate
in Init.Data.List.TakeDrop
for a generalization with different lengths.
theorem
List.map_uncurry_zip_eq_zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(l : List α)
(l' : List β)
:
List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'
zip #
theorem
List.zip_eq_zipWith
{α : Type u_1}
{β : Type u_2}
(l₁ : List α)
(l₂ : List β)
:
l₁.zip l₂ = List.zipWith Prod.mk l₁ l₂
@[reducible, inline, deprecated List.of_mem_zip]
Equations
Instances For
@[simp]
theorem
List.zip_replicate'
{α : Type u_1}
{β : Type u_2}
{a : α}
{b : β}
{n : Nat}
:
(List.replicate n a).zip (List.replicate n b) = List.replicate n (a, b)
See also List.zip_replicate
in Init.Data.List.TakeDrop
for a generalization with different lengths.
zipWithAll #
@[deprecated List.getElem?_zipWithAll]
@[reducible, inline, deprecated List.getElem?_zipWithAll]
abbrev
List.zipWithAll_get?
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{i : Nat}
{f : Option α → Option β → γ}
:
(List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
| none, none => none
| a?, b? => some (f a? b?)
Equations
Instances For
@[simp]
theorem
List.head_zipWithAll
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{f : Option α → Option β → γ}
(h : List.zipWithAll f as bs ≠ [])
:
(List.zipWithAll f as bs).head h = f as.head? bs.head?
@[simp]
theorem
List.tail_zipWithAll
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{as : List α}
{bs : List β}
{f : Option α → Option β → γ}
:
(List.zipWithAll f as bs).tail = List.zipWithAll f as.tail bs.tail
theorem
List.zipWithAll_map
{γ : Type u_1}
{δ : Type u_2}
{α : Type u_1}
{β : Type u_2}
{μ : Type u_3}
(f : Option γ → Option δ → μ)
(g : α → γ)
(h : β → δ)
(l₁ : List α)
(l₂ : List β)
:
List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) l₁ l₂
@[simp]
theorem
List.zipWithAll_replicate
{α : Type u_1}
{β : Type u_2}
:
∀ {α_1 : Type u_3} {f : Option α → Option β → α_1} {a : α} {b : β} {n : Nat},
List.zipWithAll f (List.replicate n a) (List.replicate n b) = List.replicate n (f (some a) (some b))
unzip #
@[simp]
theorem
List.unzip_replicate
{α : Type u_1}
{β : Type u_2}
{n : Nat}
{a : α}
{b : β}
:
(List.replicate n (a, b)).unzip = (List.replicate n a, List.replicate n b)