Lemmas about Array.zip, Array.zipWith, Array.zipWithAll, and Array.unzip.

Zippers

zipWith

theorem Array.zipWith_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} : zipWith f as bs = zipWith (fun (b : β) (a : α) => f a b) bs as

theorem Array.zipWith_comm_of_comm {α : Type u_1} {β : Type u_2} {f : α → α → β} (comm : ∀ (x y : α), f x y = f y x) {xs ys : Array α} : zipWith f xs ys = zipWith f ys xs

@[simp]

theorem Array.zipWith_self {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {xs : Array α} : zipWith f xs xs = map (fun (a : α) => f a a) xs

theorem Array.getElem?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : α → β → γ} {i : Nat} : (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 Array.getElem?_zipWith' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : Array α} {l₂ : Array β} {f : α → β → γ} {i : Nat} : (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.

theorem Array.getElem?_zipWith_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} {z : γ} {i : Nat} : (zipWith f as bs)[i]? = some z ↔ ∃ (x : α), ∃ (y : β), as[i]? = some x ∧ bs[i]? = some y ∧ f x y = z

theorem Array.getElem?_zip_eq_some {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {z : α × β} {i : Nat} : (as.zip bs)[i]? = some z ↔ as[i]? = some z.fst ∧ bs[i]? = some z.snd

@[simp]

theorem Array.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} : zipWith f (map g as) (map h bs) = zipWith (fun (a : α) (b : β) => f (g a) (h b)) as bs

theorem Array.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : α → α'} {g : α' → β → γ} : zipWith g (map f as) bs = zipWith (fun (a : α) (b : β) => g (f a) b) as bs

theorem Array.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : β → β'} {g : α → β' → γ} : zipWith g as (map f bs) = zipWith (fun (a : α) (b : β) => g a (f b)) as bs

theorem Array.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {as : Array α} {bs : Array β} {g : γ → δ → δ} {f : α → β → γ} {i : δ} : foldr g i (zipWith f as bs) = foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (as.zip bs)

theorem Array.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {as : Array α} {bs : Array β} {g : δ → γ → δ} {f : α → β → γ} {i : δ} : foldl g i (zipWith f as bs) = foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (as.zip bs)

@[simp]

theorem Array.zipWith_eq_empty_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} : zipWith f as bs = #[] ↔ as = #[] ∨ bs = #[]

theorem Array.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {cs : Array γ} {ds : Array δ} : map f (zipWith g cs ds) = zipWith (fun (x : γ) (y : δ) => f (g x y)) cs ds

theorem Array.take_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {as : Array α✝} {bs : Array α✝¹} {i : Nat} : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i)

theorem Array.extract_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {as : Array α✝} {bs : Array α✝¹} {i j : Nat} : (zipWith f as bs).extract i j = zipWith f (as.extract i j) (bs.extract i j)

theorem Array.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as as' : Array α} {bs bs' : Array β} (h : as.size = bs.size) : zipWith f (as ++ as') (bs ++ bs') = zipWith f as bs ++ zipWith f as' bs'

theorem Array.zipWith_eq_append_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs ys : Array γ} {f : α → β → γ} {as : Array α} {bs : Array β} : zipWith f as bs = xs ++ ys ↔ ∃ (as₁ : Array α), ∃ (as₂ : Array α), ∃ (bs₁ : Array β), ∃ (bs₂ : Array β), as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = zipWith f as₁ bs₁ ∧ ys = zipWith f as₂ bs₂

@[simp]

theorem Array.zipWith_replicate {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {a : α} {b : β} {m n : Nat} : zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b)

@[reducible, inline, deprecated Array.zipWith_replicate (since := "2025-03-18")]

abbrev Array.zipWith_mkArray {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {a : α} {b : β} {m n : Nat} : zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b)

Equations

• @Array.zipWith_mkArray = @Array.zipWith_replicate

theorem Array.map_uncurry_zip_eq_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β} : map (Function.uncurry f) (as.zip bs) = zipWith f as bs

theorem Array.map_zip_eq_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {as : Array α} {bs : Array β} : map f (as.zip bs) = zipWith (Function.curry f) as bs

theorem Array.lt_size_left_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : Nat} {as : Array α} {bs : Array β} (h : i < (zipWith f as bs).size) : i < as.size

theorem Array.lt_size_right_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {i : Nat} {as : Array α} {bs : Array β} (h : i < (zipWith f as bs).size) : i < bs.size

theorem Array.zipWith_eq_zipWith_take_min {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} (as : Array α) (bs : Array β) : zipWith f as bs = zipWith f (as.take (min as.size bs.size)) (bs.take (min as.size bs.size))

theorem Array.reverse_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {as : Array α✝} {bs : Array α✝¹} (h : as.size = bs.size) : (zipWith f as bs).reverse = zipWith f as.reverse bs.reverse

zip

theorem Array.lt_size_left_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {as : Array α} {bs : Array β} (h : i < (as.zip bs).size) : i < as.size

theorem Array.lt_size_right_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {as : Array α} {bs : Array β} (h : i < (as.zip bs).size) : i < bs.size

@[simp]

theorem Array.getElem_zip {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {i : Nat} {h : i < (as.zip bs).size} : (as.zip bs)[i] = (as[i], bs[i])

theorem Array.zip_eq_zipWith {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} : as.zip bs = zipWith Prod.mk as bs

theorem Array.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β} : (map f as).zip (map g bs) = map (Prod.map f g) (as.zip bs)

theorem Array.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {as : Array α} {bs : Array β} : (map f as).zip bs = map (Prod.map f id) (as.zip bs)

