Zulip Chat Archive

Stream: general

Topic: simps and to_additive


view this post on Zulip Johan Commelin (Dec 11 2020 at 08:02):

Do simps and to_additive play well together?

/-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
@[simps, to_additive "Composition of additive monoid morphisms
(`add_monoid_hom.comp`) as an additive monoid morphism."]
def comp_hom [monoid M] [comm_monoid N] [comm_monoid P] :

this generate monoid_hom.comp_hom_apply_apply but the additive version seems to be missing.

view this post on Zulip Eric Wieser (Dec 11 2020 at 08:09):

What order do the attributes execute in? Is it left to right, or the reverse order like python?

view this post on Zulip Reid Barton (Dec 11 2020 at 12:32):

to_additive should be last (https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive)
but there's also a fixed list of attributes that it copies somewhere, I think

view this post on Zulip Floris van Doorn (Dec 12 2020 at 01:05):

This can easily be implemented by adding simps to this list: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group/to_additive.lean#L296

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

Can this issue also be solved relatively simply?

view this post on Zulip Floris van Doorn (Dec 12 2020 at 01:29):

I think it already does that if you give an @[ancestor] attribute:
https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive
https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group/defs.lean#L64-L70

view this post on Zulip Bryan Gin-ge Chen (Dec 12 2020 at 04:09):

We have a related open issue #1639.

view this post on Zulip Johan Commelin (Dec 12 2020 at 04:14):

hmm, is it still true that to_additive shouldn't be used for structures? because that suggests I need a different way of fixing the issue, namely by manually defining add_monoid_hom.comp_hom.

view this post on Zulip Floris van Doorn (Dec 12 2020 at 04:47):

You are using to_additive for an object in a structure, which I think was always fine.

view this post on Zulip Floris van Doorn (Dec 12 2020 at 06:35):

Done in #5331.

view this post on Zulip Yury G. Kudryashov (Dec 12 2020 at 19:12):

to_additive can't generate structure or class definitions.

view this post on Zulip Yury G. Kudryashov (Dec 12 2020 at 19:12):

E.g., it can't generate class add_group from class group.


Last updated: May 14 2021 at 12:18 UTC