feat(tactic/simps): user-provided names for projections (#4663)

Adds the functionality to specify custom projection names, like this:
```lean
initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
```
These names will always be used and cannot (yet) be manually overridden. 

Implement this for embeddings: `initialize_simps_projections embedding (to_fun → apply)`.

Rename `fixed_points.to_alg_hom_apply -> fixed_points.to_alg_hom_apply_apply`, since `@[simps]` now generates the name `to_alg_hom_apply` instead of `to_alg_hom_to_fun`.

Author: fpvandoorn

src/algebra/big_operators/basic.lean

@@ -273,7 +273,7 @@ calc (∏ x in s.sigma t, f x) =
        ∏ x in s.bind (λa, (t a).map (function.embedding.sigma_mk a)), f x : by rw sigma_eq_bind
   ... = ∏ a in s, ∏ x in (t a).map (function.embedding.sigma_mk a), f x :
     prod_bind $ assume a₁ ha a₂ ha₂ h x hx,
-    by { simp only [inf_eq_inter, mem_inter, mem_map, function.embedding.sigma_mk_to_fun] at hx,
+    by { simp only [inf_eq_inter, mem_inter, mem_map, function.embedding.sigma_mk_apply] at hx,
       rcases hx with ⟨⟨y, hy, rfl⟩, ⟨z, hz, hz'⟩⟩, cc }
   ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ :
     prod_congr rfl $ λ _ _, prod_map _ _ _

src/field_theory/fixed.lean

@@ -239,14 +239,14 @@ fintype_card_le_findim_of_linear_independent $ linear_independent_to_linear_map
 
 namespace fixed_points
 /-- Embedding produced from a faithful action. -/
-@[simps to_fun {fully_applied := ff}]
+@[simps apply {fully_applied := ff}]
 def to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
   [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points G F] F) :=
 { to_fun := λ g, { commutes' := λ x, x.2 g,
     .. mul_semiring_action.to_semiring_hom G F g },
   inj' := λ g₁ g₂ hg, injective_to_semiring_hom G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
 
-lemma to_alg_hom_apply {G : Type u} {F : Type v} [group G] [field F]
+lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F]
   [faithful_mul_semiring_action G F] (g : G) (x : F) :
   to_alg_hom G F g x = g • x :=
 rfl

src/logic/embedding.lean

@@ -24,6 +24,8 @@ infixr ` ↪ `:25 := embedding
 
 instance {α : Sort u} {β : Sort v} : has_coe_to_fun (α ↪ β) := ⟨_, embedding.to_fun⟩
 
+initialize_simps_projections embedding (to_fun → apply)
+
 end function
 
 /-- Convert an `α ≃ β` to `α ↪ β`. -/
@@ -164,12 +166,12 @@ section sigma
 variables {α α' : Type*} {β : α → Type*} {β' : α' → Type*}
 
 /-- `sigma.mk` as an `function.embedding`. -/
-@[simps to_fun] def sigma_mk (a : α) : β a ↪ Σ x, β x :=
+@[simps apply] def sigma_mk (a : α) : β a ↪ Σ x, β x :=
 ⟨sigma.mk a, sigma_mk_injective⟩
 
 /-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family
 of embeddings, then `sigma.map f g` is an embedding. -/
-@[simps to_fun] def sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) :
+@[simps apply] def sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) :
   (Σ a, β a) ↪ Σ a', β' a' :=
 ⟨sigma.map f (λ a, g a), f.injective.sigma_map (λ a, (g a).injective)⟩
 
@@ -199,7 +201,7 @@ protected def subtype_map {α β} {p : α → Prop} {q : β → Prop} (f : α 
 open set
 
 /-- `set.image` as an embedding `set α ↪ set β`. -/
-@[simps to_fun] protected def image {α β} (f : α ↪ β) : set α ↪ set β :=
+@[simps apply] protected def image {α β} (f : α ↪ β) : set α ↪ set β :=
 ⟨image f, f.2.image_injective⟩
 
 end embedding
@@ -219,7 +221,7 @@ end equiv
 namespace set
 
 /-- The injection map is an embedding between subsets. -/
-@[simps to_fun] def embedding_of_subset {α} (s t : set α) (h : s ⊆ t) : s ↪ t :=
+@[simps apply] def embedding_of_subset {α} (s t : set α) (h : s ⊆ t) : s ↪ t :=
 ⟨λ x, ⟨x.1, h x.2⟩, λ ⟨x, hx⟩ ⟨y, hy⟩ h, by { congr, injection h }⟩
 
 end set

src/measure_theory/haar_measure.lean

@@ -208,7 +208,7 @@ begin
   { simp only [mem_set_of_eq], refine subset.trans (image_subset _ h1s) _,
     rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩,
     simp only [mem_preimage] at hg₁, simp only [exists_prop, mem_Union, finset.mem_map,
-      equiv.coe_mul_right, exists_exists_and_eq_and, mem_preimage, equiv.to_embedding_to_fun],
+      equiv.coe_mul_right, exists_exists_and_eq_and, mem_preimage, equiv.to_embedding_apply],
     refine ⟨_, hg₂, _⟩, simp only [mul_assoc, hg₁, inv_mul_cancel_left] }
 end
 

src/tactic/simps.lean

@@ -45,10 +45,13 @@ used by the `@[simps]` attribute.
 - To change the default value, see Note [custom simps projection].
 - You are strongly discouraged to add this attribute manually.
 - The first argument is the list of names of the universe variables used in the structure
-- The second argument is the expressions that correspond to the projections of the structure
-  (these can contain the universe parameters specified in the first argument).
+- The second argument is a list that consists of
+  - a custom name for each projection of the structure
+  - an expressions for each projections of the structure (definitionally equal to the
+    corresponding projection). These expressions can contain the universe parameters specified
+    in the first argument).
 -/
