HomogeneousPow instances in mathlib

Stream: mathlib4

[Edward van de Meent]

in discord, a question came up about tetration, where the OP defined it as follows:

def tetration {α : Type u_1} [HomogeneousPow α] [One α] (x : α) (n : ℕ) : α :=
  match x, n with
  |x, 0 => 1
  |x, Nat.succ n => x ^ (tetration x n)

although the definition compiles, it is not useful at all, since the only instance for docs#HomogeneousPow is for Float, rather than also for Nat, Real, and maybe Complex. do we want to have these instances? or maybe should we prefer to have HomogeneousPow α reduce to Pow α α or something like that?

[Edward van de Meent]

small bits of context: right now, docs#HPow , docs#Pow and docs#HomogeneousPow are all separate one-field classes (yes, they don't extend eachother) and have instances in the sensible direction, but there are no instances or anything to turn HPow a b a into Pow a b or Pow a a into HomogeneousPow a

[Eric Wieser]

I think this might just be a notation implementation detail (cc @Kyle Miller), and for the definition above you should just use Pow α α

[Edward van de Meent]

as far as i can tell, HPow is the only notation class among them, since b ^ a means HPow.hpow b a

[Eric Wieser]

Right, but I think this plays a part in the custom elaborator that implements that notation

[Edward van de Meent]

you mean the rightact% elaborator?

[Edward van de Meent]

i can't seem to find source code for that elaborator, is it built in? found it

[Edward van de Meent]

as far as i can tell, there is no mention of Pow or HomogeneousPow there...

[Eric Wieser]

lean4#2854 has some context

[Edward van de Meent]

so, if i'm reading this right, you're correct in saying that HomogeneousPow (and as it turns out NatPow as well) are implementation details...

Both NatPow and HomogeneousPow provide a default Pow instance, and types can choose to implement an instance for one of these two depending on whether they would prefer the exponent to default to being a Nat or to the base's type

[Edward van de Meent]

i suppose it would be useful if these get marked as such? they are, but apparently not clearly enough

[Edward van de Meent]

would the docs be improved if it were to explicitly say "this class should not be used as an argument"?

[Eric Wieser]

I think "prefer writing [Pow A A] to [HomogeneousPow A] in argument lists" would be clearer

[Kyle Miller]

It should be HPow in argument lists, since HPow does not provide Pow instances.

[Kyle Miller]

I would not say NatPow or HomogeneousPow are implementation details — they're intended to be used by users to specify how the exponentiation should elaborate by default.

[Edward van de Meent]

Is there a reason to distinguish between Pow A B and HPow A B A?

[Kyle Miller]

In what sense?

[Kyle Miller]

For writing instances? Probably not. For argument lists? Yes, because HPow does not provide Pow instances.

[Edward van de Meent]

From a design POV, what is wrong with having abbrev Pow (A : Type*) (B : Type*) := HPow A B A?