defining a polynomial

Stream: Is there code for X?

[Kevin Lacker]

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]

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]

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]

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]

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]

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]

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.