PNat powers in a semigroup

Stream: mathlib4

[Scott Carnahan]

I was hoping to apply strictly positive integer powers to a semigroup M (or positive integer scalar multiples in an AddSemigroup M), but there seems to be a can of worms here.

I could write a [Pow M ℕ+] (or [SMul ℕ+ M]) instance using the existing definition of semigroup, but I run into an instance diamond with Pi types. The problem seems to be that powers in a product of semigroups (which has a semigroup instance) is not defeq to component-wise powers. This is the same problem (described in Mathlib.Algebra.Group.Defs) that led to the inclusion of ℕ powers into the definition of monoid.

One solution is to add PNat powers to the definition of semigroup. This clears up the diamond, but leads to another problem: monoids extend semigroups, so with the existing definition of monoid, we would have both ℕ+ powers and ℕ powers. If we wanted a [Pow M ℕ+] instance from anything with [Pow M ℕ] structure (this seems reasonable to me), this could lead to another diamond, unless we make the powers defeq.

Does this mean we need the monoid npow to use the semigroup pnpow somehow? I am inexperienced with instances and diamonds, so I don't see a good way out of this mess.

[Eric Wieser]

Scott Carnahan said:

If we wanted a [Pow M ℕ+] instance from anything with [Pow M ℕ] structure (this seems reasonable to me)

This doesn't sound reasonable to me; we don't have anything analogous for Int and Nat powers. In general constructing data in a "backwards" way in typeclass search is a bad idea, and almost always leads to diamonds.

[Riccardo Brasca]

What we want is a theorem saying the two powers are compatible. And this will always hold.

[Kevin Buzzard]

I thought that @Jireh Loreaux has been saying for at least a year that we need to refactor semigroup to add a field pnpow?

[Floris van Doorn]

I know @Jireh Loreaux was also thinking about doing this, and started with this on branch#j-loreaux/ppow.
I am a bit worried about performance issues, and that the definition of group will contain 3 power operations...

[Riccardo Brasca]

Yes, this is not the first time the conversation pops up...

[Eric Wieser]

@Floris van Doorn: meanwhile for non-commutative (smul) cases I'm looking at doubling the number of power operations... So unless we let AddMonoid and Monoid diverge in terms of a 1:1 field mapping, they'll end up even bigger

[Kevin Buzzard]

Did the "add nsmul and zsmul to groups" PR give us a performance hit?

[Jireh Loreaux]

Yes, I did start on this on branch#j-loreaux/ppow, but it was causing performance issues, and I never finished getting it compiling (I can't remember how much was left to do). It's possible that it could be revived and those performance issues would go away because of more recent performance upgrades to master.

[Jireh Loreaux]

Also, we'll probably want the Pow M ℕ+ to be embedded in Mul, not Semigroup to allow for non-associative multiplications which are nevertheless power associative (we could have a mixin class IsPowAssoc for that possibly). Likewise, we'll probably want to move Pow M ℕ from Monoid to MulOneClass.

[Jireh Loreaux]

Ultimately though, I am worried about the sustainability of this approach. NormedField and LinearOrderedField in particular are absurdly large with this approach and with Eric's suggestions for non-commutativity, which I think are likely necessary.

[Scott Carnahan]

It's nice to see that someone else is working on it. I had tried the Pow M ℕ+ instance for semigroups in #8618 but I guess it needs to be deleted.

[Floris van Doorn]

Actually, I like the mixin approach, with the class [PNatPowAssoc M]. Just leave out the instance instance [Semigroup M] : Pow M ℕ+.
Does that scale? Are there diamond issues with that? I don't see any on first glance.
The main downside I see is that you have to write [Semigroup M] [Pow M ℕ+] [PNatPowAssoc M] to talk about "semigroup with its power operation on ℕ+". However, this will probably an uncommon enough operation that I don't think that is a huge problem. The main advantage is that we don't have to add more superfluous fields to the whole algebraic hierarchy.
Thoughts?

[Kevin Buzzard]

If "the main downside" is something which we can probably cover up with some coding hackery then this sounds great! Would this have worked for nsmul and zsmul? If not then what's the catch?