-@[user_attribute] meta def simps_str_attr : user_attribute unit (list name × list expr) :=
+@[user_attribute] meta def simps_str_attr : user_attribute unit (list name × list (name × expr)) :=
 { name := `_simps_str,
   descr := "An attribute specifying the projection of the given structure.",
   parser := do e ← texpr, eval_pexpr _ e }
@@ -77,6 +80,11 @@ attribute [notation_class* coe_fn] has_coe_to_fun
   Get the projections used by `simps` associated to a given structure `str`. The second component is
   the list of projections, and the first component the (shared) list of universe levels used by the
   projections.
+
+  The returned information is also stored in a parameter of the attribute `@[_simps_str]`, which
+  is given to `str`. If `str` already has this attribute, the information is read from this
+  attribute instead.
+
   The returned universe levels are the universe levels of the structure. For the projections there
   are three cases
   * If the declaration `{structure_name}.simps.{projection_name}` has been declared, then the value
@@ -102,15 +110,31 @@ attribute [notation_class* coe_fn] has_coe_to_fun
     ```
       def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm
     ```
+
+  Optionally, this command accepts two optional arguments
+  * If `trace_if_exists` the command will always generate a trace message when the structure already
+    has the attribute `@[_simps_str]`.
+  * The `name_changes` argument accepts a list of pairs `(old_name, new_name)`. This is used to
+    change the projection name `old_name` to the custom projection name `new_name`. Example:
+    for the structure `equiv` the projection `to_fun` could be renamed `apply`. This name will be
+    used for parsing and generating projection names. This argument is ignored if the structure
+    already has an existing attribute.
 -/
 -- if performance becomes a problem, possible heuristic: use the names of the projections to
 -- skip all classes that don't have the corresponding field.
-meta def simps_get_raw_projections (e : environment) (str : name) :
-  tactic (list name × list expr) := do
+meta def simps_get_raw_projections (e : environment) (str : name) (trace_if_exists : bool := ff)
+  (name_changes : list (name × name) := []) : tactic (list name × list (name × expr)) := do
   has_attr ← has_attribute' `_simps_str str,
   if has_attr then do
-    when_tracing `simps.verbose trace!"[simps] > found projection information for structure {str}",
-    simps_str_attr.get_param str
+    data ← simps_str_attr.get_param str,
+    to_print ← data.2.mmap $ λ s, to_string <$> pformat!"Projection {s.1}: {s.2}",
+    let to_print := string.join $ to_print.intersperse "\n        > ",
+    -- We always trace this when called by `initialize_simps_projections`,
+    -- because this doesn't do anything extra (so should not occur in mathlib).
+    -- It can be useful to find the projection names.
+    when (is_trace_enabled_for `simps.verbose || trace_if_exists) trace!
+      "[simps] > Already found projection information for structure {str}:\n        > {to_print}",
+    return data
   else do
     when_tracing `simps.verbose trace!
       "[simps] > generating projection information for structure {str}:",
@@ -172,10 +196,17 @@ Expected type:\n  {raw_expr_type}" },
       when_tracing `simps.verbose trace!
         "        > using {proj_nm} instead of the default projection {relevant_proj.last}.",
       return $ raw_exprs.update_nth pos lambda_raw_expr) <|> return raw_exprs) raw_exprs,
