norm_num for real exponentiation

Stream: general

[Bolton Bailey]

I came across the following goal

lemma simple_real_power_goal : (2 : ℝ) ^ (2 : ℝ) = (4 : ℝ) :=
begin
  norm_num, --norm_num failed to simplify
end

The documentation of norm_num sort of suggests it should solve this, but I'm not really surprised it fails. What is the canonical way to solve an goal like this?

[Heather Macbeth]

If you use docs#real.rpow_nat_cast to convert it to (2 : ℝ) ^ (2 : ℕ), then norm_num will probably be able to do it.

[Bolton Bailey]

Not quite sure how to use rpow_nat_cast here

[Patrick Stevens]

Yeah, that's the workaround I've been using - but real arithmetic is surprisingly painful, I don't know if It Is Generally Known how painful it is or if I'm doing it wrong

[Patrick Stevens]

Let me find the right line

[Patrick Stevens]

See https://github.com/leanprover-community/mathlib/pull/8002/files#diff-779714ecbcf3ae1ddff8a35448792a63daacd8e7c2b942aa723c2c19b65ec2ddR407, for example

[Patrick Stevens]

Actually a much more clear example: https://github.com/leanprover-community/mathlib/pull/8002/files#diff-779714ecbcf3ae1ddff8a35448792a63daacd8e7c2b942aa723c2c19b65ec2ddR590

[Patrick Stevens]

