Monoid power instead of nat power

Stream: new members

[Ben Nale]

How do I use monoid.has_pow instead of nat.has_pow ?
When I use ^ it defaults to nat.has_pow but I want monoid.has_pow,

[Kevin Buzzard]

Here's a better question. How do we solve this problem once and for all? I am unclear about the best way forward -- this issue comes up again and again (came up on the discord last week, came up bigtime at LFTCM). If we redefine monoid.pow so that the step case is the same way around as nat.pow will that solve it? I tried editing nat.pow and then I realised I was editing core Lean :-/ Can we have some proposed solutions as to how to proceed?

@Ben Nale you can just use monoid.pow explicitly instead of the ^ notation. Or use ^ but then apply some pow_eq_pow lemma which says that nat.pow a b = monoid.pow a b

[Mario Carneiro]

delete nat.has_pow

[Mario Carneiro]

the version in core can be called nat.pow with no notation, and you use that when you care about efficiency, otherwise monoid.pow will put a generic instance on it

[Mario Carneiro]

and eventually maybe we can find a way to get the VM to produce good code even for abstract implementations like monoid.pow on nat

[Kevin Buzzard]

I am unclear how to delete nat.has_pow because this is in core. Do I just delete it, fix core, then wait until a new lean release and then observe that mathlib is broken? I am just unsure of the workflow here.

[Bryan Gin-ge Chen]

@Chris Hughes has an old PR lean#128 which attempts to delete nat.has_pow from core. I'm not sure whether with all the changes it's better to work off that or start from scratch.

[Mario Carneiro]

I believe the pattern has been to make a PR to core (which involves fixing everything in core, probably not much), and then making fixes to mathlib in the feature branch for the upcoming version of lean

[Reid Barton]

I'm currently trying my hand at fixing this... wish me luck.

[Reid Barton]

I learned that if you break norm_num and ring you get a lot of scary errors

[Mario Carneiro]

Oh, is this something that should be addressed?

[Johan Commelin]

@Reid Barton Thanks so much. It was floating to the top of my todo list... I'm happy to skip it (-;

[Kevin Buzzard]

I tried this job once and borked my Lean installation :laughing: