simps and to_additive

Stream: general

[Johan Commelin]

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.

[Eric Wieser]

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

[Reid Barton]

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

[Floris van Doorn]

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

[Kevin Buzzard]

Can this issue also be solved relatively simply?

[Floris van Doorn]

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

[Bryan Gin-ge Chen]

We have a related open issue #1639.

[Johan Commelin]

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.

[Floris van Doorn]

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

[Floris van Doorn]

Done in #5331.

[Yury G. Kudryashov]

to_additive can't generate structure or class definitions.

[Yury G. Kudryashov]

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