[Floris van Doorn]

I don't see a reason why it wouldn't work, but that is of course different than "this actually works". A difference is that nsmul and zmul will be used more often, so you more often have to write extra things.

[Eric Wieser]

A difference is that nsmul and zmul will be used more often, so you more often have to write extra things.

This is ultimately the tradeoff with many of these diamonds; either you have to add "obvious" fields to every instance of some basic algebraic structure, or every caller has to add extra "obvious" assumptions when they need them.

Note that using [AddCommGroup A] [Module Int A] instead of adding zsmul would not have worked, unless we were also willing to give up the [Semiring R] : Module R R instance (otherwise we'd still get a diamond for Module Int Int.

[Jireh Loreaux]

That's not the mixin approach I was suggesting. Instead, I meant that the data would be available from Mul, including the Pow instance, but the useful lemmas would only apply in the presence of an IsPowAssoc instance.

[Floris van Doorn]

As a test, I refactored everything until Module.Basic (except abel) using my suggested approach, but for integer powers and integer smuls. This is in branch#group_pow_mixin. I'm quite sure this is doable for all of mathlib, if we want it. It makes some things a bit more verbose: you have to add some superfluous type-classes, like
[AddCommGroup M] [SMul ℤ M] [ZSMul M]
whenever you want to use the scalar multiplication with ℤ. On all concrete types and type constructors, you have to add these as instances (though it is barely more work than the status quo, since usually you gave the zpow field in the Group instance. But we have fewer fields in DivInvMonoid (and hence in all classes extending it).

We get the instance [AddCommGroup M] [SMul ℤ M] [ZSMul M] : Module ℤ M, and this does not lead to any diamond issues:

example : Semiring.toModule (R := ℤ) = AddCommGroup.intModule ℤ := by
  with_reducible_and_instances rfl -- works

I'm wondering how it would affect performance. I think it would be an improvement, but I don't know how much. Is there a way to test that without fixing all of mathlib?

[Jireh Loreaux]

But to actually get the lemmas we need a LawfulPow class right?

[Jireh Loreaux]

Oh sorry, that's your ZPow.

[Jireh Loreaux]

I have to say that I like this a lot, assuming it actually helps with performance, which is still TBD. Although I wonder whether it might not be better to make ZPow M extend Pow M ℤ instead. I don't think that would be problematic, and it would reduce clutter in statements.

[Jireh Loreaux]

@Floris van Doorn one way to test it which might be easier: instead of trying to pull zpow out, we could try, starting from the same commit on master, adding ppow in both ways. Although this may not serve as a realistic comparison.

[Jireh Loreaux]

The mixin approach has another advantage: due to the import hierarchy of low-level files, adding the ppow field to Semigroup had to look like:

ppow : ∀ n : ℕ, 0 < n → G → G := ppowRec

as opposed to the more natural

ppow : ℕ+ → G → G := ppowRec

because I couldn't import PNat into Algebra.Group.Defs.

With mixins, you can just declare them later.

[Yaël Dillies]

Sorry, why can't we just reuse pow here?

[Yaël Dillies]

You can always send 0 to id, as a junk value.

[Yaël Dillies]

Or is the problem somehow occurring for semigroups which are only sometimes monoids?

[Eric Wieser]

Yaël Dillies said:

You can always send 0 to id, as a junk value.

If you do this, then you can't write Semigroup.ext without adding a meaningless assumption about junk values

[Yaël Dillies]

Out of all possible concerns being able to write Semigroup.ext is definitely not the one I would have put forward.

[Eric Wieser]

I mean, it was the first thing that came to mind that expressed "semigroups would no longer be uniquely determined by their multiplication"

[Jireh Loreaux]

There's no reason to provide a junk value. The issue is only that the type signature doesn't look as clean as would be ideal, but that's a minor issue.

[Floris van Doorn]

Jireh Loreaux said:

There's no reason to provide a junk value. The issue is only that the type signature doesn't look as clean as would be ideal, but that's a minor issue.

We can always have a PNat.Defs file where we define PNat but do little else, and import this in Algebra.Group.Defs.