(I must apologise that I told you I had stopped working on #8002 and then promptly closed a couple more sorries - I really have stopped working on it for the next few days now)

[Heather Macbeth]

@Patrick Stevens In what contexts do you really need to use real exponentiation? Can you try to stick to nat exponentiation?

[Bolton Bailey]

The occurrence of ((3 : ℕ) : ℝ) is pretty funny in that file.

We are currently dealing with real exponentiation in the context of #8002 (Bertrand's postulate). We were going on a purely nat-based version for a while, but it just seems less easy without calculus, so we converted to reals and that's how we ended up here.

[Patrick Stevens]

Yeah, there's a fair bit of dodging between x * log y and log (y ^ x), which needs to go via the reals (edit: or does it? maybe not!) - it's possible that we can rephrase to avoid using the reals quite so often, but it's not obvious to me how

[Yaël Dillies]

Unrelated but I noticed you're using finset.Ico bla (blabla + 1). I must tell you that #7987 will (hopefully) soon go through which means you'll be allowed to use finset.Icc bla blabla directly.

[Patrick Stevens]

I guess it's worth us stepping back and looking over the entire PR - I've proved a couple of things which don't seem to be in mathlib yet but which are absolutely going to be useful for anyone doing arithmetic ((nat.sqrt a : ℝ) ≤ real.sqrt a, sqrt x / x = 1 / sqrt x, lemma log_eq_zero {x : ℝ} (hyp : log x = 0) : x = 0 ∨ x = 1 ∨ x = -1, lemma zero_pow_complex {a : ℂ} {x : ℂ} (hyp : 0 ^ x = a) : a = 0 ∨ (x = 0 ∧ a = 1)) but there's probably some structural changes we can do

[Patrick Stevens]

And in particular, we should absolutely see if lemma log_pow {x y : ℝ} (hyp : 0 < x) : log (x ^ y) = y * log x := has an equivalent with y : nat already in mathlib, and add it if not, and try to pivot the proof to use that new lemma instead

[Yaël Dillies]

log_eq_zero can be rewritten as an equivalence. I don't think that's the case here but sometimes I miss a lemma in mathlib because I was looking for a not general enough version.

[Yaël Dillies]

Let me find that log_pow variant. I used recently.

[Patrick Stevens]

Yeah, that was just my first get-something-working; when this PR is more ready to merge, I'll be pulling those functions into separate PRs and at that point we'll rewrite them into the fully general form and tag them with simp and so on

[Yaël Dillies]

Okay, seems like I used real.rpow_nat_castcombined with real.log_rpow, just as Heather proposes.

[Bolton Bailey]

Is there any way here to additionally cast the base to a natural? I'm trying to solve
(584 : ℝ) ^ 100 * (25000 : ℝ) ^ 637 ≤ (67957 : ℝ) ^ 637
But even norm_num doesn't work here because it times out.

[Damiano Testa]

I am not sure if this is what you are looking for, but maybe it is relevant:

import analysis.special_functions.pow

open real
lemma pow_coe (a b : ℕ) : (↑(a ^ b) : ℝ) = (↑a) ^ (↑b : ℝ) :=
by simp only [rpow_nat_cast, nat.cast_pow]

lemma pow_real (a b : ℕ) : (a : ℝ) ^ (b : ℝ) = ((id (a ^ b) : ℕ) : ℝ) :=
by simp only [real.rpow_nat_cast a b, id.def, nat.cast_pow]

[Damiano Testa]

To be honest, I do not know how to get rid of the spurious id, but, without it, I do not think that you get the right coercions.

[Mario Carneiro]

I think the problem here is that 67957 ^ 637 is huge. You should find another way to prove this

[Mario Carneiro]

norm_num can do calculations of real ^ nat as easily as nat ^ nat, but those numbers are just too big for lean

[Eric Rodriguez]

can norm_num do decent estimates of real logs?

[Mario Carneiro]

if you do the right calculations, sure

[Mario Carneiro]

it's not automatic, but there are several norm_num based approximation proofs in mathlib, including one for log 2 that you can probably use as inspiration

[Mario Carneiro]

also, if this trying to prove bertrand's postulate, it is being waay overcomplicated. I've already posted earlier about how you can do it without calculating any numbers bigger than 64

[Bolton Bailey]

Well, when I call #eval 67957^637 it works fine, so that indicates to me that if I can just convert it so nats, it would work.

[Mario Carneiro]

#eval doesn't do proofs

[Mario Carneiro]

Did you try example : 67957^637 = 67957^637 := by norm_num?

[Bolton Bailey]

Indeed, that snippet times out.
Can you explain to me why #eval and norm_num don't do the same thing under the hood?

[Bolton Bailey]

To answer my question, https://leanprover.github.io/reference/expressions.html?highlight=eval#computation says that eval is faster and uses bytecode, whereas I guess the rest of lean does not.

[Mario Carneiro]

#eval is basically what python would do when asked to do bignum arithmetic: it just does the arithmetic, using an efficient representation for large numbers. Correctness of the operation is not proven. norm_num has to do something completely different, because it is required to prove the correctness of all operations it does. In particular, it works on symbolic expressions in base 2, which is probably about 500x larger in memory, plus the proof itself is even larger

[Mario Carneiro]

That is, #eval 2 + 2 means "please calculate 2+2, however you like", while (by norm_num : 2 + 2 = 4) means "please construct a proof relative to the lean axioms that 2 + 2 = 4"

[Bolton Bailey]

So are you telling me that lean does not even have the capability to use the addition multiplication functionality of the ALU when verifying proofs?

[Mario Carneiro]

no

[Mario Carneiro]

It has the capability to use add_mul and add_succ

[Bolton Bailey]

Ok, good to know

[Mario Carneiro]

because it's supposed to be working in ZFC (well, type theory), not ZFC + your computer

[Mario Carneiro]

the latter adds quite a bit to the trust base

[Mario Carneiro]

note that norm_num quite often uses #eval under the hood as an oracle. For example, when asked to prove or disprove prime 123671, the first thing it does is eval it to find out whether it's going to be proving primality or verifying non-primality (and in this case it just uses #eval to find the factors and verifies the multiplication)

[Mario Carneiro]

Bolton Bailey said:

To answer my question, https://leanprover.github.io/reference/expressions.html?highlight=eval#computation says that eval is faster and uses bytecode, whereas I guess the rest of lean does not.

Actually, that quote is talking about #eval vs #reduce. norm_num is much faster than #reduce, because #reduce works directly from the axioms of nat, which are defined using unary numerals, and so it takes exponential time to do anything. norm_num uses an asymptotically efficient representation by directly working with binary numbers, and uses theorems like distributivity in order to validate the individual moves. There should only be a constant factor difference between norm_num and #eval, although it's a rather large constant factor because addition and multiplication are heavily hardware accelerated, plus at very large numbers #eval gains an asymptotic improvement because it uses the GMP bignum library and this has a whole bunch of fancy algorithms like toom-cook multiplication that could be implemented in principle in norm_num but aren't because lean isn't practical at those sizes anyway

[Bolton Bailey]

Mario Carneiro said:

note that norm_num quite often uses #eval under the hood as an oracle. For example, when asked to prove or disprove prime 123671, the first thing it does is eval it to find out whether it's going to be proving primality or verifying non-primality (and in this case it just uses #eval to find the factors and verifies the multiplication)

Could norm_num use #eval under the hood to quickly factor ~10 digit numbers then? If so, perhaps we could think about using #eval to help compute Pratt certificates which the kernel could quickly check.

[Mario Carneiro]

Sure. I actually implemented this in metamath in order to do bertrand's postulate. In the end it turned out to be way overkill - you need to be dealing with primes of at least 6 digits before pratt certificates start to win over eratosthenes