lemma naming by @[simps]

Stream: general

[Floris van Doorn]

I'm copying this comment from #4169 to get more visibility. @Sebastien Gouezel @Scott Morrison @others: opinions?

This was in response to @Johan Commelin's comment:

Hmmm, I really like simps! Would it be possible to have the new names use coe instead of to_fun? Because, when I see a simp-lemma whose name ends in to_fun I assume that it is a lemma that turns f.to_fun into a coerced (f : _ → _).

Or will this require ugly hackery?

I've been thinking about custom naming of @[simps].

Just renaming a projection should not be a problem. The nontrivial thing is to decide on the syntax to (1) do this automatically every time and (2) do this once for a specific simps attribute (if we want that).
An even easier thing to do is to is just to rename all projections that are coercions coe (and have no further control over it).

However, there are still questions like

• do we want the lemma name coe_foo or foo_coe? The former seems more standard in mathlib, but the latter is probably be more standard for all projections not named coe.
• What to do with multiple projections. For example, the following lemma generated by simps came up in #4155:

fixed_points.to_alg_hom_to_fun_to_fun : ∀ (G : Type u) (F : Type v) [_inst_4 : group G] [_inst_5 : field F]
[_inst_6 : faithful_mul_semiring_action G F] (g : G) (a : F), ⇑(⇑(to_alg_hom G F) g) a = g • a

If we rename the projections, this might become fixed_points.to_alg_hom_coe_coe. There is already an option to only use the last projection name, so that it would become fixed_points.to_alg_hom_coe. That is satisfactory in this case, but in other cases you might want more freedom (if projection X and then Y is applied, I want the name to be foo_Z instead of foo_X_Y).

[Johan Commelin]

Thanks a lot for looking into this Floris. I'm afraid that I can't be of much help. But it's clear that simps adds some really nice icing on the cake that is mathlib/lean.

[Floris van Doorn]

The low-hanging fruit is done in #4663. We can now rename projection names to a different string. We cannot rename a string of projections into 1 short name, and we cannot override the custom name once we have specified it. But the features of #4663 should cover 95+% of the cases.