Any news on semigroup powers?

Stream: mathlib4

[Uni Marx]

there's #22517 but from what I can gather from an old topic on here it seems to have been abandoned for performance reasons as well as that it is rather annoying to have another power to implement everywhere. has anyone been thinking about new approaches since then/is the old one still considered more-or-less viable? I'd like to work on some semigroup theory but it's quite hard without basics like this nailed down

[Alex Meiburg]

+1, I recently "gave up" on formalizing a big results because it was a bunch of terrible working with semigroup powers. (We're proving a weaker result that it's only true on monoids.)

[Kevin Buzzard]

I wonder whether we should just basically merge #22517 and take the hit.

[Junyan Xu]

I think this is a good opportunity to unbundle npow from Monoid.

[Junyan Xu]

I think there needn't be any change to existing classes: you can just define class SemigroupPNatPow like the class MonoidNPow I extract here.

[Uni Marx]

the issue with that is that it's a bit unclear (at least to me) where to insert the extra [MonoidNPow] hypothesis for defeq or extensionality reasons

[Uni Marx]

you write
theorem blah [Monoid M] (x : M) : x^n = 1 and specialize it to the integers or whatever, then get potentially confused about mismatching instances, right? not as huge of a deal for semigroups since PNat powers are going to be way less prevalent, but important to keep in mind

[Matthew Ballard]

docs#NatPow

[Uni Marx]

What about it?

[Kenny Lau]

what's the argument for unbundling npow from Monoid?

[Matthew Ballard]

I think there is little value beyond unbundling the data. I started an attempt at factoring out as a parent 29482 but then noticed that elaboration helper class in core.

[Matthew Ballard]

Inlined data is more likely to get unfolded unnecessarily.

[Eric Wieser]

Kevin Buzzard said:

I wonder whether we should just basically merge #22517 and take the hit.

It's picked up conflicts with Kim's work to use a repeated-squaring power implementation by default

[Jovan Gerbscheid]

Is it understood what causes the big performace hit?

[Jireh Loreaux]

@Matthew Ballard said on GitHub:

I wonder if extending a new PNatPow class would be better. I have been playing around with this for Monoid but don't have the bandwidth to get things building completely. This might be a more targeted test ground.

Why do you think this would be significantly better?

[Matthew Ballard]

I’ve seen these provided as inlined lambdas for the existing pow fields. Those can be more aggressively unfolded. Separately, when autoparams inject something compared to you building it by hand, Lean might need to work to figure they are defeq.

Will it be significantly better? Probably not. Most likely it just becomes another field that needs to be checked when Lean has to unify two instances.

Why does it end up here so often? Better diagnostics would be nice.

Even so gating data carrying stuff to be filled out by typeclass synthesis with actual classes seems like good hygiene regardless. Autoparams can be set in the child classes if desired.