!4#4085

Stream: mathlib4

[Xavier Roblot]

I am having trouble in Analysis.SpecialFunctions.Pow.Real because of some automatic unwanted coercion. More precisely, once Pow ℝ ℝ has been defined, all the integers exponents are coerced to real exponents, eg.

example (n : ℕ) (x : ℝ) : x ^ (n + 1) = x * x ^ n := pow_succ x n -- succeeds

noncomputable instance : Pow ℝ ℝ := ⟨rpow⟩

example (n : ℕ) (x : ℝ) :  x ^ (n + 1) = x * x ^ n := pow_succ x n -- fails

Indeed, in the second example, the goal is now : x ^ (↑n + 1) = x * x ^ ↑n. Writing x ^ (n : ℕ) does not help, it is still changed automatically to x ^ ↑n. I tried to change the priority of the instance but that did not help either.

[Ruben Van de Velde]

I got the same with complex powers and the only thing I found that worked was using HPow.hPow directly instead of ^

[Ruben Van de Velde]

I didn't look hard, though

[Heather Macbeth]

What about with integer powers of integers? Same issue?

[Ruben Van de Velde]

One thing I thought of but didn't try was replacing the Pow instance by a HPow instance

[Xavier Roblot]

Heather Macbeth said:

What about with integer powers of integers? Same issue?

No, that still works

[Xavier Roblot]

Ruben Van de Velde said:

One thing I thought of but didn't try was replacing the Pow instance by a HPow instance

You mean this

noncomputable instance : HPow ℝ ℝ ℝ := ⟨rpow⟩

I doesn't solve anything. I have the same issue after the change.

[Kevin Buzzard]

Does x ^ (n + 1 : \N) work? This is pretty horrible. Why would lean coerce to reals without looking for an instance for naturals first?

[Xavier Roblot]

Kevin Buzzard said:

Does x ^ (n + 1 : \N) work?

No. For

example (n : ℕ) (x : ℝ) :  x ^ (n + 1 : ℕ) = x * x ^ (n : ℕ) :=

I still get x ^ ↑(n + 1) = x * x ^ ↑n as goal.

[Heather Macbeth]

Xavier Roblot said:

Heather Macbeth said:

What about with integer powers of integers? Same issue?

No, that still works

I guess actually there's no confusion here, integer powers require a group-with-zero, which the integers aren't.

[Johan Commelin]

Shouldn't they only require a div_inv_monoid or something like that?

[Johan Commelin]

Still ℤ is not an instance of that, of course

[Heather Macbeth]

This is Xavier's problem, right?

axiom A : Type

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

variable (a : A)


instance : HPow A Nat A := sorry

set_option pp.all true

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

instance : HPow A A A := sorry

#check a ^ 4
-- @HPow.hPow.{0, 0, 0} A A A instHPowA a (@OfNat.ofNat.{0} A 4 (instOfNatA 4)) : A

[Ruben Van de Velde]

Xavier Roblot said:

Ruben Van de Velde said:

One thing I thought of but didn't try was replacing the Pow instance by a HPow instance

You mean this

noncomputable instance : HPow ℝ ℝ ℝ := ⟨rpow⟩

I doesn't solve anything. I have the same issue after the change.

Too bad

[Kevin Buzzard]

This should probably move to #lean4

[Xavier Roblot]

Kevin Buzzard said:

This should probably move to #lean4

Should I post a copy of my original message there? It is probably better if @Heather Macbeth posts her #mwe

[Floris van Doorn]

Note that in @Heather Macbeth's mwe the expression #check a ^ (4 : Nat) uses the intended instance, so it doesn't capture the exact behavior in the wild.

[Floris van Doorn]

This captures the full problem:

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 (priority := 10) : 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

[Floris van Doorn]

I think I know what's going on. The notation ^ is declared as

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

where binop% is a special elaborator that elaborates binary operations, and can insert casts to either argument. Removing this elaborator fixes this issue.

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

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

#check a ^ 4 -- Nat instance

instance : HPow ℝ ℝ ℝ := sorry

#check a ^ 4 -- Nat instance
#check a ^ (4 : Nat) -- Nat instance
#check a ^ (4 : Real) -- Real instance

[Floris van Doorn]

