Converting polynomials to Expr

Stream: metaprogramming / tactics

[Sarah Azevedo Pereira]

Hi, everyone!
I'm trying to represent polynomials as Expr, but I'm not sure how they would be represented. Would they appear as a function application? Since polynomials like these don't exactly "return" a value, I'm struggling to understand how to map them into the Expr world.

import Mathlib
open MvPolynomial
noncomputable def mexample : MvPolynomial (Fin 3) ℤ := (X 0 ^ 2 + 3 * X 1 - X 2)

Any insights on how to convert a polynomial like this example would be apreciated!
Thanks in advance

[Patrick Massot]

I’m afraid this question is too vague to get a good answer. Maybe you could try to tell us what you want to do with this Expr?

[Sarah Azevedo Pereira]

It would be for ideal membership proof automation. The idea is to have a set of polynomials and use some rules to manipulate and combine them to verify if a given polynomial belongs to the ideal generated by the set.

[Sarah Azevedo Pereira]

For this, I was thinking of representing the polynomials as Expr to leverage Lean's metaprogramming tools...
The theorem that should be proven would look like this:

theorem thrm : tgt ∈ Ideal.span G :=
by (...)

where G is the set of polynomials, and the list of rules to be applied may contain polynomials that aren't in G, so i couldn't get them from the local context