Problem with add_pow

Stream: new members

[Andrew Wheen]

I'm having trouble getting add_pow (binomial theorem) to run properly. For example:

import data.nat.basic
import data.real.basic
import data.nat.choose.sum -- Binomial Theorem
variables (x y : ℝ)
variables (z : ℕ)
def x : ℝ := 2.0
def y : ℝ := 3.0
def z : ℕ := 4

#eval add_pow x y z

produces the message "cannot evaluate function: 0 arguments given but expected 3". When I tried:

#eval add_pow 2.0 3.0 4

it returned an answer of #0 with "result type does not have an instance of type class 'has_repr', dumping internal representation". Any suggestions?

[Reid Barton]

add_pow is a theorem that says that two real numbers (in this case) are equal.
What are you expecting to happen when you "run" it?

[Reid Barton]

Maybe #check add_pow 2.0 3.0 4 is more like what you want?

[Eric Wieser]

(Please also take a look at #backticks)

[Ruben Van de Velde]

I don't think #eval is going to do much for you, especially with real numbers

[Andrew Wheen]

My expectation was that '''#eval 2 3 4''' would return a result of 625 (ie (2 + 3)^4). The definition of add_pow says that it is an implementation of the binomial theorem. I've tried making x and y into natural numbers but the result is the same.
Thanks for the guidance on backticks.

[Reid Barton]

#eval (2 + 3)^4 should print 625.

[Andrew Wheen]

Yes, '''#eval (2 + 3)^4''' does print 625, but for some reason '''#eval add_pow 2 3 4''' prints #0.

[Reid Barton]

Right, it doesn't really make sense to #eval a theorem.

[Kevin Buzzard]

More precisely, add_pow 2 3 4 is the proof of a theorem.

[Kevin Buzzard]

(in this case it's a proof that 625=625)

[Mauricio Collares]

And all that lean stores about proofs at runtime is "Yep, that was a proof indeed" (which is printed as #0)

[Andrew Wheen]

OK. So why does #eval nat.choose 5 3 return a result of 10 (as I expected)?

[Kevin Buzzard]

Because nat.choose is a function, and nat.choose 5 3 is a number.

[Matthew Ballard]

It’s a def.

[Matthew Ballard]

def’s can store data that your computer can compute on.

[Andrew Wheen]

Is the binomial theorem available as a function?

[Kevin Buzzard]

What does that question even mean? The binomial theorem is a theorem statement or a theorem proof, depending on what precisely you mean. It is not a number or a function.

[Kevin Buzzard]

I guess strictly speaking add_pow is a function which eats three numbers and then returns a proof, so it is a function in that sense.

[Matthew Ballard]

theorems carry no such data. As Mauricio, they are evidence to the Lean kernel that a theorem statement is ok

[Kevin Buzzard]

But nat.choose is a function which eats two numbers and returns a number.

[Reid Barton]

Can you rephrase your question without the phrase "binomial theorem"?

[Andrew Wheen]

OK. Perhaps I've asked the wrong question. In simple terms, I want to prove that (a + b)^n > a^n + b^n if n > 1, and the simplest way to do this seemed to be to use a binomial expansion and show that the total is greater than the first and last terms. Is there a better way of doing this in Lean3 ?

[Kevin Buzzard]

Sure you can do that, that will work just fine (as long as a,b>0). But what does that have to do with #eval?

[Reid Barton]

Try #check as suggested above.

[Andrew Wheen]

I used #eval because I hadn't spotted the distinction between add_pow returning a proof while choose returns a number . I therefore assumed that add_pow wasn't working properly when I started getting strange error messages, and my first response in these circumstances is typically to try #eval and #check.
Many thanks to everyone who replied. I think I can now see a way forward.