Non-associative powers

Stream: mathlib4

[Christopher Hoskin]

I'm trying to make powers work for non-associative algebras by moving nsmul, nsmul_zero and nsmul_succ from Monoid into MulOneClass. I've solved a lot of issues, but I'm stuck: on this one:

[1131/1819] Building Mathlib.Algebra.FreeMonoid.Count
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/mans0954/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/Algebra/FreeMonoid/Count.lean -R ././. -o ./.lake/build/lib/Mathlib/Algebra/FreeMonoid/Count.olean -i ./.lake/build/lib/Mathlib/Algebra/FreeMonoid/Count.ilean -c ./.lake/build/ir/Mathlib/Algebra/FreeMonoid/Count.c
error: stdout:
./././Mathlib/Algebra/FreeMonoid/Count.lean:58:4: error: type mismatch
  AddMonoidHom.toMultiplicative (FreeAddMonoid.countP p)
has type
  @MonoidHom (Multiplicative (FreeAddMonoid α)) (Multiplicative ℕ) Multiplicative.mulOneClass
    Multiplicative.mulOneClass : Type u_1
but is expected to have type
  @MonoidHom (FreeMonoid α) (Multiplicative ℕ) Monoid.toMulOneClass Multiplicative.mulOneClass : Type u_1

Anyone able to give me a hint please?

PR here: https://github.com/leanprover-community/mathlib4/pull/12281

Not clear to me that I can pull out a MWE from a refactor like this.

Thanks.

Christopher

[Richard Copley]

Won't you need to assume power associativity?

[Kevin Buzzard]

I guess strictly speaking the answer to that is "no", as the definition will go through fine! Indeed both definitions will, and will give different answers in general :-)

[Richard Copley]

Hmm. Right, x^3 will mean either x^2*x or x*x^2, and it won't necessarily follow that those are equal.

[Christopher Hoskin]

Yes, without associativity, power associativity isn't automatic, but it does hold for some special cases (e.g. Jordan algebras).

For the opposite algebra, I have stuck with the default nsmul rather than try to define the opposite one. https://github.com/leanprover-community/mathlib4/pull/12281/files#diff-ac8c71e48327ed7815458d03a7b509e49fc7262daa8cc61f2206d0c6fda599bfL127 This then means that some previously rfl results now require inductive proofs https://github.com/leanprover-community/mathlib4/pull/12281/files#diff-ac8c71e48327ed7815458d03a7b509e49fc7262daa8cc61f2206d0c6fda599bfR190

[Yaël Dillies]

I don't think changing docs#MulOneClass is the right way to go

[Yaël Dillies]

cc @Scott Carnahan who did something similar in spirit with docs#PNatPowAssoc

[Jireh Loreaux]

Ack, we really need some forgetful inheritance here, or else I fear we're going to end up in an untenable situation.

[Scott Carnahan]

I'm afraid I don't have any particularly helpful advice, but I like the fact that you are trying this generalization.

One unsatisfying point I encountered when writing docs#PNatPowAssoc was the lack of PNat power structure in semigroups. This meant I couldn't easily write a PNatPowAssoc instance for semigroups (and hence nonunital rings). I had thought about changing Mul to incorporate a pnpowRec function, but was daunted by the vastness of the potential refactor. See this earlier discussion.

[Jireh Loreaux]

I'm really busy with some other things, but if I get a chance I'll try to revive my work on adding a ppow field for forgetful inheritance in the algebraic hierarchy. It's not actually as much work as you might expect if you just let it use the default values everywhere. If it goes well, I'll see about factoring both that and the standard Pow instance on monoids out.

[Jireh Loreaux]

Yaël Dillies said:

I don't think changing docs#MulOneClass is the right way to go

@Yaël Dillies can you explain why you think we should avoid forgetful inheritance here? It doesn't make any sense to me.

[Christopher Hoskin]

Thanks. I realised that the approach I was trying wouldn't solve the problem of powers in non-unital algebras, which I'd also like to have. But I was hoping it might be an achievable interim step that would let me get a bit further with non-associative algebras.

[Yaël Dillies]

Jireh Loreaux said:

