Neg ℕ when looking for zpow

Stream: mathlib4

[Thomas Murrills]

I noticed the following:

import Mathlib.Data.Rat.Basic

example (x y : ℚ) : x ^ (-1) = y := sorry
  -- failed to synthesize instance Neg ℕ

We instead have to write x ^ (-1 : ℤ). I would think Lean ought to be able to infer we were using zpow. Is there a reason it can't? Could we change that somehow?

[Eric Wieser]

This feels like something a unification hint might be able to deal with, assuming those still exist

[Ruben Van de Velde]

Could it be

example (x y : ℚ) : (x : ℝ) ^ (-1 : ℝ) = y := sorry

instead? :)

[Thomas Murrills]

Okay okay, hear me out…………HNeg

[Thomas Murrills]

Seems like we can at least make the literal case a little nicer by adding e.g.

macro_rules | `(- $x:num) => `(unop% Neg.neg ($x : Int))

somewhere! (Don't actually know what that unop% is doing, it's just copypasta) Maybe a unification hint would be a better solution, but I don't know how those work yet.

It would be nice to be able to write -y and get an Int when y is a Nat in general, though—I don't know if that's something unification hints are capable of, and I'm worried it might be a bad idea performance-wise to infer the type of y and match it against Nat within a macro.

(I also think I remember it being said somewhere that often unification hints are almost never the best/most robust solution to a problem? But I'm not sure what is, here.)

[Eric Wieser]

Won't your code do the wrong thing for (-1 : Rat)?

[Thomas Murrills]

I tried it, and apparently not? I’m guessing it turns it into (-(1 : Int) : Rat). But that’s still not great. Oops, had a simp. Yeah, that's not good. I suppose it should be simply something like

macro_rules | `($b ^ (- $x:num)) => `($b ^ (- ($x : ℤ)))

if this is the way we'd want to go. Seems a bit fragile and restricted to me, though. I'd rather a more general/robust solution...

[Eric Wieser]

Does that do the wrong thing for x ^ (-1 : Real) where x : Real?

[Eric Wieser]

We probably don't have the rpow instance yet in mathlib4....

[Thomas Murrills]

I'd hope not, given that x ^ (-1 : Real) doesn't match the pattern...but if there are macros that eliminate the type ascription syntactically, then it would match