feat(tactic/simps): implement prefix names (#7596)

* You can now write `initialize_simps_projections equiv (to_fun → coe as_prefix)` to add the projection name as a prefix to the simp lemmas: if you then write `@[simps coe] def foo ...` you get a lemma named `coe_foo`.
* Remove the `short_name` option from `simps_cfg`. This was unused and not that useful. 
* Refactor some tuples used in the functions into structures.
* Implements one item of #5489.

Author: fpvandoorn

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,28 @@ 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 also be written in terms of `list.zip` or `list.zip_with`.
+For example, `zip_with3 f xs ys zs` could also be written as
+`zip_with id (zip_with f xs ys) zs`
+or 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`