Topic: lemma naming by @[simps]
Floris van Doorn (Sep 18 2020 at 19:33):
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
to_fun? Because, when I see a simp-lemma whose name ends in
to_funI assume that it is a lemma that turns
f.to_funinto a coerced
(f : _ → _).
Or will this require ugly hackery?
I've been thinking about custom naming of
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
foo_coe? The former seems more standard in mathlib, but the latter is probably be more standard for all projections not named
- What to do with multiple projections. For example, the following lemma generated by
simpscame 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
Johan Commelin (Sep 19 2020 at 03:36):
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 (Oct 17 2020 at 22:30):
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.
Last updated: May 14 2021 at 12:18 UTC