Stream: Beginner Questions

Topic: polynomials


view this post on Zulip Anthony Bordg (Nov 17 2020 at 17:22):

Is there anything on multivariate polynomials either in the basic library or in the AFP? Or at least on bivariate polynomials?
A quick search led me to the theory Polynomial and the archive Hilbert's Nullstellensatz. Both are difficult to parse due to the lack of comments, but I assume they deal only with univariate polynomials. Am I right?

view this post on Zulip Mathias Fleury (Nov 17 2020 at 17:36):

They are multivariate, see http://www.andreas-lochbihler.de/pub/haftmann14iw.pdf (or the slides) that explains the main ideas.

view this post on Zulip Mathias Fleury (Nov 17 2020 at 17:37):

I found polynomials very painful to use(you need to understand the construction, otherwise sledgegammer does not work) when I needed them, but it works.

view this post on Zulip Mathias Fleury (Nov 17 2020 at 20:22):

Some less negative comment: I used polynomials and needed very practical theorems (is x in the variables of the polynom 1? -- no this is not automatic). I did not need any analysis. The library was developed for the latter, not for my use case.

view this post on Zulip Manuel Eberl (Nov 18 2020 at 07:46):

@Mathias Fleury: Anthony was linking to the Polynomial theory from HOL-Computational_Algebra, which is univariate. What you're thinking of is the Polynomials entry in the AFP.

I use the latter in my entries on symmetric polynomials and power sum polynomials, and I heavily use the first of those in my proof of the transcendence of π\pi. But yes, they are very painful to use and there's a lot of stuff missing.

There might be a lot of material in my entries that should be moved to the Polynomials entry as well.

view this post on Zulip Mathias Fleury (Nov 18 2020 at 07:49):

ah yeah, true, sorry for the confusion.

view this post on Zulip Mathias Fleury (Nov 18 2020 at 07:51):

I forgot that we have at least 2 different libraries of polynomials...

view this post on Zulip Manuel Eberl (Nov 18 2020 at 07:54):

That's a very optimistic estimate. :P

view this post on Zulip Manuel Eberl (Nov 18 2020 at 07:54):

There's at least 3 more in HOL-Algebra.

view this post on Zulip Manuel Eberl (Nov 18 2020 at 07:56):

The univariate ones from HOL-Computational_Algebra are by far the most pleasant ones to use, but, well, they are univariate. And they are bound to the type classes, like everything in HOL-Computational_Algebra.

view this post on Zulip Anthony Bordg (Nov 18 2020 at 20:38):

Mathias Fleury said:

They are multivariate, see http://www.andreas-lochbihler.de/pub/haftmann14iw.pdf (or the slides) that explains the main ideas.

Thanks for the reference.

view this post on Zulip Anthony Bordg (Nov 19 2020 at 12:18):

When using univariate polynomials, should one see them as particular cases of multivariate polynomials or is there one of the many formalizations of univariate polynomials which is compatible with multivariate polynomials as formalized in Polynomials?

view this post on Zulip Manuel Eberl (Nov 19 2020 at 12:36):

I don't think there is one that is compatible to that. But I would say if you can use the ones from HOL-Computational_Algebra, you should use those.

view this post on Zulip Manuel Eberl (Nov 19 2020 at 12:37):

There's also some work on bivariate polynomials that sees them as 'a poly poly.

view this post on Zulip Manuel Eberl (Nov 19 2020 at 12:37):

(where poly is the type from HOL-Computational_Algebra)

view this post on Zulip Gergely Buday (Nov 19 2020 at 16:20):

(deleted)

view this post on Zulip Mathias Fleury (Nov 20 2020 at 11:49):

(deleted)


Last updated: Aug 13 2022 at 05:18 UTC