syntax for powers?

Stream: mathlib4

[David Loeffler]

In porting Analysis.SpecialFunctions.Gaussian, I came across a proof which was mysteriously failing to work, involving an expression containing x ^ 2 for a real variable x .

The problem seems to be that mathlib3 read this as an instance of pow : ℝ × ℕ → ℝ while mathlib4 seems to prefer to interpret the 2 as a real number and use rpow : ℝ × ℝ → ℝ. This can be fixed using rw [← Nat.cast_two, rpow_nat_cast] but that adds an annoying extra step (which is going to occur over and over again in this file since it's all about integration of exp (-x ^ 2)).

Is there some syntax I can use to force it to interpret x ^ 2 as a natural-number power rather than a real power?

[Ruben Van de Velde]

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220

directly under the module documentation comment

[David Loeffler]

Ruben Van de Velde said:

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220

directly under the module documentation comment

Excellent, I had a feeling this must have come up before, thanks!

[Ruben Van de Velde]

This may cause another issue where numerals like 1 are treated as ((1 : Nat) : Real) (with an explicit cast) rather than (1 : Real), but you can work around that by writing (1 : Real) explicitly

[Patrick Massot]

What is the current status of this issue? Is there an actual fix coming?

[Kevin Buzzard]

lean4#2220

[Kyle Miller]

I've got a prototype fix, in case anyone wants to experiment and report back: https://gist.github.com/kmill/bc58941368cc60738f3c932fe2546c9d

This is how it performs on some simple tests:

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

This can also support smul, but I didn't write a macro for it.

[Kyle Miller]

If it seems good, I can create a Lean 4 PR

[Eric Wieser]

Supporting smul would be handy too: we have a lot of silly annotations where lean can't work out that r \smul m is of type M when m : M

[Eric Wieser]

I assume

a) Given `n : Nat` and `i : Nat`, it can successfully elaborate `n + i` and `i + n`. Recall that Lean 3
   fails on the former.

is a typo

[Eric Wieser]

I don't remember Lean3 having any trouble adding two natural numbers

[Kevin Buzzard]

My guess is that it should say i : Int :-) (note one of the benefits of not calling all your types alpha, beta, gamma and all your terms a,b,c ;-) )

[Kyle Miller]

@Eric Wieser More examples:

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

[Oliver Nash]

I lost quite some time to this earlier today. The example I encountered was:

import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.SpecialFunctions.Pow.Real

-- The below `by simp` succeeds only if the import defining `Real.rpow`
-- is commented out (as shown above).
example : deriv (fun x : ℝ ↦ x ^ 3) 1 = 3 := by simp

-- This always works.
example : deriv (fun x : ℝ ↦ HPow.hPow x (3 : ℕ)) 1 = 3 := by simp

[Oliver Nash]

I find it unsettling that meaning of statements are sensitive to the imports in this way!

[Johan Commelin]

Yeah, this macro_rules saga is far from over...

[Oliver Nash]

OTOH I was very happy when I discovered Ruben's one-line patch:

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

[Ruben Van de Velde]

I can only claim credit for copy/pasting it into Zulip :)

[Notification Bot]

3 messages were moved from this topic to #mathlib4 > addressing lean4#2220 (HPow elaboration) by Kyle Miller.