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₂]).

@[simp]

theorem List.zip_swap {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) : List.map Prod.swap (List.zip l₁ l₂) = List.zip l₂ l₁

theorem List.forall_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {p : γ → Prop} {l₁ : List α} {l₂ : List β} : List.length l₁ = List.length l₂ → (List.Forall p (List.zipWith f l₁ l₂) ↔ List.Forall₂ (fun (x : α) (y : β) => p (f x y)) l₁ l₂)

theorem List.lt_length_left_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β} (h : i < List.length (List.zipWith f l l')) : i < List.length l

theorem List.lt_length_right_of_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β} (h : i < List.length (List.zipWith f l l')) : i < List.length l'

theorem List.lt_length_left_of_zip {α : Type u} {β : Type u_1} {i : ℕ} {l : List α} {l' : List β} (h : i < List.length (List.zip l l')) : i < List.length l

theorem List.lt_length_right_of_zip {α : Type u} {β : Type u_1} {i : ℕ} {l : List α} {l' : List β} (h : i < List.length (List.zip l l')) : i < List.length l'

theorem List.mem_zip {α : Type u} {β : Type u_1} {a : α} {b : β} {l₁ : List α} {l₂ : List β} : (a, b) ∈ List.zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂

theorem List.unzip_eq_map {α : Type u} {β : Type u_1} (l : List (α × β)) : List.unzip l = (List.map Prod.fst l, List.map Prod.snd l)

theorem List.unzip_left {α : Type u} {β : Type u_1} (l : List (α × β)) : (List.unzip l).1 = List.map Prod.fst l

theorem List.unzip_right {α : Type u} {β : Type u_1} (l : List (α × β)) : (List.unzip l).2 = List.map Prod.snd l

theorem List.unzip_swap {α : Type u} {β : Type u_1} (l : List (α × β)) : List.unzip (List.map Prod.swap l) = Prod.swap (List.unzip l)

theorem List.zip_unzip {α : Type u} {β : Type u_1} (l : List (α × β)) : List.zip (List.unzip l).1 (List.unzip l).2 = l

theorem List.unzip_zip_left {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} : List.length l₁ ≤ List.length l₂ → (List.unzip (List.zip l₁ l₂)).1 = l₁

theorem List.unzip_zip_right {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : List.length l₂ ≤ List.length l₁) : (List.unzip (List.zip l₁ l₂)).2 = l₂

theorem List.unzip_zip {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β} (h : List.length l₁ = List.length l₂) : List.unzip (List.zip l₁ l₂) = (l₁, l₂)

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

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

theorem List.map_prod_right_eq_zip {α : Type u} {β : Type u_1} {l : List α} (f : α → β) : List.map (fun (x : α) => (f x, x)) l = List.zip (List.map f 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.instIsSymmOpListListZipWith {α : Type u} {β : Type u_1} (f : α → α → β) [IsSymmOp α β f] : IsSymmOp (List α) (List β) (List.zipWith f)

Equations

• (_ : IsSymmOp (List α) (List β) (List.zipWith f)) = (_ : IsSymmOp (List α) (List β) (List.zipWith f))

@[simp]

theorem List.length_revzip {α : Type u} (l : List α) : List.length (List.revzip l) = List.length l

@[simp]

theorem List.unzip_revzip {α : Type u} (l : List α) : List.unzip (List.revzip l) = (l, List.reverse l)

@[simp]

theorem List.revzip_map_fst {α : Type u} (l : List α) : List.map Prod.fst (List.revzip l) = l

@[simp]

theorem List.revzip_map_snd {α : Type u} (l : List α) : List.map Prod.snd (List.revzip l) = List.reverse l

theorem List.reverse_revzip {α : Type u} (l : List α) : List.reverse (List.revzip l) = List.revzip (List.reverse l)

theorem List.revzip_swap {α : Type u} (l : List α) : List.map Prod.swap (List.revzip l) = List.revzip (List.reverse l)

theorem List.get?_zip_with {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l₁ : List α) (l₂ : List β) (i : ℕ) : List.get? (List.zipWith f l₁ l₂) i = Option.bind (Option.map f (List.get? l₁ i)) fun (g : β → γ) => Option.map g (List.get? l₂ i)

theorem List.get?_zip_with_eq_some {α : Type u_5} {β : Type u_6} {γ : Type u_7} (f : α → β → γ) (l₁ : List α) (l₂ : List β) (z : γ) (i : ℕ) : List.get? (List.zipWith f l₁ l₂) i = some z ↔ ∃ (x : α), ∃ (y : β), List.get? l₁ i = some x ∧ List.get? l₂ i = some y ∧ f x y = z

theorem List.get?_zip_eq_some {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β) (z : α × β) (i : ℕ) : List.get? (List.zip l₁ l₂) i = some z ↔ List.get? l₁ i = some z.1 ∧ List.get? l₂ i = some z.2

@[simp]

theorem List.get_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : List α} {l' : List β} {i : Fin (List.length (List.zipWith f l l'))} : List.get (List.zipWith f l l') i = f (List.get l { val := ↑i, isLt := (_ : ↑i < List.length l) }) (List.get l' { val := ↑i, isLt := (_ : ↑i < List.length l') })

@[simp]

theorem List.nthLe_zipWith {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : List α} {l' : List β} {i : ℕ} {h : i < List.length (List.zipWith f l l')} : List.nthLe (List.zipWith f l l') i h = f (List.nthLe l i (_ : i < List.length l)) (List.nthLe l' i (_ : i < List.length l'))

@[simp]

theorem List.get_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (List.length (List.zip l l'))} : List.get (List.zip l l') i = (List.get l { val := ↑i, isLt := (_ : ↑i < List.length l) }, List.get l' { val := ↑i, isLt := (_ : ↑i < List.length l') })

@[simp]

theorem List.nthLe_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : ℕ} {h : i < List.length (List.zip l l')} : List.nthLe (List.zip l l') i h = (List.nthLe l i (_ : i < List.length l), List.nthLe l' i (_ : i < List.length l'))

theorem List.mem_zip_inits_tails {α : Type u} {l : List α} {init : List α} {tail : List α} : (init, tail) ∈ List.zip (List.inits l) (List.tails l) ↔ init ++ tail = l

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) (List.zip l l') = List.zipWith f l l'

@[simp]

theorem List.sum_zipWith_distrib_left {α : Type u} {β : Type u_1} {γ : Type u_5} [Semiring γ] (f : α → β → γ) (n : γ) (l : List α) (l' : List β) : List.sum (List.zipWith (fun (x : α) (y : β) => n * f x y) l l') = n * List.sum (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 : List.length l = List.length l') : List.reverse (List.zipWith f l l') = List.zipWith f (List.reverse l) (List.reverse l')

theorem List.sum_add_sum_eq_sum_zipWith_add_sum_drop {α : Type u} [AddCommMonoid α] (L : List α) (L' : List α) : List.sum L + List.sum L' = List.sum (List.zipWith (fun (x x_1 : α) => x + x_1) L L') + List.sum (List.drop (List.length L') L) + List.sum (List.drop (List.length L) L')

abbrev List.sum_add_sum_eq_sum_zipWith_add_sum_drop.match_1 {α : Type u_1} (motive : List α → List α → Prop) : ∀ (x x_1 : List α), (∀ (ys : List α), motive [] ys) → (∀ (xs : List α), motive xs []) → (∀ (x : α) (xs : List α) (y : α) (ys : List α), motive (x :: xs) (y :: ys)) → motive x x_1

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

theorem List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop {α : Type u} [CommMonoid α] (L : List α) (L' : List α) : List.prod L * List.prod L' = List.prod (List.zipWith (fun (x x_1 : α) => x * x_1) L L') * List.prod (List.drop (List.length L') L) * List.prod (List.drop (List.length L) L')

theorem List.sum_add_sum_eq_sum_zipWith_of_length_eq {α : Type u} [AddCommMonoid α] (L : List α) (L' : List α) (h : List.length L = List.length L') : List.sum L + List.sum L' = List.sum (List.zipWith (fun (x x_1 : α) => x + x_1) L L')

theorem List.prod_mul_prod_eq_prod_zipWith_of_length_eq {α : Type u} [CommMonoid α] (L : List α) (L' : List α) (h : List.length L = List.length L') : List.prod L * List.prod L' = List.prod (List.zipWith (fun (x x_1 : α) => x * x_1) L L')