Zulip Chat Archive

Stream: general

Topic: simps and to_additive

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.

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?

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

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

Kevin Buzzard (Dec 12 2020 at 01:22):

Can this issue also be solved relatively simply?

Floris van Doorn (Dec 12 2020 at 01:29):

I think it already does that if you give an @[ancestor] attribute:

Bryan Gin-ge Chen (Dec 12 2020 at 04:09):

We have a related open issue #1639.

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.

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.

Floris van Doorn (Dec 12 2020 at 06:35):

Done in #5331.

Yury G. Kudryashov (Dec 12 2020 at 19:12):

to_additive can't generate structure or class definitions.

Yury G. Kudryashov (Dec 12 2020 at 19:12):

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

Last updated: Aug 03 2023 at 10:10 UTC