feat(data/list/defs): map_with_prefix_suffix and map_with_complement (#…

…10020)

Adds two list definitions: one that will be useful to me, and a generalization which may be useful to @semorrison 



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/data/list/defs.lean

@@ -986,4 +986,32 @@ def zip_with5 (f : α → β → γ → δ → ε → ζ) : list α → list β
 | (x::xs) (y::ys) (z::zs) (u::us) (v::vs) := f x y z u v :: zip_with5 xs ys zs us vs
 | _       _       _       _       _       := []
 
+/-- An auxiliary function for `list.map_with_prefix_suffix`. -/
+def map_with_prefix_suffix_aux {α β} (f : list α → α → list α → β) : list α → list α → list β
+| prev [] := []
+| prev (h::t) := f prev h t :: map_with_prefix_suffix_aux (prev.concat h) t
+
+/--
+`list.map_with_prefix_suffix f l` maps `f` across a list `l`.
+For each `a ∈ l` with `l = pref ++ [a] ++ suff`, `a` is mapped to `f pref a suff`.
+
+Example: if `f : list ℕ → ℕ → list ℕ → β`,
+`list.map_with_prefix_suffix f [1, 2, 3]` will produce the list
+`[f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []]`.
+-/
+def map_with_prefix_suffix {α β} (f : list α → α → list α → β) (l : list α) : list β :=
+map_with_prefix_suffix_aux f [] l
+
+/--
+`list.map_with_complement f l` is a variant of `list.map_with_prefix_suffix`
+that maps `f` across a list `l`.
+For each `a ∈ l` with `l = pref ++ [a] ++ suff`, `a` is mapped to `f a (pref ++ suff)`,
+i.e., the list input to `f` is `l` with `a` removed.
+
+Example: if `f : ℕ → list ℕ → β`, `list.map_with_complement f [1, 2, 3]` will produce the list
+`[f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]]`.
+-/
+def map_with_complement {α β} (f : α → list α → β) : list α → list β :=
+map_with_prefix_suffix $ λ pref a suff, f a (pref ++ suff)
+
 end list