canonically_ordered_monoid

Stream: general

[Yaël Dillies]

What's the to_additive tag on docs#canonically_ordered_monoid supposed to achieve? docs#canonically_ordered_add_monoid already exists by that point.

[Yury G. Kudryashov]

It registers the fact that canonically_ordered_add_monoid is the additive version of canonically_ordered_monoid.

[Floris van Doorn]

To expand on what Yury said: to_additive cannot automatically create an additive structure/class (there are some automatically generated declarations - like the projections - that we cannot easily generate using metaprogramming).
But we still need tot tell to_additive that canonically_ordered_add_monoid is the additive version of canonically_ordered_monoid and that the declarations generated automatically by canonically_ordered_monoid also are matched up with their additive counterparts.

[Yaël Dillies]

Interesting! I didn't know about that.

[Yaël Dillies]

However it doesn't work on def?

[Floris van Doorn]

It also works on def. We sometimes first give the additive def, and then the multiplicative def marked with a to_additive attribute. This is sometimes necessary when we hit one of the limitations to to_additive.

[Yaël Dillies]

I tried to do this in data.list.defs but it doesn't work. Is it just because to_additive doesn't exist yet at that point?

[Mario Carneiro]

Most likely. Note that you can also do it in the other direction if the file is a dependency of to_additive, i.e. you can add the attribute to all the core files inside the file that declares to_additive

[Eric Wieser]

Most likely. I think the file that defines to_additive adds the attribute on a bunch of things that appeared earlier in the import graph for exactly this reason

[Mario Carneiro]

I don't think data.list.defs even knows the vocabulary to talk about groups and additive groups

[Yaël Dillies]

It was to link alternating_sum and alternating_prod.

[Floris van Doorn]

You should probably do this retroactively in some list file that has basic tactics (maybe data.list.basic?)

[Floris van Doorn]

similar: https://github.com/leanprover-community/mathlib/blob/de79226c64ab6177029fdbd069fdfe40d252f7cd/src/data/list/basic.lean#L2396

[Floris van Doorn]

-- list.sum was already defined in defs.lean, but we couldn't tag it with `to_additive` yet.

[Yaël Dillies]

Yeah, that's what was being done, and that's how I kept it: #10164

[Floris van Doorn]

Given that this confused you, can you add a docstring to list.alternating_prod that the to_additive is added later and why.

[Eric Wieser]

A regular comment would make more sense IMO

[Yaël Dillies]

I've put both to_additiveization in a section with a comment.