## Stream: Is there code for X?

### Topic: defining a polynomial

#### Kevin Lacker (Oct 06 2020 at 22:11):

I'm looking for code around polynomials, and obviously there is a lot of code that deals with polynomials, but how do I just do basic stuff with a polynomial, like, specify that p = 16 * x ^ 3 - 20 * x ^ 2 + 6 * x + 1 is a polynomial, calculate that p(0) = 1, and so on

#### Kevin Lacker (Oct 06 2020 at 22:20):

i am guessing at it but I feel like I must be doing something fundamentally wrong; things like def four : polynomial ℝ := 4 fail saying "four is noncomputable"

#### Alex J. Best (Oct 06 2020 at 22:43):

Its not really possible for lean to compute with polynomials (specifically) right now in the same way it can compute that
1 + 2 = 3
via
#eval 1 + 2
that's what four is noncomputable is saying, you can do something like this though

noncomputable theory
open polynomial
def p : polynomial ℝ := 16 * X ^ 3 - 20 * X ^ 2 + 6 * X + 1
lemma t : eval 0 p = -1 :=
begin
conv_lhs {
norm_num [p],
},
end


to use the simplifier and norm_num to evaluate expressions.
I put -1 as a placeholder value, if you put your cursor after norm_num [p], you should see that it simplified to 1.

#### Alex J. Best (Oct 06 2020 at 22:52):

A variant of basically the same thing is to do

def t : eval (0 : ℝ) (16 * X ^ 3 - 20 * X ^ 2 + 6 * X + 1) = _ :=
begin
conv_lhs {
norm_num,
},
end
#print t


as its a def lean can infer the hole _ from the proof, and #print t shows that you proved the right evaluation.

#### Kevin Lacker (Oct 06 2020 at 22:58):

what is the noncomputable theory there doing - is it legitimate to just put that everywhere, if someone cared only about what is true, rather than what is computable?

#### Alex J. Best (Oct 06 2020 at 23:01):

Noncomputable theory means "instead of telling me when some def is not computable automatically mark it as noncomputable def if needed". For proving mathematical things its basically legitimate to put it everywhere, unless you want and are expecting your defs to be computable (in the sense that lean will produce bytecode to evaluate your functions) and want to be warned when they accidentally aren't.

#### Alex J. Best (Oct 06 2020 at 23:03):

Polynomials used to be computable in that sense in lean, but it caused some trouble when proving theorems to worry about different decidable instances, and you wouldn't really want to compute directly with the mathlib definition of a polynomial anyway (a function with finite support isn't really an efficient data structure). So it was changed a year or so back, maybe there are some findable threads on zulip about it.

Last updated: May 16 2021 at 05:21 UTC