formalizing growth of the Grigorchuk group in Lean 4

Stream: mathlib4

[Yury G. Kudryashov]

@Laurent Bartholdi and I are going to formalize estimates on the growth of the Grigorchuk group in Lean 4, so we're going to start making feature PRs unique to mathlib4. The first two are !4#2192 and !4#2193.

[Eric Wieser]

Should we have a new label for "new theory not in mathlib3"?

[Mario Carneiro]

Wouldn't that just be the negation of a port-like tag? I would rather this be the default

[Eric Wieser]

The advantage of an explicit label is it distinguishes "new mathlib4 content" from "I forgot to label this"

[Yury G. Kudryashov]

The first nontrivial PR: !4#2214 (needs a lot of documentation; possibly, needs @[to_additive])

[Thomas Murrills]

Eric Wieser said:

The advantage of an explicit label is it distinguishes "new mathlib4 content" from "I forgot to label this"

Plus: color coding and easy github UI filtering! :)

[Eric Wieser]

Yury G. Kudryashov said:

The first nontrivial PR: !4#2214 (needs a lot of documentation; possibly, needs @[to_additive])

Is this worth the boilerplate vs using @free_product bool or @free_product (fin 2)? (docs#free_product / docs4#FreeProduct)

[Eric Wieser]

I think this perhaps highlights a danger of adding new content to mathlib4 mid-port; the content you add can end up overlapping with other content that hasn't been ported yet (port-status#group_theory/free_product)

[Yury G. Kudryashov]

Yes, it is worth it. A minor argument is that M and N can be in different universes (I don't care too much about it). A more important argument is that we don't have machinery to go from [Monoid M] [Monoid N] to ∀ i, Monoid (![M, N] i).

[Yury G. Kudryashov]

Also, Con gives the universal property for free, so proving all these properties directly is as easy (if not easier) than transfering them from FreeProduct ![M, N].

[Yury G. Kudryashov]

And I want to have convenience API based on Sum instead of Sigma.

[Yury G. Kudryashov]

How should I call the additive version of FreeProd? FreeSum? Something else?

[Yury G. Kudryashov]

The PR !4#2214 is ready for review. @Floris van Doorn , could you please have a look at the last 4 definitions? I tried to generate the additive ones using to_additive but it doesn't translate _ : MulOneClass PUnit to _ : AddZeroClass PUnit. This looks like the reversed version of the issue we had with Nats. Is it easy to (locally?) disable the rule you introduced to make it work with 1 : Nat for PUnit?

[Yury G. Kudryashov]

@Eric Wieser I added a label new-feature. Feel free to edit name/description/color.

[Reid Barton]

Yury G. Kudryashov said:

How should I call the additive version of FreeProd? FreeSum? Something else?

I think it's fine if it doesn't exist

[Yury G. Kudryashov]

free_sum doesn't exist in mathlib3.

[Kevin Buzzard]

Sounds very easy to port then ;-)

[Yury G. Kudryashov]

What is easy to port?

[Floris van Doorn]

Yury G. Kudryashov said:

The PR !4#2214 is ready for review. Floris van Doorn , could you please have a look at the last 4 definitions? I tried to generate the additive ones using to_additive but it doesn't translate _ : MulOneClass PUnit to _ : AddZeroClass PUnit. This looks like the reversed version of the issue we had with Nats. Is it easy to (locally?) disable the rule you introduced to make it work with 1 : Nat for PUnit?

This heuristic is not applied to PUnit.

The problem is that the synthesized instance for MulOneClass PUnit is derived from the instance PUnit.commRing : CommRing PUnit. The latter (of course) doesn't have an additive analogue, and so to_additive cannot translate the instance.
This is fixed if all multiplicative only instances on PUnit (like MulOneClass) are not derived from any ring-like instances.
This can probably be fixed by setting manual instance priorities. In this case, setting MulZeroOneClass.toMulOneClass to have a lower priority than Monoid.toMulOneClass. More generally, forgetful instances that have additive+multiplicative data and forget the additive data should maybe have a lower priority than instances that don't involve additive data in the first place.