However, using that macro globally doesn't work, since we need some of the functionality of binop% in other places. So a full fix is nontrivial, and might require defining a variant of binop%.
As a workaround, you can add the following line on top of file/section that experiences this issue:

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

[Floris van Doorn]

Here is a regression that you would have with this local macro rule:

import Std.Classes.Cast

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.notation false
set_option pp.explicit true

section default

#check a ^ 4 -- Real ^ Nat instance

local instance : HPow ℝ ℝ ℝ := sorry

#check a ^ 4 -- Real ^ Real instance
#check a ^ (4 : Nat) -- Real ^ Real instance
#check a ^ (4 : Real) -- Real ^ Real instance
example (n : Nat) := ∃ k, n = 2 ^ k -- Nat ^ Nat instance

end default

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

#check a ^ 4 -- Real ^ Nat instance

local instance : HPow ℝ ℝ ℝ := sorry

#check a ^ 4 -- Real ^ Nat instance
#check a ^ (4 : Nat) -- Real ^ Nat instance
#check a ^ (4 : Real) -- Real ^ Real instance

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

[Floris van Doorn]

I opened lean4#2220 to record this issue.

[Xavier Roblot]

Floris van Doorn said:

However, using that macro globally doesn't work, since we need some of the functionality of binop% in other places. So a full fix is nontrivial, and might require defining a variant of binop%.
As a workaround, you can add the following line on top of file/section that experiences this issue:

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

Thanks, that helps a lot!

[Eric Wieser]

Presumably binop% has a preference for A -> A -> A, and so we want a custom elaborator with a preference for A -> B -> A (for pow) and A -> B -> B (for smul)

[Xavier Roblot]

The only problems left in this file are for the Tactics section. I see that in the already ported Analysis.SpecialFunctions.Pow.Complex, the whole section Tactics has been commented out. Is it okay to do the same for this file?

[Heather Macbeth]

Ruben Van de Velde said:

I got the same with complex powers and the only thing I found that worked was using HPow.hPow directly instead of ^

Do we need to adjust the previous file on complex powers to use Floris' workaround, too?

[Scott Morrison]

@Xavier Roblot, yes, you can just drop the tactics section while porting the theory.

[Eric Wieser]

Don't drop it without a porting note naming the tactic that was removed!

[Floris van Doorn]

Heather Macbeth said:

Do we need to adjust the previous file on complex powers to use Floris' workaround, too?

I tried one file (I forgot which one) by doing the local macro_rules for the whole file, but that resulted in a few new elaboration errors, so it might not be worth it until we get a proper fix.

[Gabriel Ebner]

The elaboration error you've mentioned on the bugtracker is fixed by importing Mathlib.Algebra.Group.Defs

[Floris van Doorn]

Oh, neat!

I looked through some other files that now use Pow workarounds, and there are a few other errors I get, but maybe we can also solve that with some default instance. Below is an example (I import a lot to show that in actual mathlib it's failing - it is likely reproducible with very few imports).

import Mathlib.Analysis.SpecialFunctions.Pow.Real

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)
example {x : ℂ} {a : ℂ} : 0 ^ x = a := sorry
-- failed to synthesize instance HPow ℕ ℂ ?m.1970

example {x : ℝ} (y : ℂ) : abs (x ^ y) = x ^ y.re := sorry
-- failed to synthesize instance HPow ℝ ℂ ?m.2123

[Floris van Doorn]

All errors I saw from the local macro_rules where cases where the return type / codomain of the power function was a metavariable, and these two examples are (I think) representative. The first one might be a bit harder since the numeral has unspecified type (which should be ℂ, not the ℕ in the error message).

[Floris van Doorn]

I would have guessed that docs4#instHPow being a default instance would be enough to elaborate the second example.

[Floris van Doorn]

Another minor issue is that if we change this in core, we also need to fix core (the n = 2 ^ k error in the issue was the first error on a branch where I tried to change the macro).

[Jon Eugster]

Floris van Doorn said:

As a workaround, you can add the following line on top of file/section that experiences this issue:

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

I added a comment about this temporary workaround in the port wiki as it came up again in !4#4331

[David Renshaw]

I just ran into this problem too: https://github.com/dwrensha/math-puzzles-in-lean4/commit/07cb970e06f60cd37990f478168cfa919f317be6
Thanks for posting a workaround.