Examples of mv_polynomials

Stream: new members

[YurySerdyuk]

Hi, I am a complete newbie with Lean, but I would like to prove some properties of simple programs dealing with the multivariate polynomials.
At first, I would like to create the examples of polynomials and to do some operations on them.

My first attempt was :

import data.mv_polynomial.comm_ring
variables x y : ℕ

def p1 : mv_polynomial (fin 2) ℚ := x^3 * y + 1
def p2 : mv_polynomial (fin 2) ℚ := x * y + x + y + 1

#eval p1 + p2

What is wrong with my code ? The answer of Lean was

missing 'noncomputable' modifier, definition 'p1' depends on 'mv_polynomial.comm_ring'

[Eric Wieser]

Lean is telling you to write noncomputable before the word def; but you can also just write noncomputable theory near the top of the file

[Eric Wieser]

But those aren't the polynomials you think they are; those are families of constant polynomials parametrized by x, y

[Eric Wieser]

The two generators of your polynomial are actually mv_polynomial.X 0 and mv_polynomial.X 1

[YurySerdyuk]

def p1 : mv_polynomial (fin 2) ℚ := mv_polynomial.X 3
def p2 : mv_polynomial (fin 2) ℚ := mv_polynomial.X 2

#eval p1 + p2

code generation failed, VM does not have code for 'classical.choice'

[Matthew Ballard]

mv_polynomial does not currently generate any executable computer code

[Eric Rodriguez]

The way polynomials are implemented doesn't let you use #eval to see them, but you can definitely prove whatever you want about p1 and p2

[Matthew Ballard]

When you call #eval you ask your computer to do a computation which is not possible with the design

[Eric Rodriguez]

Also note that the number is not a power, it's the index: we tend to use X and Y in pen and paper for 2 degrees but because computers, we have to write X_0, X_1