norm_num

Stream: mathlib4

[Antoine Chambert-Loir]

In this night's port of docs#RingTheory.Bertrand, one of the issues was that Lean didn't solve by norm_num an inequality of real numbers that only involved natural numbers and standard operations.

import Mathlib.Analysis.SpecialFunctions.Pow.Real
example :  (512 : ℝ) * ((1024 : ℝ) ^ 32) ≤ (4 ^ (512 / 3)) := by sorry

Because of the div, that couldn't be absolutely automatic, but even when the terms involve pow, add and mul, this does not seem to be automatic. Example:

import Mathlib.Analysis.SpecialFunctions.Pow.Real

example : (512 : ℝ) ^ 5 + (6198 : ℝ) ^ ((2 : ℝ ) ^ 3) > (4 : ℝ) * 1024 ^ 6  := by
  simp only [← @Nat.cast_ofNat ℝ]
  simp only [Real.rpow_nat_cast, ← Nat.cast_pow, ← Nat.cast_mul, ← Nat.cast_add]
  simp only [Nat.cast_lt, Nat.cast_le]

[Heather Macbeth]

I think this may be a known issue,
https://github.com/leanprover/lean4/issues/2220
about wrong parsing of powers.

[Heather Macbeth]

Does putting

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

at the beginning of the file change anything?

[Kyle Miller]

It looks like norm_num only handles a ^ b where b : Nat, rather than more generally whenever b is a nat literal. @Mario Carneiro Is this something that could be handled by norm_num itself? Could there be another norm_num extension that applies cast lemmas like Real.rpow_nat_cast to get the pow extension to apply? Or should norm_num rely on using simp lemmas, as Real.rpow_nat_cast is one? (Maybe there should be a norm_num simp set so it doesn't have to rely on whatever the global simp set is?)

Edit: I missed that Real.rpow_nat_cast isn't enough to convert a ^ b with b : Real a nat literal to a ^ b with b : Nat the "same" nat literal. That needs some more norm_num-like power than what simp can do alone.

[Mario Carneiro]

Kyle Miller said:

It looks like norm_num only handles a ^ b where b : Nat, rather than more generally whenever b is a nat literal.

That's a weird sentence, that's not more general, it's a different function

[Mario Carneiro]

norm_num handles the npow function, there is no extension written for the rpow function

[Kyle Miller]

It's HPow.hPow either way, right? There's a norm_num extension right now for the npow instance, and it would handle HPow.hPow more generally if it handled rpow too. I don't mean to suggest it's an oversight in the implementation

[Mario Carneiro]

No, the discrimination tree matches on more than that

[Mario Carneiro]

that extension is specifically about hPow with the npow instance

[Mario Carneiro]

if you put rpow stuff in there it wouldn't be called

[Kyle Miller]

The "it" in "and it would" is referring to norm_num, not the extension

[Mario Carneiro]

I'm saying that there is a missing extension

[Kyle Miller]

"generality" is referring to norm_num too, not a specific extension

[Kyle Miller]

Yes, we are in agreement

[Mario Carneiro]

you wouldn't be able to put the rpow extension in that file anyway

[Mario Carneiro]

because rpow has a ton of requirements

[Kyle Miller]

Couldn't there be some setup where HPow.hPow instances with some cast axioms (wired up using some attribute maybe) could be calculated by an extension in that file?

[Mario Carneiro]

I don't see why that would be desirable

[Mario Carneiro]

rpow has specific theorems for it, in addition to a broader range of valid values that have to be handled

[Mario Carneiro]

it's clearly a new extension

[Kyle Miller]

Even for just the (x : real) ^ (nat literal : real) case?

[Mario Carneiro]

yes

[Mario Carneiro]

if you wanted to have a one liner extension that applies a cast theorem and reduces to the npow case you can do that

[Mario Carneiro]

but the architecture is such that each "pattern" gets its own extension, even if it is a one liner

[Kyle Miller]

I wasn't surprised about needing a new extension for this, it was the "broader range of valid values that have to be handled"

[Kyle Miller]

Anyway, it might be worth making some attribute for cast lemmas that auto-generates a norm-num extension (like when applied to docs4#Real.rpow_nat_cast)

[Mario Carneiro]

perhaps. I just worked with @Heather Macbeth this weekend to do the same thing for positivity. I would rather hold off on doing so for norm_num, at least for this kind of example, both because I am concerned about the performance characteristics and also because this example is not actually suitable for auto-implementation because of the logic around rational powers

[Mario Carneiro]

There are definitely examples where a simple attribute would suffice, but this is not one of them

[Kyle Miller]

Is your concern that norm_num doesn't cache normalized values, so having two extensions will cause re-normalization of operands? Because the performance characteristics of the Real.rpow_nat_cast-based extension seem like they'd otherwise be as good as you'd want for just the natlit-exponent case.

[Mario Carneiro]

having two extensions is just fine, the performance issue is just that the auto-generated extension won't be as good as the hand written one unless the generator is very complex

[Mario Carneiro]

the two extensions aren't both being called on the same thing here

[Mario Carneiro]

the rpow extension is called when the goal is an rpow, and the npow extension is called when it is an npow, and when it is an uninterpreted hPow nothing is called

[Kyle Miller]

The two I was talking about were (x : Real) ^ (ratlit : Real) and (x : Real) ^ (natlit : Real)

[Kyle Miller]

Do you think you can write a norm_num extension for (x : Real) ^ (natlit : Real) that has a meaningful difference in performance characteristics than one that applies Real.rpow_nat_cast and uses the natlit extension? Other than being able to call that extension directly rather than go through another loop of the norm-num algorithm?

[Mario Carneiro]

That would not be two extensions, or at least I don't see why you would do that

[Mario Carneiro]

there would just be one, for (x : Real) ^ (ratlit : Real), possibly written in stages if the rational case isn't too important

[Mario Carneiro]

Do you think you can write a norm_num extension for (x : Real) ^ (natlit : Real) that has a meaningful difference in performance characteristics than one that applies Real.rpow_nat_cast and uses the natlit extension?

Yes, it would not use that theorem, it would dispatch to the same function that the natlit extension uses

[Kyle Miller]

I don't know, this seems like a very acceptable amount of indirection (an extra couple lemmas in the proof term along with a little more overhead looking into the discrimination tree again?), especially if it would give people who aren't norm_num experts the ability to deal with annoying natlit-casting issues. This isn't just about powers either, but rather any sort of polymorphic function that respects numeric coercions.

If they're actually slow enough to be noticable, then experts such as yourself can replace them with something faster as the need arises.

[Mario Carneiro]

maybe. This is a very simple issue though and I'd rather fix the problem in front of me than develop a more complicated solution to address cases which are improperly modeled by this one

[Antoine Chambert-Loir]

For inequalities involving real numbers, how complicated would that be to have Lean compute in floats (with interval arithmetic) and evaluate both terms at a sufficient precision to conclude to inequalities ?

[Johan Commelin]

they have something like that in Coq, and a similar thing in Isabelle. It can certainly be done, but it will require some nontrivial engineering afaik.

[Mario Carneiro]

Even if you do such a computation, the results are not really useful for the actual proof though if you want a proof-producing method because Float is opaque

[Johan Commelin]

Ooh, I thought that Antoine meant "float" instead of Float...

[Eric Wieser]

Mario Carneiro said:

there would just be one, for (x : Real) ^ (ratlit : Real), possibly written in stages if the rational case isn't too important

Did the norm_num extension for rpow (https://github.com/leanprover-community/mathlib/pull/11382) ever get ported?

[Eric Wieser]

(ah, no)