elaboration of ^ shouldn't try to put the arguments in the same type

[fpvandoorn]

Description

The macro for the ^ notation for exponentiation is defined as

macro_rules | `($x ^ $y)   => `(binop% HPow.hPow $x $y)

However, the binop% elaborator tries to make the type of x and y the same, which is not desired for exponentiation.

MWE

class NatCast (R : Type u) where
  natCast : Nat → R

instance [NatCast R] : CoeTail Nat R where coe := NatCast.natCast
instance [NatCast R] : CoeHTCT Nat R where coe := NatCast.natCast

axiom Real : Type
notation "ℝ" => Real

instance (n : Nat) : OfNat ℝ n := sorry

variable (a : ℝ)

instance natCast : NatCast ℝ where natCast n := sorry
instance : HPow ℝ Nat ℝ := sorry

set_option pp.all true


#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Nat Real instHPowRealNat a (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) : Real

instance : HPow ℝ ℝ ℝ := sorry

#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@OfNat.ofNat.{0} Real 4 (instOfNatReal 4)) : Real

#check a ^ (4 : Nat)
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@NatCast.natCast.{0} Real natCast (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4))) : Real

The desired result is that all checks use the instHPowRealNat instance, i.e. that 4 is interpreted as a Nat.

Additional Notes

Just removing binop% and replacing the macro with the following fixes the current issue, but it causes problems in other elaboration problems.

macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

With this macro an example like the following fails.

example (n : Nat) := ∃ k, n = 2 ^ k -- fails to find any instance, needs to know the type of `k`

Zulip Discussion

link

[gebner]

The idea is to have a default instance for Pow here:

macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

class Semiring (R : Type) extends Pow R Nat
instance : Semiring Nat where
@[default_instance high] instance [Semiring R] : Pow R Nat := inferInstance

example (n : Nat) := ∃ k, n = 2 ^ k -- works fine

(We have that instance in Mathlib/Algebra/Group/Defs.lean btw.)

[kmill]

@gebner A design I've been thinking about that would help with HPow and other sorts of functions that are more actions than operators would be to have a couple additional term elaborators that participate in the "binop%" algorithm. I don't think we actually want the algorithm to ignore both the arguments to HPow, but rather it should descend into the base of the exponent (and similarly in mathlib, we want it to descend into the second argument of SMul). In both cases, the acted-upon argument should have a type that's compatible with the whole arithmetic expression.

Here's a simple proposal for how to handle this: add actionop1% and actionop2% term elaborators with the syntax actionop1% f lhs rhs and actionop2% f lhs rhs such that they behave like unop% (fun x => f x rhs) lhs and unop% (fun x => f lhs x) rhs repsecitively. Then we would have

macro_rules | `($x ^ $y)   => `(actionop1% HPow.hPow $x $y)

The effect is that x would still be coerced to the common type that the elaborator solves for, but y will be left untouched, letting it remain a Nat for example even in a Real expression.

Another design would be to adjust unop% to allow these lambdas and to do beta-reduced application. Then we'd have

macro_rules | `($x ^ $y)   => `(unop% (fun x' => HPow.hPow x' $y) $x)

[kmill]

I have a prototype of my suggestion at https://gist.github.com/kmill/bc58941368cc60738f3c932fe2546c9d

With it, we can see the following behavior:

import Mathlib.binop2
import Mathlib.Data.Real.Basic

#check (3 : ℝ) ^ 2
-- 3 is real
-- 2 is a nat

#check (1 : ℝ) + 3 ^ 2
-- 1 is real
-- 3 is real
-- 2 is a nat

#check (1 + 3 ^ 2 : ℝ)
-- 1 is real
-- 3 is real
-- 2 is a nat

In particular, exponentiation is modeled as a right action, and only the LHS participates in the coercion protocol.

Some more examples with Mathlib's left action notation:

import Mathlib.binop2
import Mathlib.Algebra.Algebra.Basic

macro_rules | `($x • $y)   => `(leftact% HSMul.hSMul $x $y)

#check (1 • 2 : ℝ)
-- 1 is a nat
-- 2 is real

variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)

#check m + r • n
-- m + r • ↑n : M

We'll see how it works in practice in some mathlib files, and then if it seems good I'll create a PR. I think it only involves adding about 15 lines.

[kbuzzard]

An undergraduate just ran into this issue: they had a working file, and then added an import (which gave an instance of (z : \C)^(y : \C)), and a simp only call which was closing a goal stopped working. I told them to add local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) to the top of their file; this fixed it.

import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.Data.Complex.Basic
-- uncomment this import to break the proof
--import Mathlib.Analysis.SpecialFunctions.Pow.Complex

-- uncomment this hack to fix it again
--local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

example (q : ℕ+) : ζ ∈ rootsOfUnity q ℂ ↔ ((ζ : ℂˣ) : ℂ) ^ ((q : ℕ+) : ℕ) = 1 := by
  simp only [mem_rootsOfUnity']
  done

[b-mehta]

The solution of adding local macro_rules | ($x ^ $y) => (HPow.hPow $x $y) can change elaboration in weird ways however, see for instance

import Mathlib.Analysis.SpecialFunctions.Pow.Real

-- local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

lemma foo (t : ℝ) (ht : 3 ≤ t) : 12 * t + 1 ≤ 13 * t ^ 2 := sorry

in which uncommenting the macro changes the elaboration of 12 (and in my case also broke a proof)

[kmill]

leanprover-community/mathlib4#6852 has a large-scale experiment with my modifications to the binop% elaborator. It switches to marking HPow as a right action and mathlib's HSMul as a left action. It took some tweaking of type ascriptions, but overall it seems to be an improvement (it seems you can usually just delete the local macro_rules fixes!)

In Bhavik's example, the conclusion elaborates as (12 : ℝ) * t + (1 : ℝ) ≤ (13 : ℝ) * t ^ (2 : ℕ). (To be clear, as OfNat literals, not as coerced literals.)