Zulip Chat Archive

Stream: general

Topic: norm_num for real exponentiation


Bolton Bailey (Jun 20 2021 at 18:15):

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 (Jun 20 2021 at 18:20):

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 (Jun 20 2021 at 19:29):

Not quite sure how to use rpow_nat_cast here

Patrick Stevens (Jun 20 2021 at 19:29):

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 (Jun 20 2021 at 19:29):

Let me find the right line

Patrick Stevens (Jun 20 2021 at 19:30):

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

Patrick Stevens (Jun 20 2021 at 19:31):

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

Patrick Stevens (Jun 20 2021 at 19:31):

(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 (Jun 20 2021 at 19:42):

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

Bolton Bailey (Jun 20 2021 at 19:46):

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 (Jun 20 2021 at 19:49):

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 (Jun 20 2021 at 19:52):

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 (Jun 20 2021 at 19:53):

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 (Jun 20 2021 at 19:54):

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 (Jun 20 2021 at 19:55):

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 (Jun 20 2021 at 19:55):

Let me find that log_pow variant. I used recently.

Patrick Stevens (Jun 20 2021 at 19:56):

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 (Jun 20 2021 at 20:04):

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

Bolton Bailey (Jun 21 2021 at 18:26):

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 (Jun 21 2021 at 19:33):

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 (Jun 21 2021 at 19:34):

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 (Jun 21 2021 at 19:36):

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

Mario Carneiro (Jun 21 2021 at 19:39):

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

Eric Rodriguez (Jun 21 2021 at 19:41):

can norm_num do decent estimates of real logs?

Mario Carneiro (Jun 21 2021 at 19:41):

if you do the right calculations, sure

Mario Carneiro (Jun 21 2021 at 19:42):

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 (Jun 21 2021 at 19:44):

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 (Jun 21 2021 at 23:45):

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 (Jun 21 2021 at 23:59):

#eval doesn't do proofs

Mario Carneiro (Jun 22 2021 at 00:00):

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

Bolton Bailey (Jun 22 2021 at 00:04):

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 (Jun 22 2021 at 00:10):

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 (Jun 22 2021 at 00:11):

#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 (Jun 22 2021 at 00:13):

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 (Jun 22 2021 at 00:13):

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 (Jun 22 2021 at 00:13):

no

Mario Carneiro (Jun 22 2021 at 00:14):

It has the capability to use add_mul and add_succ

Bolton Bailey (Jun 22 2021 at 00:14):

Ok, good to know

Mario Carneiro (Jun 22 2021 at 00:14):

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

Mario Carneiro (Jun 22 2021 at 00:15):

the latter adds quite a bit to the trust base

Mario Carneiro (Jun 22 2021 at 00:16):

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 (Jun 22 2021 at 00:43):

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 (Aug 16 2021 at 07:04):

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 (Aug 16 2021 at 16:57):

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


Last updated: Dec 20 2023 at 11:08 UTC