Zulip Chat Archive

Stream: new members

Topic: lemmas for add_equiv


view this post on Zulip Andre Knispel (Aug 14 2020 at 14:22):

There are many lemmas for mul_equiv that don't seem to exist for add_equiv. Is there some way of converting them, or can I use them somehow without duplicating them?

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 15:15):

Can you give an example?

view this post on Zulip Andre Knispel (Aug 14 2020 at 15:18):

There is map_one, saying that mul_equiv respects 1, but I can't find the equivalent one in the additive case

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 15:19):

import tactic

#check mul_equiv.map_one
#check add_equiv.map_zero

Both work fine for me.

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 15:20):

@[simp, to_additive]
lemma map_one {M N} [monoid M] [monoid N] (h : M * N) : h 1 = 1 :=
by rw [mul_one (h 1), h.apply_symm_apply 1, h.map_mul, one_mul]

That to_additive attribute that the lemma is tagged with, means "automatically generate the additive version and give it an appropriate name"; you won't see the proof of the additive version explicitly in mathlib because it's auto-generated by the system.

view this post on Zulip Andre Knispel (Aug 14 2020 at 15:21):

Ah, I see, thanks! I didn't expect that!

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 15:23):

Attributes are some of the hardest things to figure out in Lean. They are not particuarly well documented. When you type @[foo] lemma bar ... then all this means that Lean tags bar with the foo attribute. Some of these attributes are little more than labels, e.g. tagging something with simp just says "simplifier, use me if you need me", but other tags actually make stuff happen on the spot. We should have a list somewhere. Is there a list somewhere? I've just picked them up from seeing them so many times.

view this post on Zulip Andre Knispel (Aug 14 2020 at 15:35):

Are they builtins? Or is there e.g. some fancy metaprogram that generates the additive version if it sees such a tag?

view this post on Zulip Reid Barton (Aug 14 2020 at 15:41):

There are both kinds, but to_additive is implemented in mathlib: src#to_additive.attr

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 16:36):

More precisely: @[foo] lemma bar means that once lemma bar is parsed and added to the environment, Lean will run the function associated with attribute foo. This function can do whatever it wants. to_additive parses both declaration and definition of its argument and tries to generate the corresponding lemma/def with all * replaced with + etc.

view this post on Zulip Bryan Gin-ge Chen (Aug 14 2020 at 16:39):

There is a doc page on to_additive now (suggestions welcome!): https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive


Last updated: May 13 2021 at 18:26 UTC