Zulip Chat Archive

Stream: Is there code for X?

Topic: defining a polynomial


view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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