Documentation

Init.Data.List.Zip

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 α) :
@[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.

theorem List.getElem?_zipWith_eq_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {l₁ : List α} {l₂ : List β} {z : γ} {i : Nat} :
(List.zipWith f l₁ l₂)[i]? = some z ∃ (x : α), ∃ (y : β), l₁[i]? = some x l₂[i]? = some y f x y = z
theorem List.getElem?_zip_eq_some {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {z : α × β} {i : Nat} :
(l₁.zip l₂)[i]? = some z l₁[i]? = some z.fst l₂[i]? = some z.snd
@[deprecated List.getElem?_zipWith]
theorem List.get?_zipWith {α : 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
@[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 : αβγ} :
    (List.zipWith f as bs).head? = match as.head?, bs.head? with | some a, some b => some (f a b) | x, x_1 => none
    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₂)
    @[simp]
    theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {l : List α} {l' : List β} :
    List.zipWith f l l' = [] l = [] 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'
    theorem List.take_zipWith :
    ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')
    @[reducible, inline, deprecated List.take_zipWith]
    abbrev List.zipWith_distrib_take :
    ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')
    Equations
    Instances For
      theorem List.drop_zipWith :
      ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')
      @[reducible, inline, deprecated List.drop_zipWith]
      abbrev List.zipWith_distrib_drop :
      ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')
      Equations
      Instances For
        @[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
        Equations
        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
          theorem List.zipWith_eq_cons_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {l : List γ} {f : αβγ} {l₁ : List α} {l₂ : List β} :
          List.zipWith f l₁ l₂ = g :: l ∃ (a : α), ∃ (l₁' : List α), ∃ (b : β), ∃ (l₂' : List β), l₁ = a :: l₁' l₂ = b :: l₂' g = f a b l = List.zipWith f l₁' l₂'
          theorem List.zipWith_eq_append_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁' : List γ} {l₂' : List γ} {f : αβγ} {l₁ : List α} {l₂ : List β} :
          List.zipWith f l₁ l₂ = l₁' ++ l₂' ∃ (w : List α), ∃ (x : List α), ∃ (y : List β), ∃ (z : List β), w.length = y.length l₁ = w ++ x l₂ = y ++ z l₁' = List.zipWith f w y l₂' = List.zipWith f x z
          @[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₂
          theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : αγ) (g : βδ) (l₁ : List α) (l₂ : List β) :
          (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
          theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : αγ) (l₁ : List α) (l₂ : List β) :
          (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
          theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (l₁ : List α) (l₂ : List β) :
          l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
          @[simp]
          theorem List.tail_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
          (l₁.zip l₂).tail = l₁.tail.zip l₂.tail
          theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : l₁.length = l₂.length) :
          (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
          theorem List.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (l : List α) :
          (List.map f l).zip (List.map g l) = List.map (fun (a : α) => (f a, g a)) l
          theorem List.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
          (a, b) l₁.zip l₂a l₁ b l₂
          @[reducible, inline, deprecated List.of_mem_zip]
          abbrev List.mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
          (a, b) l₁.zip l₂a l₁ b l₂
          Equations
          Instances For
            theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
            l₁.length l₂.lengthList.map Prod.fst (l₁.zip l₂) = l₁
            theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
            l₂.length l₁.lengthList.map Prod.snd (l₁.zip l₂) = l₂
            theorem List.map_prod_left_eq_zip {α : Type u_1} {β : Type u_2} {l : List α} (f : αβ) :
            List.map (fun (x : α) => (x, f x)) l = l.zip (List.map f l)
            theorem List.map_prod_right_eq_zip {α : Type u_1} {β : Type u_2} {l : List α} (f : αβ) :
            List.map (fun (x : α) => (f x, x)) l = (List.map f l).zip l
            @[simp]
            theorem List.zip_eq_nil_iff {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
            l₁.zip l₂ = [] l₁ = [] l₂ = []
            theorem List.zip_eq_cons_iff {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l : List (α × β)} {l₁ : List α} {l₂ : List β} :
            l₁.zip l₂ = (a, b) :: l ∃ (l₁' : List α), ∃ (l₂' : List β), l₁ = a :: l₁' l₂ = b :: l₂' l = l₁'.zip l₂'
            theorem List.zip_eq_append_iff {α : Type u_1} {β : Type u_2} {l₁' : List (α × β)} {l₂' : List (α × β)} {l₁ : List α} {l₂ : List β} :
            l₁.zip l₂ = l₁' ++ l₂' ∃ (w : List α), ∃ (x : List α), ∃ (y : List β), ∃ (z : List β), w.length = y.length l₁ = w ++ x l₂ = y ++ z l₁' = w.zip y l₂' = x.zip z
            @[simp]
            theorem List.zip_replicate' {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} :

            See also List.zip_replicate in Init.Data.List.TakeDrop for a generalization with different lengths.

            zipWithAll #

            theorem List.getElem?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option αOption βγ} {i : Nat} :
            (List.zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => none | a?, b? => some (f a? b?)
            @[deprecated List.getElem?_zipWithAll]
            theorem List.get?_zipWithAll {α : 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?)
            @[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
              theorem List.head?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option αOption βγ} :
              (List.zipWithAll f as bs).head? = match as.head?, bs.head? with | none, none => none | a?, b? => some (f a? b?)
              @[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₂
              theorem List.zipWithAll_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : αα') (g : Option α'Option βγ) :
              List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun (a : Option α) (b : Option β) => g (f <$> a) b) l₁ l₂
              theorem List.zipWithAll_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_2} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : ββ') (g : Option αOption β'γ) :
              List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => g a (f <$> b)) l₁ l₂
              theorem List.map_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : Option γOption δα) (l : List γ) (l' : List δ) :
              List.map f (List.zipWithAll g l l') = List.zipWithAll (fun (x : Option γ) (y : Option δ) => f (g x y)) 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_fst :
              ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.fst = List.map Prod.fst l
              @[simp]
              theorem List.unzip_snd :
              ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.snd = List.map Prod.snd l
              @[reducible, inline, deprecated List.unzip_fst]
              abbrev List.unzip_left :
              ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.fst = List.map Prod.fst l
              Equations
              Instances For
                @[reducible, inline, deprecated List.unzip_snd]
                abbrev List.unzip_right :
                ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.snd = List.map Prod.snd l
                Equations
                Instances For
                  theorem List.unzip_eq_map {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
                  l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
                  theorem List.zip_unzip {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
                  l.unzip.fst.zip l.unzip.snd = l
                  theorem List.unzip_zip_left {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
                  l₁.length l₂.length(l₁.zip l₂).unzip.fst = l₁
                  theorem List.unzip_zip_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} :
                  l₂.length l₁.length(l₁.zip l₂).unzip.snd = l₂
                  theorem List.unzip_zip {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} (h : l₁.length = l₂.length) :
                  (l₁.zip l₂).unzip = (l₁, l₂)
                  theorem List.zip_of_prod {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {lp : List (α × β)} (hl : List.map Prod.fst lp = l) (hr : List.map Prod.snd lp = l') :
                  lp = l.zip l'
                  theorem List.tail_zip_fst {α : Type u_1} {β : Type u_2} {l : List (α × β)} :
                  l.unzip.fst.tail = l.tail.unzip.fst
                  theorem List.tail_zip_snd {α : Type u_1} {β : Type u_2} {l : List (α × β)} :
                  l.unzip.snd.tail = l.tail.unzip.snd
                  @[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)