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 : α → β → γ) (la : Array α) (lb : Array β) : zipWith f la lb = zipWith (fun (b : β) (a : α) => f a b) lb la

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

@[simp]

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

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 : α → β → γ} {l₁ : Array α} {l₂ : Array β} {z : γ} {i : Nat} : (zipWith f l₁ l₂)[i]? = some z ↔ ∃ (x : α), ∃ (y : β), l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

theorem Array.getElem?_zip_eq_some {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} {z : α × β} {i : Nat} : (l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.fst ∧ l₂[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 : β → δ) (l₁ : Array α) (l₂ : Array β) : zipWith f (map g l₁) (map h l₂) = zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂

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

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

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

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

@[simp]

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

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

theorem Array.take_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : Array α✝} {l' : Array α✝¹} {n : Nat} : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

theorem Array.extract_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : Array α✝} {l' : Array α✝¹} {m n : Nat} : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n)

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

theorem Array.zipWith_eq_append_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁' l₂' : Array γ} {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} : zipWith f l₁ l₂ = l₁' ++ l₂' ↔ ∃ (w : Array α), ∃ (x : Array α), ∃ (y : Array β), ∃ (z : Array β), w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

@[simp]

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

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

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

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

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

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

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

zip

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

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

@[simp]

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

theorem Array.zip_eq_zipWith {α : Type u_1} {β : Type u_2} (l₁ : Array α) (l₂ : Array β) : l₁.zip l₂ = zipWith Prod.mk l₁ l₂

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

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

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

theorem Array.zip_append {α : Type u_1} {β : Type u_2} {l₁ r₁ : Array α} {l₂ r₂ : Array β} (_h : l₁.size = l₂.size) : (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

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

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

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

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

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

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

@[simp]

theorem Array.zip_eq_empty_iff {α : Type u_1} {β : Type u_2} {l₁ : Array α} {l₂ : Array β} : l₁.zip l₂ = #[] ↔ l₁ = #[] ∨ l₂ = #[]

theorem Array.zip_eq_append_iff {α : Type u_1} {β : Type u_2} {l₁' l₂' : Array (α × β)} {l₁ : Array α} {l₂ : Array β} : l₁.zip l₂ = l₁' ++ l₂' ↔ ∃ (w : Array α), ∃ (x : Array α), ∃ (y : Array β), ∃ (z : Array β), w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = w.zip y ∧ l₂' = x.zip z

@[simp]

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

theorem Array.zip_eq_zip_take_min {α : Type u_1} {β : Type u_2} (l₁ : Array α) (l₂ : Array β) : l₁.zip l₂ = (l₁.take (min l₁.size l₂.size)).zip (l₂.take (min l₁.size l₂.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 : β → δ) (l₁ : Array α) (l₂ : Array β) : zipWithAll f (map g l₁) (map h l₂) = zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) l₁ l₂

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

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

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

@[simp]

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

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} (l : Array (α × β)) : l.unzip = (map Prod.fst l, map Prod.snd l)

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

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

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

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

theorem Array.zip_of_prod {α : Type u_1} {β : Type u_2} {l : Array α} {l' : Array β} {lp : Array (α × β)} (hl : map Prod.fst lp = l) (hr : map Prod.snd lp = l') : lp = l.zip l'

@[simp]

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