Map₂ Lemmas

This file contains additional lemmas about a number of list functions related to combining zipping Lists together. In particular, we include lemmas about:

• map₂Left'
• map₂Right'
• zipWith
• zipLeft'
• zipRight'

map₂Left'

@[simp]

theorem List.map₂Left'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) : map₂Left' f as [] = (map (fun (a : α) => f a none) as, [])

map₂Right'

@[simp]

theorem List.map₂Right'_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β) : map₂Right' f [] bs = (map (f none) bs, [])

@[simp]

theorem List.map₂Right'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) : map₂Right' f as [] = ([], as)

@[simp]

theorem List.map₂Right'_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β) : map₂Right' f [] (b :: bs) = (f none b :: map (f none) bs, [])

@[simp]

theorem List.map₂Right'_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β) : map₂Right' f (a :: as) (b :: bs) = let r := map₂Right' f as bs; (f (some a) b :: r.fst, r.snd)

zipWith

theorem List.nil_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List β) : zipWith f [] l = []

theorem List.zipWith_nil {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List α) : zipWith f l [] = []

@[simp]

theorem List.zipWith_flip {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (as : List α) (bs : List β) : zipWith (flip f) bs as = zipWith f as bs

zipLeft'

@[simp]

theorem List.zipLeft'_nil_right {α : Type u} {β : Type v} (as : List α) : as.zipLeft' [] = (map (fun (a : α) => (a, none)) as, [])

@[simp]

theorem List.zipLeft'_nil_left {α : Type u} {β : Type v} (bs : List β) : [].zipLeft' bs = ([], bs)

@[simp]

theorem List.zipLeft'_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) : (a :: as).zipLeft' [] = ((a, none) :: map (fun (a : α) => (a, none)) as, [])

@[simp]

theorem List.zipLeft'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : (a :: as).zipLeft' (b :: bs) = let r := as.zipLeft' bs; ((a, some b) :: r.fst, r.snd)

zipRight'

@[simp]

theorem List.zipRight'_nil_left {α : Type u} {β : Type v} (bs : List β) : [].zipRight' bs = (map (fun (b : β) => (none, b)) bs, [])

@[simp]

theorem List.zipRight'_nil_right {α : Type u} {β : Type v} (as : List α) : as.zipRight' [] = ([], as)

@[simp]

theorem List.zipRight'_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) : [].zipRight' (b :: bs) = ((none, b) :: map (fun (b : β) => (none, b)) bs, [])

@[simp]

theorem List.zipRight'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : (a :: as).zipRight' (b :: bs) = let r := as.zipRight' bs; ((some a, b) :: r.fst, r.snd)

map₂Left

@[simp]

theorem List.map₂Left_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) : map₂Left f as [] = map (fun (a : α) => f a none) as

theorem List.map₂Left_eq_map₂Left' {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β) : map₂Left f as bs = (map₂Left' f as bs).fst

theorem List.map₂Left_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β) : as.length ≤ bs.length → map₂Left f as bs = zipWith (fun (a : α) (b : β) => f a (some b)) as bs

map₂Right

@[simp]

theorem List.map₂Right_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β) : map₂Right f [] bs = map (f none) bs

@[simp]

theorem List.map₂Right_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) : map₂Right f as [] = []

@[simp]

theorem List.map₂Right_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β) : map₂Right f [] (b :: bs) = f none b :: map (f none) bs

@[simp]

theorem List.map₂Right_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β) : map₂Right f (a :: as) (b :: bs) = f (some a) b :: map₂Right f as bs

theorem List.map₂Right_eq_map₂Right' {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β) : map₂Right f as bs = (map₂Right' f as bs).fst

theorem List.map₂Right_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β) (h : bs.length ≤ as.length) : map₂Right f as bs = zipWith (fun (a : α) (b : β) => f (some a) b) as bs

zipLeft

@[simp]

theorem List.zipLeft_nil_right {α : Type u} {β : Type v} (as : List α) : as.zipLeft [] = map (fun (a : α) => (a, none)) as

@[simp]

theorem List.zipLeft_nil_left {α : Type u} {β : Type v} (bs : List β) : [].zipLeft bs = []

@[simp]

theorem List.zipLeft_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) : (a :: as).zipLeft [] = (a, none) :: map (fun (a : α) => (a, none)) as

@[simp]

theorem List.zipLeft_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : (a :: as).zipLeft (b :: bs) = (a, some b) :: as.zipLeft bs

theorem List.zipLeft_eq_zipLeft' {α : Type u} {β : Type v} (as : List α) (bs : List β) : as.zipLeft bs = (as.zipLeft' bs).fst

zipRight

@[simp]

theorem List.zipRight_nil_left {α : Type u} {β : Type v} (bs : List β) : [].zipRight bs = map (fun (b : β) => (none, b)) bs

@[simp]

theorem List.zipRight_nil_right {α : Type u} {β : Type v} (as : List α) : as.zipRight [] = []

@[simp]

theorem List.zipRight_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) : [].zipRight (b :: bs) = (none, b) :: map (fun (b : β) => (none, b)) bs

@[simp]

theorem List.zipRight_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : (a :: as).zipRight (b :: bs) = (some a, b) :: as.zipRight bs

theorem List.zipRight_eq_zipRight' {α : Type u} {β : Type v} (as : List α) (bs : List β) : as.zipRight bs = (as.zipRight' bs).fst