can you explain why you think we should avoid forgetful inheritance here?

I'm not saying we should avoid forgetful inheritance. I'm saying that MulOneClass is probably not the right class to go for to mean "power associative multiplication". But also I don't know how much MulOneClass is used (it's one of those typeclasses I don't understand the use of), so maybe you could recycle it to mean "power associative multiplication", assuming you rename it to something more mathematically accurate.

[Christopher Hoskin]

Yaël Dillies said:

I'm not saying we should avoid forgetful inheritance. I'm saying that MulOneClass is probably not the right class to go for to mean "power associative multiplication". But also I don't know how much MulOneClass is used (it's one of those typeclasses I don't understand the use of), so maybe you could recycle it to mean "power associative multiplication", assuming you rename it to something more mathematically accurate.

I did wonder about inserting a class in between MulOneClass and Monoid but that doesn't necessarily help with NonAssocSemiring which extends MulZeroOneClass rather than MulOneClass directly. Would having a mixin class which just contained nsmul, nsmul_zero and nsmul_succ help?

[Yaël Dillies]

Christopher Hoskin said:

I did wonder about inserting a class in between MulOneClass and Monoid but that doesn't necessarily help with NonAssocSemiring which extends MulZeroOneClass rather than MulOneClass directly

You know you are allowed to change the extends clauses, right?

[Yaël Dillies]

It's not because structures are extended in a certain way in mathlib that the algebraic hierarchy is immutable

[Yaël Dillies]

Here you could just replace

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

with

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α, PowAssocClass α

or something like that

[Kevin Buzzard]

Yaël Dillies said:

You know you are allowed to change the extends clauses, right?

I'm not sure that you're allowed to change the first one -- this is the "preferred parent" right?

[Christopher Hoskin]

From https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/PNat.20powers.20in.20a.20semigroup/near/404727588 :

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.

I was curious, so I had a go at merging recent HEAD of master into this branch.

With a few tweaks I was able to get it to build (except for linting): https://github.com/leanprover-community/mathlib4/pull/12355

The tweaks and fudges included:

• (Add)CommSemigroup.ext was defined in two places, so I commented one out
• Some lemmas like ppow_add appear in two places - I've masked this by putting one set in the Mul namespace for now
• An instance in AlgebraicGeometry/Properties needed a few more heartbeats
• I added the hypothesis [FunLike F M N] to map_ppow

[Jireh Loreaux]

Omg that diff +541,230 -284,439 :rolling_on_the_floor_laughing: (it's not a diff against master)

[Jireh Loreaux]

Thanks for doing this by the way!

[Jireh Loreaux]

I've just hit !bench

[Eric Wieser]

I think that diff has a git screwup in it

[Jireh Loreaux]

No, it's on purpose, it's merging into my branch, that's why

[Jireh Loreaux]

I guess we've added a quarter million lines of code in the past 9 months or so though?

[Yaël Dillies]

Sounds about right, but we can't actually know since Github gives up on line counts in repos with more than 10000 commits

[Floris van Doorn]

https://leanprover-community.github.io/mathlib_stats.html gives ~200k net lines added since July last year.

[Jireh Loreaux]

@Christopher Hoskin I just checked the diff of that branch against current master, and it was pretty reasonable. There were a few heartbeat bumps I had added months ago when I was trying to get it to work. I was able to remove all of those without issue, so the only bump is to that decl in algebraic geometry. I also tried to address the linting issues, and I've push these changes to that branch. I'm happy for you to merge this into my branch if you want.

[Jireh Loreaux]

Ultimately, if people are happy with this idea / approach, then I think the right approach is to not merge this, but start a new branch with an intermediate PPowAssoc class in between Mul and Semigroup and an intermediate PowAssoc class in between MulOneClass and Monoid.

Then, hopefully that version will have the same success. :fingers_crossed:

[Christopher Hoskin]

Thanks! I've merged my branch into yours. I hope I haven't distracted you too much. I probably should be doing other things...

[Jireh Loreaux]

No, honestly I really appreciate your taking the time to do this. It's something I've meant to get back to and have just never had the impetus to do it. It would be very satisfying to finally be able to talk about PNat powers appropriately.