Zulip Chat Archive

Stream: general

Topic: attribute resource


view this post on Zulip Kevin Buzzard (Dec 21 2020 at 10:51):

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?

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 10:59):

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.

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:07):

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

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:08):

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 :-)

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:31):

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?

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:38):

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?

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:57):

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?

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 11:59):

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

view this post on Zulip Bhavik Mehta (Dec 21 2020 at 12:00):

attr#simps

view this post on Zulip Bhavik Mehta (Dec 21 2020 at 12:00):

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

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 12:01):

Oh _great_! Thanks!

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 12:25):

@[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.

view this post on Zulip Alex J. Best (Dec 21 2020 at 12:33):

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

view this post on Zulip Kevin Buzzard (Dec 21 2020 at 12:45):

OK, I'll add norm_cast attributes where necessary.

view this post on Zulip Alex J. Best (Dec 21 2020 at 12:52):

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.

view this post on Zulip Alex J. Best (Dec 21 2020 at 12:55):

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:

view this post on Zulip Alex J. Best (Dec 21 2020 at 13:15):

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...?

view this post on Zulip Reid Barton (Dec 21 2020 at 16:04):

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

view this post on Zulip Alex J. Best (Dec 23 2020 at 22:23):

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


Last updated: May 15 2021 at 02:11 UTC