nat.pow is not right-associative

[kbuzzard]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

^ is defined to be left-associative in Lean, breaking with tradition.

Steps to Reproduce

#eval 2^3^2 -- 64

Expected behavior: [What you expect to happen]

result should be 2^(3^2)=2^9=512

Actual behavior: [What actually happens]

get (2^3)^2 = 8^2 = 64.

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

commit 28f4143 (and probably all versions of lean 3)

Additional Information

Exponentiation is traditionally defined to be right associative, because (a^b)^c = a^(b*c) whereas a^(b^c) cannot be simplified in any useful way. Exponentiation is used as the canonical example of a right associative operator in the Wikipedia page on operator associativity. My impression from talking to former devs is that exponentiation is left associative in Lean because of an oversight. I checked that exponentiation was right associative in sage, pari-gp and python and I am fairly confident that it will be right associative in any mainstream language that anyone else cares to check. If changing the associativity of nat.powchanges the behaviour of any code then I suspect there is a fair chance that it changes the code so that it now performs in the way the author was expecting it to perform. I am aware that the devs are probably not currently interested in this sort of bug report but this is something which might want to be dealt with some day (possibly by changing one line of code) so I am recording it here.

[Kha]

Suggestion: Replace with proper typeclass

class has_pow (α : Type u) (β : Type v) :=
(pow : α → β → α)

Perhaps β should be an out_param, at least I can't think of an α that would need two different β not related by coercions.