Zulip Chat Archive

Stream: new members

Topic: lemmas for add_equiv

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?

Kevin Buzzard (Aug 14 2020 at 15:15):

Can you give an example?

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

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.

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.

Andre Knispel (Aug 14 2020 at 15:21):

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

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.

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?

Reid Barton (Aug 14 2020 at 15:41):

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

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.

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: Dec 20 2023 at 11:08 UTC