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 β) : map Prod.swap (l₁.zip l₂) = l₂.zip l₁

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

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

theorem List.zipWith_congr {α : Type u} {β : Type u_1} {γ : Type u_2} (f g : α → β → γ) (la : List α) (lb : List β) (h : Forall₂ (fun (a : α) (b : β) => f a b = g a b) la lb) : zipWith f la lb = zipWith g la lb

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

instance List.instIsSymmOpZipWith {α : Type u} {β : Type u_1} (f : α → α → β) [IsSymmOp f] : IsSymmOp (zipWith f)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[deprecated List.getElem?_zipWith' (since := "2024-07-29")]

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

Alias of List.getElem?_zipWith'.

---

Variant of getElem?_zipWith using Option.map and Option.bind rather than a match.

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

@[deprecated List.get?_zipWith' (since := "2024-07-29")]

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

Alias of List.get?_zipWith'.

@[deprecated List.getElem?_zipWith_eq_some (since := "2024-07-29")]

theorem List.getElem?_zip_with_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : ℕ} : (zipWith f l₁ l₂)[i]? = some z ↔ ∃ (x : α), ∃ (y : β), l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Alias of List.getElem?_zipWith_eq_some.

theorem List.get?_zipWith_eq_some {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l₁ : List α) (l₂ : List β) (z : γ) (i : ℕ) : (zipWith f l₁ l₂).get? i = some z ↔ ∃ (x : α), ∃ (y : β), l₁.get? i = some x ∧ l₂.get? i = some y ∧ f x y = z

@[deprecated List.get?_zipWith_eq_some (since := "2024-07-29")]

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

Alias of List.get?_zipWith_eq_some.

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

@[deprecated List.getElem_zipWith (since := "2024-06-12")]

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

@[deprecated List.getElem_zip (since := "2024-06-12")]

theorem List.get_zip {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (l.zip l').length} : (l.zip l').get i = (l.get ⟨↑i, ⋯⟩, l'.get ⟨↑i, ⋯⟩)

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