attribute resource

Stream: general

[Kevin Buzzard]

I just found out the hard way that @[to_additive, simp] doesn't attach the simp attribute to the to_additive-ised version of the lemma (I'm adding multiplicative versions of some additive lemmas in a branch and a random file broke); one has instead to do [simp, to_additive]. On the other hand there are several occurrences of [to_additive, simp] in mathlib (so other people also don't know this). Of course this sort of thing will be obvious to people who actually know how to_additive works, but for people like me, who just want to do stuff with valuations and don't have a clue about what is going on with attributes, it's hard to know where to look. In an unrelated PR Bhavik just told me to add [simps] to a lemma and of course I'll do this, but again I don't know where to look to find out what this actually does (I don't want to plough through commit messages or library notes or old Zulip messages really, this is quite inefficient). I'm wondering if it is getting to the point where we need one document explaining basic stuff about modern attributes and tricks for using them. How might I go about starting to write this?

[Kevin Buzzard]

This is all documented in algebra.group.to_additive, I now discover (I had no idea that to_additive was defined in algebra.group and I don't know how to discover this (right clicking on a @[to_additive] doesn't work). I still don't know how to look up documentation for simps -- if I did, I wouldn't be asking here.

[Kevin Buzzard]

#5468 (you can tell it's the end of term)

[Kevin Buzzard]

Along the way I was amused to note that @[to_additive] lemma mul_equiv_of_localizations_right_inv (about a right inverse function) is changed to ...right_neg by to_additive :-)

[Kevin Buzzard]

Oh great, I just found tactic/simps (whilst looking for occurrences of the regex to_additive[^\]]). OK so now the dust (and an unexpected PR) has settled, my revised observation is that it is hard to find documentation for attributes, unless I'm missing a trick. Attributes appear to have been carefully documented, but apparently we don't yet know if the documentation goes in tactic or algebra. Can we make right clicking on an attribute take us to the documentation for the attribute? I think that if this had happened I would never have opened this thread. If we can't, can we somehow solve this problem another way so I can naturally find a way to read about the intricacies of @[to_additive] or the explanation of what @[simps] means, without having to ask here?

[Kevin Buzzard]

Bug report -- @[simp, norm_cast, to_additive] doesn't attach the norm_cast attribute to the to_additivised lemma (this actually happens in e.g. algebra/ordered_monoid). @Floris van Doorn is this a one-line fix?

[Kevin Buzzard]

This is more confusing than I first imagined. @[to_additive, priority 100] instance linear_ordered_comm_group.to_ordered_comm_group seems to put the 100 priority on the additive instance even though it's after to_additive. Maybe this is a bit above my pay grade after all?

[Kevin Buzzard]

[to_additive, ext] does not put the ext attribute on the additive lemma.

[Bhavik Mehta]

attr#simps

[Bhavik Mehta]

I can't answer the other questions but I can show you that!

[Kevin Buzzard]

Oh _great_! Thanks!

[Kevin Buzzard]

@[continuity, to_additive] continuous.mul does not put the continuity attribute on continuous.add in topology/algebra/monoid. If there's a simple fix for these then I can add them to the PR.

[Alex J. Best]

I took a look at the norm_cast to additive thing, and I'm fairly sure its not a 1-line fix, or at the very least the "obvious" one line to fix isn't sufficient

[Kevin Buzzard]

OK, I'll add norm_cast attributes where necessary.

[Alex J. Best]

To add some more detail, norm_cast and others are user attributes, and are more involved than the basic attributes like instance and simp. User attributes take parameters (in the case of norm cast this is whether it is an elim, squash or whatever) and currently the code does not even attempt to copy user attributes.

[Alex J. Best]

Probably its only 20 lines to add this? I might give it a go later, but if anyone else wants to beat me to it go ahead :smile:

[Alex J. Best]

Also I noticed that norm_cast doesn't show up in the docs, I think that is because we need to update https://github.com/leanprover-community/doc-gen/blob/459e19a8f6ec6de8c2fe32d6543a08ac7ecba385/src/export_json.lean#L230 . What else should we include there now? Continuity...?

[Reid Barton]

attr#to_additive also has the answers to some of your questions, above "Implementation notes"

[Alex J. Best]

I made #5487 for this, lets see what breaks, comments welcome :smile: