Recursive representation of polynomials · Is there code for X?

Stream: Is there code for X?

Topic: Recursive representation of polynomials

David Vodička (Mar 25 2024 at 07:23):

Hello everyone. I am currently trying to use the Polynomials library for multivariate polynomials and i wonder if there is a recursive representation as it was mentioned in the article "Towards abstract and executable multivariate polynomials in Isabelle". I haven't found the type poly-rec or anything similar in the theories. I feel it could be buried in the Power_products file but i get lost pretty quick there.

Yong Kiam (Mar 25 2024 at 07:57):

I believe the type to look for is mpoly. there're conversions from 'a mpoly to 'a mpoly poly (isolating one variable)

Manuel Eberl (Mar 25 2024 at 09:36):

Yes. The lemmas and definitions for that type are unfortunately spread over a million different AFP entries, so if you're looking for anything specific do ask in this thread and I can see if I remember where it is exactly.

David Vodička (Mar 25 2024 at 09:54):

I am working with the type 'a mpoly introduced in the theory MPoly_Type but I am unable to locate the conversion mentioned by Yong Kiam. I see that the theory MPoly_Type_Univariate is only a bridge between different univariate theories. I also found the type poly in the theory Polynomials but its just a type synonym for a list of monomials. I cannot find anything recursive-like in terms of variables.

Manuel Eberl (Mar 25 2024 at 09:57):

https://www.isa-afp.org/sessions/factor_algebraic_polynomial/#Poly_Connection.html#Poly_Connection.mpoly_to_mpoly_poly_def|fact

Manuel Eberl (Mar 25 2024 at 09:58):

Of course you can also just do induction on the variables occuring in a multivariate polynomial. Depends a bit on what you want to do exactly.

Manuel Eberl (Mar 25 2024 at 09:59):

If I recall correctly I do something like that in my entry on symmetric polynomials. Successively eliminating variables until you have a constant mpoly.

David Vodička (Mar 25 2024 at 10:19):

Thank you very much. I will definitely check your entry on the symmetric polynomials. To clarify what I want to do; I ended up doing a bachelor's thesis on formalizing Hilbert basis theorem for multivariate polynomials in Isabelle. With the help of my advisor, I managed to define multivariate polynomials over a ring a prove that it also forms a ring, but I am stuck how to deal with setting up the induction for the proof of Hilbert theorem.

Manuel Eberl (Mar 25 2024 at 10:21):

What definition of a ring are you using?

Manuel Eberl (Mar 25 2024 at 10:22):

Like, HOL-Algebra style rings? Or just rings as a type class?

Manuel Eberl (Mar 25 2024 at 10:22):

Also if I may ask, who is your advisor?

Manuel Eberl (Mar 25 2024 at 10:23):

I guess if you want to talk about ideals you'll probably have to use HOL-Algebra, or the newer library by Clemens Ballarin. But I'm not sure if that one even has a definition of ideals.

David Vodička (Mar 25 2024 at 11:44):

Yes I do use HOL-Algebra style rings. I intend to use the theory Ring_Divisibility containing ideals.

Manuel Eberl (Mar 25 2024 at 11:46):

All right. Just a word of warning: dealing with HOL-Algebra can be very frustrating.

Yong Kiam (Mar 25 2024 at 14:15):

BTW, isn't the standard (?) strategy for this to prove it for univariate poly first then lift it to mpoly? you might hopefully avoid a lot of the complications to deal with mpoly if you formalize it over a general enough type class for poly

ah now I read your message more carefully, you're already at the induction, my bad

Wenda Li (Mar 25 2024 at 21:13):

Sorry for the late chime in. Just to ensure that you didn't miss other Groebner-related entries by Alexander Maletzky:

He also has an entry on Hilbert's Nullstellensatz.

'a poly poly has been used to encode bivariate polynomials: https://www.isa-afp.org/sessions/algebraic_numbers/#Bivariate_Polynomials

HOL-Algebra is indeed, as Manuel mentioned, quite chaotic -- I always hope we will have enough incentive to give it an overhaul. The library has two univariate polynomials and one multivariate polynomial:

Aaron Crighton has been developing on top of those polynomial definitions:

Stepan Holub (Mar 26 2024 at 17:17):

Manuel Eberl said:

Also if I may ask, who is your advisor?

Hi, Manuel,
David is my student. I keep wondering why/whether Hilbet Basis theorem is not already there in some form. Perhaps the Groebner basis library mentioned by Wenda is the right answer. Need to have a closer look.
Stepan

Stepan Holub (Mar 26 2024 at 17:21):

Wenda Li said:

HOL-Algebra is indeed, as Manuel mentioned, quite chaotic -- I always hope we will have enough incentive to give it an overhaul.

I, for one, certainly vote for an overhaul. :smile:

Last updated: Nov 05 2025 at 20:25 UTC