[Merged by Bors] - feat(tactic/simps): implement prefix names

src/data/list/defs.lean

@@ -17,8 +17,7 @@ namespace list
 
 open function nat native (rb_map mk_rb_map rb_map.of_list)
 universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
-
+variables {α β γ δ ε ζ : Type*}
 instance [decidable_eq α] : has_sdiff (list α) :=
 ⟨ list.diff ⟩
 
@@ -936,4 +935,27 @@ Asynchronous version of `list.map`.
 meta def map_async_chunked {α β} (f : α → β) (xs : list α) (chunk_size := 1024) : list β :=
 ((xs.to_chunks chunk_size).map (λ xs, task.delay (λ _, list.map f xs))).bind task.get
 
+/-!
+  We add some n-ary versions of `list.zip_with` for functions with more than two arguments.
+  These can be written in terms of `list.zip` and `list.map`, but these are more convenient
+  (and efficient) to use.
+  For example, `zip_with3 f xs ys zs` could also be written as
+  `(zip xs $ zip ys zs).map $ λ ⟨x, y, z⟩, f x y z`.
+-/
+
+/-- Ternary version of `list.zip_with`. -/
+def zip_with3 (f : α → β → γ → δ) : list α → list β → list γ → list δ
+| (x::xs) (y::ys) (z::zs) := f x y z :: zip_with3 xs ys zs
+| _       _       _       := []
+
+/-- Quaternary version of `list.zip_with`. -/
+def zip_with4 (f : α → β → γ → δ → ε) : list α → list β → list γ → list δ → list ε
+| (x::xs) (y::ys) (z::zs) (u::us) := f x y z u :: zip_with4 xs ys zs us
+| _       _       _       _       := []
+
+/-- Quinary version of `list.zip_with`. -/
+def zip_with5 (f : α → β → γ → δ → ε → ζ) : list α → list β → list γ → list δ → 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
+| _       _       _       _       _       := []
+
 end list

src/meta/expr.lean

@@ -95,11 +95,22 @@ meta def sanitize_name : name → name
 | (name.mk_string s p) := name.mk_string s $ sanitize_name p
 | (name.mk_numeral s p) := name.mk_string sformat!"n{s}" $ sanitize_name p
 
-/-- Append a string to the last component of a name -/
+/-- Append a string to the last component of a name. -/
 def append_suffix : name → string → name
 | (mk_string s n) s' := mk_string (s ++ s') n
 | n _ := n
 
+/-- Update the last component of a name. -/
+def update_last (f : string → string) : name → name
+| (mk_string s n) := mk_string (f s) n
+| n := n
+
+/-- `append_to_last nm s is_prefix` adds `s` to the last component of `nm`,
+  either as prefix or as suffix (specified by `is_prefix`), separated by `_`.
+  Used by `simps_add_projections`. -/
+def append_to_last (nm : name) (s : string) (is_prefix : bool) : name :=
+nm.update_last $ λ s', if is_prefix then s ++ "_" ++ s' else s' ++ "_" ++ s
+
 /-- The first component of a name, turning a number to a string -/
 meta def head : name → string
 | (mk_string s anonymous) := s

src/tactic/reserved_notation.lean

@@ -39,6 +39,7 @@ reserve prefix `#where`:max
 
 -- used in `tactic/simps.lean`
 reserve notation `initialize_simps_projections`
+reserve notation `as_prefix`
 
 -- used in `tactic/lift.lean`
 reserve notation `to`