Real^Nat should not be interpreted as Real^Real

Stream: mathlib4

[Yongyi Chen]

Minimal working example:

#check (2 : ℝ) ^ 2
#check (2 : ℂ) ^ 2

Hover over the 2 in the exponent in each line, and observe that the types are ℝ and ℂ respectively. The expected types are ℕ and ℕ. A practical example where this causes an issue is the following, taken from Lean for the Curious Mathematician:

-- This does not work.
example {x y z w : ℂ} (h₁ : x * z = y^2) (h₂ : y * w = z^2) : z * (x * w - y * z) = 0 := by
  polyrith  -- polyrith failed to retrieve a solution from Sage! ValueError: polynomial is not in the ideal

-- This works.
example {x y z w : ℂ} (h₁ : x * z = y^2) (h₂ : y * w = z^2) : z * (x * w - y * z) = 0 := by
  norm_cast at h₁ h₂
  polyrith  -- Try this: linear_combination w * h₁ + y * h₂

[Kyle Miller]

This is a known issue: lean4#2220

There is a mathlib override in the WIP branch mathlib4#6852. If you import the Mathlib/binop2.lean file you'll get Real^Nat rather than Real^Real.

[Kyle Miller]

There's also a local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) workaround you can see in current mathlib, but this completely turns off the coercion propagation features for ^ notation and can lead to unexpected results.

[Yongyi Chen]

OK, good to know!