-    when_tracing `simps.verbose trace!
-      "[simps] > generated projections for {str}:\n        > {raw_exprs}",
-    simps_str_attr.set str (raw_univs, raw_exprs) tt,
-    return (raw_univs, raw_exprs)
+    proj_names ← e.structure_fields str,
+    -- if we find the name in name_changes, change the name
+    let proj_names : list name := proj_names.map $
+      λ nm, (name_changes.find $ λ p : _ × _, p.1 = nm).elim nm prod.snd,
+    let projs := proj_names.zip raw_exprs,
+    when_tracing `simps.verbose $ do {
+      to_print ← projs.mmap $ λ s, to_string <$> pformat!"Projection {s.1}: {s.2}",
+      let to_print := string.join $ to_print.intersperse "\n        > ",
+      trace!"[simps] > generated projections for {str}:\n        > {to_print}" },
+    simps_str_attr.set str (raw_univs, projs) tt,
+    return (raw_univs, projs)
 
 /--
   You can specify custom projections for the `@[simps]` attribute.
@@ -194,39 +225,65 @@ Expected type:\n  {raw_expr_type}" },
 library_note "custom simps projection"
 
 /-- Specify simps projections, see Note [custom simps projection].
-  Set `trace.simps.verbose` to true to see the generated projections. -/
+  You can specify custom names by writing e.g.
+  `initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)`.
+  Set `trace.simps.verbose` to true to see the generated projections.
+  If the projections were already specified before, you can call `initialize_simps_projections`
+  again to see the generated projections. -/
 @[user_command] meta def initialize_simps_projections_cmd
   (_ : parse $ tk "initialize_simps_projections") : parser unit := do
   env ← get_env,
-  ns ← many ident,
-  ns.mmap' $ λ nm, do nm ← resolve_constant nm, simps_get_raw_projections env nm
+  ns ← (prod.mk <$> ident <*> (tk "(" >>
+    sep_by (tk ",") (prod.mk <$> ident <*> (tk "->" >> ident)) <* tk ")")?)*,
+  ns.mmap' $ λ data, do
+    nm ← resolve_constant data.1,
+    simps_get_raw_projections env nm tt $ data.2.get_or_else []
 
 /--
   Get the projections of a structure used by `@[simps]` applied to the appropriate arguments.
-  Returns a list of triples (projection expression, projection name, corresponding right-hand-side),
-  one for each projection.
+  Returns a list of quadruples
+  (projection expression, given projection name, original (full) projection name,
+    corresponding right-hand-side),
+  one for each projection. The given projection name is the name for the projection used by the user
+  used to generate (and parse) projection names. The original projection name is the actual
+  projection name in the structure, which is only used to check whether the expression is an
+  eta-expansion of some other expression. For example, in the structure
+
+  Example 1: ``simps_get_projection_exprs env `(α × β) `(⟨x, y⟩)`` will give the output
+  ```
+    [(`(@prod.fst.{u v} α β), `fst, `prod.fst, `(x)),
+     (`(@prod.snd.{u v} α β), `snd, `prod.snd, `(y))]
+  ```
 
