arithmetic proof with big constants

Stream: new members

[Travis Hance]

I want to prove a simple arithmetic calculation theorem:

theorem x : 9000 / 3 = 3000 := rfl

This works for smaller numbers, but for the given example, I get a warning about "(deterministic timeout)". How exactly does the arithmetic scale? What's the suggested way to deal with things like this?

I notice that #eval isn't absurdly slow or anything, e.g.,

#eval 90000000000 / 3

works fine. So how come when constructing proof terms it chokes on such small numbers?

[Simon Hudon]

try import tactic.norm_num and by norm_num (from mathlib)

[Simon Hudon]

#eval uses the virtual machine to do its computation. In the virtual machine, natural numbers are implemented very efficiently: it uses libgmp. With rfl, the computation is done using logical reduction rules the definition of nat in the logic is very inefficient: it uses unary representation.

[Travis Hance]

That worked. Thank you!

[Travis Hance]

I see the proof term it generates is doing some binary representation thing. That's pretty neat.

[Simon Hudon]

Yes, that's the cool thing about numerals. the lexeme 10 is syntactic sugar for bit0 (bit1 (bit0 one)) which are functions that evaluate into succ and zero (in the case of nat) but which don't have to be evaluated to do arithmetic.

[Kevin Buzzard]

One of the questions on my undergraduate example sheets was: "which number is bigger: $2^{1/2000000000000}$ or $3^{1/3000000000000}$?" I had to be careful when formalising the result in Lean. In theory I could work out both sides to 20 decimal places and I'd be done, but Lean cannot do this yet with a verified argument (as far as I know) so I had to use other tricks.

[Mario Carneiro]

Oh, this reminds me of a recent question that came up on puzzling.SE: Which is bigger, $g_{64}$ or $BB(18)$? That's Graham's number vs the busy beaver function

[Kevin Buzzard]

busy beaver hands down

[Kevin Buzzard]

even BB(12) is bigger than Graham's number, right?

[Mario Carneiro]

that's my intuition as well, but I have no idea how to prove it

[Kevin Buzzard]

Where does your intuition come from?

[Kevin Buzzard]

Mine came from a children's book

[Kevin Buzzard]

"Stinky Finger's House Of Fun"

[Mario Carneiro]

My intuition is BB is bigger than everything

[Mario Carneiro]

but I'm not sure about really small inputs

[Kevin Buzzard]

One of the characters in it. Brian Brain, at some point makes exactly the same observation

[Kevin Buzzard]

"all of these are dwarfed by Busy Beaver 12", he says. I had to go to Wikipedia to look up the Busy Beaver function

[Mario Carneiro]

wikipedia actually contains a statement that BB(12) is bigger than 3^^^^3, but it doesn't say about g64

[Patrick Massot]

BB(8) is not so tall, especially when standing on sand

[Mario Carneiro]

Oh, it also mentions that BB(17) > g64

[Mario Carneiro]

Your question about $2^{1/2000000000000}<3^{1/3000000000000}$ boils down to proving $\log_23<3/2$, or $2^3<3^2$; I don't think any high precision estimates are needed

[Mario Carneiro]

In fact the hardest part, numerically, is just showing that 2000000000000 = 2 * 1000000000000 and 3000000000000 = 3 * 1000000000000

[Mario Carneiro]

(which is of course much harder in binary)

[Chris Hughes]

But it would require no work if we could do high precision estimates.

[Mario Carneiro]

It would require a lot of work, by the computer. Nothing is free

[Mario Carneiro]

If you prove (x + 1)^100 = (1 + x)^100 by using ring, I will be sad

[Mario Carneiro]

I'm pretty sure that question was written specifically to foil attempts to prove it by plug-and-chug calculator methods

[Kevin Buzzard]

Yes, sure it was. And yes, the point is that $2^3<3^2$, but it was interesting to prove this in Lean because you had to be careful to never write anything which triggered a computation.

[Kevin Buzzard]

I proved some general lemma first, and then applied it to get the result.

[Chris Hughes]

Computer work is waaaay cheaper than human work.

[Mario Carneiro]

the computer will be asked to solve this problem many many times on many many computers though. Think of the environment

[Mario Carneiro]

also if you ever want to move this proof anywhere else, it helps if you didn't write intentionally bad proofs

[Kevin Buzzard]

In fact the hardest part, numerically, is just showing that 2000000000000 = 2 * 1000000000000 and 3000000000000 = 3 * 1000000000000

My memory is that this is exactly where I started: I set $N=10^{12}$ and then rewrote for 2N and 3N and then never thought about the explicit value of N again

[Kevin Buzzard]

I would dig it out from the xena archives but I'm busy wrestling with type class hell

[Chris Hughes]

the computer will be asked to solve this problem many many times on many many computers though. Think of the environment

Let's solve that problem instead.