theorem Array.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {as : Array α} {bs : Array β} : as.zip (map f bs) = map (Prod.map id f) (as.zip bs)

theorem Array.zip_append {α : Type u_1} {β : Type u_2} {as bs : Array α} {cs ds : Array β} (_h : as.size = cs.size) : (as ++ bs).zip (cs ++ ds) = as.zip cs ++ bs.zip ds

theorem Array.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {xs : Array α} : (map f xs).zip (map g xs) = map (fun (a : α) => (f a, g a)) xs

theorem Array.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {as : Array α} {bs : Array β} : (a, b) ∈ as.zip bs → a ∈ as ∧ b ∈ bs

theorem Array.map_fst_zip {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : as.size ≤ bs.size) : map Prod.fst (as.zip bs) = as

theorem Array.map_snd_zip {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : bs.size ≤ as.size) : map Prod.snd (as.zip bs) = bs

theorem Array.map_prod_left_eq_zip {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : map (fun (x : α) => (x, f x)) xs = xs.zip (map f xs)

theorem Array.map_prod_right_eq_zip {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} : map (fun (x : α) => (f x, x)) xs = (map f xs).zip xs

@[simp]

theorem Array.zip_eq_empty_iff {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} : as.zip bs = #[] ↔ as = #[] ∨ bs = #[]

theorem Array.zip_eq_append_iff {α : Type u_1} {β : Type u_2} {xs ys : Array (α × β)} {as : Array α} {bs : Array β} : as.zip bs = xs ++ ys ↔ ∃ (as₁ : Array α), ∃ (as₂ : Array α), ∃ (bs₁ : Array β), ∃ (bs₂ : Array β), as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = as₁.zip bs₁ ∧ ys = as₂.zip bs₂

@[simp]

theorem Array.zip_replicate {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : Nat} : (replicate m a).zip (replicate n b) = replicate (min m n) (a, b)

@[reducible, inline, deprecated Array.zip_replicate (since := "2025-03-18")]

abbrev Array.zip_mkArray {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : Nat} : (replicate m a).zip (replicate n b) = replicate (min m n) (a, b)

Equations

• @Array.zip_mkArray = @Array.zip_replicate

theorem Array.zip_eq_zip_take_min {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} : as.zip bs = (as.take (min as.size bs.size)).zip (bs.take (min as.size bs.size))

zipWithAll

theorem Array.getElem?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : Option α → Option β → γ} {i : Nat} : (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => none | a?, b? => some (f a? b?)

theorem Array.zipWithAll_map {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ} {h : β → δ} {as : Array α} {bs : Array β} : zipWithAll f (map g as) (map h bs) = zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) as bs

theorem Array.zipWithAll_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {as : Array α} {bs : Array β} {f : α → α'} {g : Option α' → Option β → γ} : zipWithAll g (map f as) bs = zipWithAll (fun (a : Option α) (b : Option β) => g (f <$> a) b) as bs

theorem Array.zipWithAll_map_right {α : Type u_1} {β β' : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : β → β'} {g : Option α → Option β' → γ} : zipWithAll g as (map f bs) = zipWithAll (fun (a : Option α) (b : Option β) => g a (f <$> b)) as bs

theorem Array.map_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : Option γ → Option δ → α} {cs : Array γ} {ds : Array δ} : map f (zipWithAll g cs ds) = zipWithAll (fun (x : Option γ) (y : Option δ) => f (g x y)) cs ds

@[simp]

theorem Array.zipWithAll_replicate {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : Option α → Option β → α✝} {a : α} {b : β} {n : Nat} : zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b))

@[reducible, inline, deprecated Array.zipWithAll_replicate (since := "2025-03-18")]

abbrev Array.zipWithAll_mkArray {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : Option α → Option β → α✝} {a : α} {b : β} {n : Nat} : zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b))

Equations

• @Array.zipWithAll_mkArray = @Array.zipWithAll_replicate

unzip

@[simp]

theorem Array.unzip_fst {α✝ : Type u_1} {β✝ : Type u_2} {l : Array (α✝ × β✝)} : l.unzip.fst = map Prod.fst l

@[simp]

theorem Array.unzip_snd {α✝ : Type u_1} {β✝ : Type u_2} {l : Array (α✝ × β✝)} : l.unzip.snd = map Prod.snd l

theorem Array.unzip_eq_map {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip = (map Prod.fst xs, map Prod.snd xs)

theorem Array.zip_unzip {α : Type u_1} {β : Type u_2} (xs : Array (α × β)) : xs.unzip.fst.zip xs.unzip.snd = xs

theorem Array.unzip_zip_left {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : as.size ≤ bs.size) : (as.zip bs).unzip.fst = as

theorem Array.unzip_zip_right {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : bs.size ≤ as.size) : (as.zip bs).unzip.snd = bs

theorem Array.unzip_zip {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : as.size = bs.size) : (as.zip bs).unzip = (as, bs)

theorem Array.zip_of_prod {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : map Prod.fst xs = as) (hr : map Prod.snd xs = bs) : xs = as.zip bs

@[simp]

theorem Array.unzip_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {b : β} : (replicate n (a, b)).unzip = (replicate n a, replicate n b)

@[reducible, inline, deprecated Array.unzip_replicate (since := "2025-03-18")]

abbrev Array.unzip_mkArray {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {b : β} : (replicate n (a, b)).unzip = (replicate n a, replicate n b)

Equations

• @Array.unzip_mkArray = @Array.unzip_replicate