-  Example: ``simps_get_projection_exprs env `(α × β) `(⟨x, y⟩)`` will give the output
+  Example 2: ``simps_get_projection_exprs env `(α ≃ α) `(⟨id, id, λ _, rfl, λ _, rfl⟩)``
+  will give the output
   ```
-    [(`(@prod.fst.{u v} α β), `prod.fst, `(x)), (`(@prod.snd.{u v} α β), `prod.snd, `(y))]
+    [(`(@equiv.to_fun.{u u} α α), `apply, `equiv.to_fun, `(id)),
+     (`(@equiv.inv_fun.{u u} α α), `symm_apply, `equiv.inv_fun, `(id)),
+     ...,
+     ...]
   ```
+  The last two fields of the list correspond to the propositional fields of the structure,
+  and are rarely/never used.
 -/
 -- This function does not use `tactic.mk_app` or `tactic.mk_mapp`, because the the given arguments
 -- might not uniquely specify the universe levels yet.
 meta def simps_get_projection_exprs (e : environment) (tgt : expr)
-  (rhs : expr) : tactic $ list $ expr × name × expr := do
+  (rhs : expr) : tactic $ list $ expr × name × name × expr := do
   let params := get_app_args tgt, -- the parameters of the structure
   (params.zip $ (get_app_args rhs).take params.length).mmap' (λ ⟨a, b⟩, is_def_eq a b)
     <|> fail "unreachable code (1)",
   let str := tgt.get_app_fn.const_name,
-  projs ← e.structure_fields_full str,
   let rhs_args := (get_app_args rhs).drop params.length, -- the fields of the object
-  guard (rhs_args.length = projs.length) <|> fail "unreachable code (2)",
-  (raw_univs, raw_exprs) ← simps_get_raw_projections e str,
+  (raw_univs, projs_and_raw_exprs) ← simps_get_raw_projections e str,
+  guard (rhs_args.length = projs_and_raw_exprs.length) <|> fail "unreachable code (2)",
   let univs := raw_univs.zip tgt.get_app_fn.univ_levels,
+  let projs := projs_and_raw_exprs.map $ prod.fst,
+  original_projection_names ← e.structure_fields_full str,
+  let raw_exprs := projs_and_raw_exprs.map $ prod.snd,
   let proj_exprs := raw_exprs.map $
     λ raw_expr, (raw_expr.instantiate_univ_params univs).instantiate_lambdas_or_apps params,
-  return $ proj_exprs.zip $ projs.zip rhs_args
+  return $ proj_exprs.zip $ projs.zip $ original_projection_names.zip rhs_args
 
 /--
   Configuration options for the `@[simps]` attribute.
@@ -316,8 +373,8 @@ meta def simps_add_projections : ∀(e : environment) (nm : name) (suffix : stri
     if is_constant_of (get_app_fn rhs_ap) intro then do -- if the value is a constructor application
       tuples ← simps_get_projection_exprs e tgt rhs_ap,
       let projs := tuples.map $ λ x, x.2.1,
-      let pairs := tuples.map $ λ x, x.2,
-      eta ← expr.is_eta_expansion_aux rhs_ap pairs, -- check whether `rhs_ap` is an eta-expansion
+      let pairs := tuples.map $ λ x, x.2.2,
+      eta ← rhs_ap.is_eta_expansion_aux pairs, -- check whether `rhs_ap` is an eta-expansion
       let rhs_ap := eta.lhoare rhs_ap, -- eta-reduce `rhs_ap`
       /- As a special case, we want to automatically generate the current projection if `rhs_ap`
         was an eta-expansion. Also, when this was a desired projection, we need to generate the
@@ -335,8 +392,14 @@ meta def simps_add_projections : ∀(e : environment) (nm : name) (suffix : stri
           let x := (todo.find $ λ x, projs.all $ λ proj, ¬ ("_" ++ proj.last).is_prefix_of x).iget,
             simp_lemma := nm.append_suffix $ suffix ++ x,
             needed_proj := (x.split_on '_').tail.head in
-          fail!"Invalid simp-lemma {simp_lemma}. Projection {needed_proj} doesn't exist.",
-        tuples.mmap' $ λ ⟨proj_expr, proj, new_rhs⟩, do
+          fail!
+"Invalid simp-lemma {simp_lemma}. Structure {str} does not have projection {needed_proj}.
+The known projections are:
+  {projs}
+You can also see this information by running
+  `initialize_simps_projections {str}`.
+Note: the projection names used by @[simps] might not correspond to the projection names in the structure.",
+        tuples.mmap' $ λ ⟨proj_expr, proj, _, new_rhs⟩, do
           new_type ← infer_type new_rhs,
           let new_todo := todo.filter_map $ λ x, string.get_rest x $ "_" ++ proj.last,
           b ← is_prop new_type,
@@ -380,7 +443,7 @@ meta def simps_tac (nm : name) (cfg : simps_cfg := {}) (todo : list string := []
 
 /-- The parser for the `@[simps]` attribute. -/
 meta def simps_parser : parser (list string × simps_cfg) := do
-/- note: we currently don't check whether the user has written a nonsense namespace as arguments. -/
+/- note: we don't check whether the user has written a nonsense namespace in an argument. -/
 prod.mk <$> many (name.last <$> ident) <*>
   (do some e ← parser.pexpr? | return {}, eval_pexpr simps_cfg e)
 
@@ -420,10 +483,14 @@ derives two simp-lemmas:
     ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
   ```
 
+* You can specify custom projection names, by specifying the new projection names using
+  `initialize_simps_projections`.
+  Example: `initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)`.
+
 * If one of the fields itself is a structure, this command will recursively create
   simp-lemmas for all fields in that structure.
   * Exception: by default it will not recursively create simp-lemmas for fields in the structures
-    `prod` and `pprod`. Give explicit projection names to override this.
+    `prod` and `pprod`. Give explicit projection names to override this behavior.
 
   Example:
   ```lean
@@ -432,7 +499,7 @@ derives two simp-lemmas:
   ```
   generates
   ```lean
-  @[simp] lemma  foo_fst : foo.fst = (1, 2)
+  @[simp] lemma foo_fst : foo.fst = (1, 2)
   @[simp] lemma foo_snd_fst : foo.snd.fst = 3
   @[simp] lemma foo_snd_snd : foo.snd.snd = 4
   ```

test/simps.lean

@@ -237,9 +237,19 @@ run_cmd do
     "Invalid simp-lemma specify.specify1_fst_fst.
 Projection fst doesn't exist, because target is not a structure.",
   success_if_fail_with_msg (simps_tac `specify.specify1 {} ["foo_fst"])
-    "Invalid simp-lemma specify.specify1_foo_fst. Projection foo doesn't exist.",
+    "Invalid simp-lemma specify.specify1_foo_fst. Structure prod does not have projection foo.
+The known projections are:
+  [fst, snd]
+You can also see this information by running
+  `initialize_simps_projections prod`.
+Note: the projection names used by @[simps] might not correspond to the projection names in the structure.",
   success_if_fail_with_msg (simps_tac `specify.specify1 {} ["snd_bar"])
-    "Invalid simp-lemma specify.specify1_snd_bar. Projection bar doesn't exist.",
+    "Invalid simp-lemma specify.specify1_snd_bar. Structure prod does not have projection bar.
+The known projections are:
+  [fst, snd]
+You can also see this information by running
+  `initialize_simps_projections prod`.
+Note: the projection names used by @[simps] might not correspond to the projection names in the structure.",
   success_if_fail_with_msg (simps_tac `specify.specify5 {} ["snd_snd"])
     "Invalid simp-lemma specify.specify5_snd_snd.
 The given definition is not a constructor application:
@@ -586,6 +596,48 @@ initialize_simps_projections equiv
 
 end manual_universes
 
+namespace manual_projection_names
+
+structure equiv (α : Sort*) (β : Sort*) :=
+(to_fun    : α → β)
+(inv_fun   : β → α)
+
+local infix ` ≃ `:25 := manual_projection_names.equiv
+
+variables {α β γ : Sort*}
+
+instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩
+
+def equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun⟩
+
+/-- See Note [custom simps projection] -/
+def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm
+
+initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
+
+run_cmd do
+  e ← get_env,
+  data ← simps_get_raw_projections e `manual_projection_names.equiv,
+  guard $ data.2.map prod.fst = [`apply, `symm_apply]
+
+@[simps {simp_rhs := tt}] protected def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
+⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
+
+example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : α) : (e₁.trans e₂) x = e₂ (e₁ x) :=
+by simp only [equiv.trans_apply]
+
+example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) : (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) :=
+by simp only [equiv.trans_symm_apply]
+
+-- the new projection names are parsed correctly (the old projection names won't work anymore)
+@[simps apply symm_apply] protected def equiv.trans2 (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
+⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
+
+-- initialize_simps_projections equiv
+
+end manual_projection_names
+
+
 -- test transparency setting
 structure set_plus (α : Type) :=
 (s : set α)