feat(data/list/*): add left- and right-biased versions of map₂ and zip (#4512)

When given lists of different lengths, `map₂` and `zip` truncate the output to
the length of the shorter input list. This commit adds variations on `map₂` and
`zip` whose output is always as long as the left/right input.

Author: JLimperg

src/data/list/basic.lean

@@ -1402,6 +1402,13 @@ by cases l; refl
 theorem map₂_nil (f : α → β → γ) (l : list α) : map₂ f l [] = [] :=
 by cases l; refl
 
+@[simp] theorem map₂_flip (f : α → β → γ) :
+  ∀ as bs, map₂ (flip f) bs as = map₂ f as bs
+| [] [] := rfl
+| [] (b :: bs) := rfl
+| (a :: as) [] := rfl
+| (a :: as) (b :: bs) := by { simp! [map₂_flip], refl }
+
 /-! ### take, drop -/
 @[simp] theorem take_zero (l : list α) : take 0 l = [] := rfl
 
@@ -4024,7 +4031,218 @@ lemma choose_property (hp : ∃ a, a ∈ l ∧ p a) : p (choose p l hp) := (choo
 
 end choose
 
--- A jumble of lost lemmas:
+/-! ### map₂_left' -/
+
+section map₂_left'
+
+-- The definitional equalities for `map₂_left'` can already be used by the
+-- simplifie because `map₂_left'` is marked `@[simp]`.
+
+@[simp] theorem map₂_left'_nil_right (f : α → option β → γ) (as) :
+  map₂_left' f as [] = (as.map (λ a, f a none), []) :=
+by cases as; refl
+
+end map₂_left'
+
+/-! ### map₂_right' -/
+
+section map₂_right'
+
+variables (f : option α → β → γ) (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem map₂_right'_nil_left :
+  map₂_right' f [] bs = (bs.map (f none), []) :=
+by cases bs; refl
+
+@[simp] theorem map₂_right'_nil_right  :
+  map₂_right' f as [] = ([], as) :=
+rfl
+
+@[simp] theorem map₂_right'_nil_cons :
+  map₂_right' f [] (b :: bs) = (f none b :: bs.map (f none), []) :=
+rfl
+
+@[simp] theorem map₂_right'_cons_cons :
+  map₂_right' f (a :: as) (b :: bs) =
+    let rec := map₂_right' f as bs in
+    (f (some a) b :: rec.fst, rec.snd) :=
+rfl
+
+end map₂_right'
+
+/-! ### zip_left' -/
+
+section zip_left'
+
+variables (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem zip_left'_nil_right :
+  zip_left' as ([] : list β) = (as.map (λ a, (a, none)), []) :=
+by cases as; refl
+
+@[simp] theorem zip_left'_nil_left :
+  zip_left' ([] : list α) bs = ([], bs) :=
+rfl
+
+@[simp] theorem zip_left'_cons_nil :
+  zip_left' (a :: as) ([] : list β) = ((a, none) :: as.map (λ a, (a, none)), []) :=
+rfl
+
+@[simp] theorem zip_left'_cons_cons :
+  zip_left' (a :: as) (b :: bs) =
+    let rec := zip_left' as bs in
+    ((a, some b) :: rec.fst, rec.snd) :=
+rfl
+
+end zip_left'
+
+/-! ### zip_right' -/
+
+section zip_right'
+
+variables (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem zip_right'_nil_left :
+  zip_right' ([] : list α) bs = (bs.map (λ b, (none, b)), []) :=
+by cases bs; refl
+
+@[simp] theorem zip_right'_nil_right :
+  zip_right' as ([] : list β) = ([], as) :=
+rfl
+
+@[simp] theorem zip_right'_nil_cons :
+  zip_right' ([] : list α) (b :: bs) = ((none, b) :: bs.map (λ b, (none, b)), []) :=
+rfl
+
+@[simp] theorem zip_right'_cons_cons :
+  zip_right' (a :: as) (b :: bs) =
+    let rec := zip_right' as bs in
+    ((some a, b) :: rec.fst, rec.snd) :=
+rfl
+
+end zip_right'
+
+/-! ### map₂_left -/
+
+section map₂_left
+
+variables (f : α → option β → γ) (as : list α)
+
+-- The definitional equalities for `map₂_left` can already be used by the
+-- simplifier because `map₂_left` is marked `@[simp]`.
+
+@[simp] theorem map₂_left_nil_right :
+  map₂_left f as [] = as.map (λ a, f a none) :=
+by cases as; refl
+
+theorem map₂_left_eq_map₂_left' : ∀ as bs,
+  map₂_left f as bs = (map₂_left' f as bs).fst
+| [] bs := by simp!
+| (a :: as) [] := by simp!
+| (a :: as) (b :: bs) := by simp! [*]
+
+theorem map₂_left_eq_map₂ : ∀ as bs,
+  length as ≤ length bs →
+  map₂_left f as bs = map₂ (λ a b, f a (some b)) as bs
+| [] [] h := by simp!
+| [] (b :: bs) h := by simp!
+| (a :: as) [] h := by { simp at h, contradiction }
+| (a :: as) (b :: bs) h := by { simp at h, simp! [*] }
+
+end map₂_left
+
+/-! ### map₂_right -/
+
+section map₂_right
+
+variables (f : option α → β → γ) (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem map₂_right_nil_left :
+  map₂_right f [] bs = bs.map (f none) :=
+by cases bs; refl
+
+@[simp] theorem map₂_right_nil_right :
+  map₂_right f as [] = [] :=
+rfl
+
+@[simp] theorem map₂_right_nil_cons :
+  map₂_right f [] (b :: bs) = f none b :: bs.map (f none) :=
+rfl
+
+@[simp] theorem map₂_right_cons_cons :
+  map₂_right f (a :: as) (b :: bs) = f (some a) b :: map₂_right f as bs :=
+rfl
+
+theorem map₂_right_eq_map₂_right' :
+  map₂_right f as bs = (map₂_right' f as bs).fst :=
+by simp only [map₂_right, map₂_right', map₂_left_eq_map₂_left']
+
+theorem map₂_right_eq_map₂ (h : length bs ≤ length as) :
+  map₂_right f as bs = map₂ (λ a b, f (some a) b) as bs :=
+begin
+  have : (λ a b, flip f a (some b)) = (flip (λ a b, f (some a) b)) := rfl,
+  simp only [map₂_right, map₂_left_eq_map₂, map₂_flip, *]
+end
+
+end map₂_right
+
+/-! ### zip_left -/
+
+section zip_left
+
+variables (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem zip_left_nil_right :
+  zip_left as ([] : list β) = as.map (λ a, (a, none)) :=
+by cases as; refl
+
+@[simp] theorem zip_left_nil_left :
+  zip_left ([] : list α) bs = [] :=
+rfl
+
+@[simp] theorem zip_left_cons_nil :
+  zip_left (a :: as) ([] : list β) = (a, none) :: as.map (λ a, (a, none)) :=
+rfl
+
+@[simp] theorem zip_left_cons_cons :
+  zip_left (a :: as) (b :: bs) = (a, some b) :: zip_left as bs :=
+rfl
+
+theorem zip_left_eq_zip_left' :
+  zip_left as bs = (zip_left' as bs).fst :=
+by simp only [zip_left, zip_left', map₂_left_eq_map₂_left']
+
+end zip_left
+
+/-! ### zip_right -/
+
+section zip_right
+
+variables (a : α) (as : list α) (b : β) (bs : list β)
+
+@[simp] theorem zip_right_nil_left :
+  zip_right ([] : list α) bs = bs.map (λ b, (none, b)) :=
+by cases bs; refl
+
+@[simp] theorem zip_right_nil_right :
+  zip_right as ([] : list β) = [] :=
+rfl
+
+@[simp] theorem zip_right_nil_cons :
+  zip_right ([] : list α) (b :: bs) = (none, b) :: bs.map (λ b, (none, b)) :=
+rfl
+
+@[simp] theorem zip_right_cons_cons :
+  zip_right (a :: as) (b :: bs) = (some a, b) :: zip_right as bs :=
+rfl
+
+theorem zip_right_eq_zip_right' :
+  zip_right as bs = (zip_right' as bs).fst :=
+by simp only [zip_right, zip_right', map₂_right_eq_map₂_right']
+
+end zip_right
+
+/-! ### Miscellaneous lemmas -/
 
 theorem ilast'_mem : ∀ a l, @ilast' α a l ∈ a :: l
 | a []     := or.inl rfl

src/data/list/defs.lean

@@ -703,4 +703,139 @@ def slice {α} : ℕ → ℕ → list α → list α
 | (succ n) m [] := []
 | (succ n) m (x :: xs) := x :: slice n m xs
 
+/--
+Left-biased version of `list.map₂`. `map₂_left' f as bs` applies `f` to each
+pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, `f` is
+applied to `none` for the remaining `aᵢ`. Returns the results of the `f`
+applications and the remaining `bs`.
+
+```
+map₂_left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
+
+map₂_left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
+```
+-/
+@[simp] def map₂_left' (f : α → option β → γ) : list α → list β → (list γ × list β)
+| [] bs := ([], bs)
+| (a :: as) [] :=
+  ((a :: as).map (λ a, f a none), [])
+| (a :: as) (b :: bs) :=
+  let rec := map₂_left' as bs in
+  (f a (some b) :: rec.fst, rec.snd)
+
+/--
+Right-biased version of `list.map₂`. `map₂_right' f as bs` applies `f` to each
+pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, `f` is
+applied to `none` for the remaining `bᵢ`. Returns the results of the `f`
+applications and the remaining `as`.
+
+```
+map₂_right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
+
+map₂_right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
+```
+-/
+def map₂_right' (f : option α → β → γ) (as : list α) (bs : list β) : (list γ × list α) :=
+map₂_left' (flip f) bs as
+
+/--
+Left-biased version of `list.zip`. `zip_left' as bs` returns the list of
+pairs `(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, the
+remaining `aᵢ` are paired with `none`. Also returns the remaining `bs`.
+
+```
+zip_left' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
+
+zip_left' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
+
+zip_left' = map₂_left' prod.mk
+
+```
+-/
+def zip_left' : list α → list β → list (α × option β) × list β :=
+map₂_left' prod.mk
+
+/--
+Right-biased version of `list.zip`. `zip_right' as bs` returns the list of
+pairs `(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, the
+remaining `bᵢ` are paired with `none`. Also returns the remaining `as`.
+
+```
+zip_right' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
+
+zip_right' [1, 2] ['a'] = ([(some 1, 'a')], [2])
+
+zip_right' = map₂_right' prod.mk
+```
+-/
+def zip_right' : list α → list β → list (option α × β) × list α :=
+map₂_right' prod.mk
+
+/--
+Left-biased version of `list.map₂`. `map₂_left f as bs` applies `f` to each pair
+`aᵢ ∈ as` and `bᵢ ‌∈ bs`. If `bs` is shorter than `as`, `f` is applied to `none`
+for the remaining `aᵢ`.
+
+```
+map₂_left prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
+
+map₂_left prod.mk [1] ['a', 'b'] = [(1, some 'a')]
+
+map₂_left f as bs = (map₂_left' f as bs).fst
+```
+-/
+@[simp] def map₂_left (f : α → option β → γ) : list α → list β → list γ
+| [] _ := []
+| (a :: as) [] := (a :: as).map (λ a, f a none)
+| (a :: as) (b :: bs) := f a (some b) :: map₂_left as bs
+
+/--
+Right-biased version of `list.map₂`. `map₂_right f as bs` applies `f` to each
+pair `aᵢ ∈ as` and `bᵢ ‌∈ bs`. If `as` is shorter than `bs`, `f` is applied to
+`none` for the remaining `bᵢ`.
+
+```
+map₂_right prod.mk [1, 2] ['a'] = [(some 1, 'a')]
+
+map₂_right prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
+
+map₂_right f as bs = (map₂_right' f as bs).fst
+```
+-/
+def map₂_right (f : option α → β → γ) (as : list α) (bs : list β) :
+  list γ :=
+map₂_left (flip f) bs as
+
+/--
+Left-biased version of `list.zip`. `zip_left as bs` returns the list of pairs
+`(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, the
+remaining `aᵢ` are paired with `none`.
+
+```
+zip_left [1, 2] ['a'] = [(1, some 'a'), (2, none)]
+
+zip_left [1] ['a', 'b'] = [(1, some 'a')]
+
+zip_left = map₂_left prod.mk
+```
+-/
+def zip_left : list α → list β → list (α × option β) :=
+map₂_left prod.mk
+
+/--
+Right-biased version of `list.zip`. `zip_right as bs` returns the list of pairs
+`(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, the
+remaining `bᵢ` are paired with `none`.
+
+```
+zip_right [1, 2] ['a'] = [(some 1, 'a')]
+
+zip_right [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
+
+zip_right = map₂_right prod.mk
+```
+-/
+def zip_right : list α → list β → list (option α × β) :=
+map₂_right prod.mk
+
 end list