Anthony Bordg (Nov 17 2020 at 17:22): 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?
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.
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.
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.
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 . 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.
Mathias Fleury (Nov 18 2020 at 07:49):ah yeah, true, sorry for the confusion.
Mathias Fleury (Nov 18 2020 at 07:51):I forgot that we have at least 2 different libraries of polynomials...
Manuel Eberl (Nov 18 2020 at 07:54):That's a very optimistic estimate. :P
Manuel Eberl (Nov 18 2020 at 07:54):There's at least 3 more in HOL-Algebra.
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.
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.
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?
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.
Manuel Eberl (Nov 19 2020 at 12:37):There's also some work on bivariate polynomials that sees them as 'a poly poly.
Manuel Eberl (Nov 19 2020 at 12:37):(where poly is the type from HOL-Computational_Algebra)
Gergely Buday (Nov 19 2020 at 16:20):(deleted)
Mathias Fleury (Nov 20 2020 at 11:49):(deleted)
Last updated: Dec 30 2024 at 16:22 UTC