Stream: Coq users

Topic: question on paper by Coquand & Persson


view this post on Zulip Sergei Meshveliani (Dec 21 2021 at 20:34):

I am looking into "Groebner bases in type theory" by Th.Coquand & H.Persson (1998),
and trying to understand its 2.2 "A constructive proof of Dickson's lemma".
May be there are people here who are familiar with such papers (?)
There are certain ambiguities, and I have got confused, to some degree.
In the definition Good_R(b₀ ... bₘ) to be ∃ i < j ≤ m. bᵢ R bⱼ , do i, j belong to , or may them belong to A introduced earlier?
Then, there follows the definition

M(σ.(x,b)) = ......  Good_×R | σ.(y,b)

First, Good was defined above as over B, and here Good is applied as over A × B. So, do we have here B := A × B ?
Second, really is it ≤ × R rather than ≤ × S ?
S was said a relation on B, so that probably is on A and R is not on B ?
May be the authors could explain?
Thanks.

view this post on Zulip Gaëtan Gilbert (Dec 21 2021 at 20:48):

is this coq related?

view this post on Zulip Sergei Meshveliani (Dec 21 2021 at 21:41):

is this coq related?

I believe, this proof is implemented somewhere in Coq. Also Th. Coquand is among the authors.
And for me, it is easier to read a paper than its Coq program.
My aim is to implement the thing in Agda.

view this post on Zulip Gaëtan Gilbert (Dec 21 2021 at 21:44):

doesn't the paer already have an agda proof?

view this post on Zulip Sergei Meshveliani (Dec 21 2021 at 21:49):

doesn't the paer already have an agda proof?

I shall ask, but I am sure it does not.
The proof is used in advanced polynomial algebra, and generally, Coq has much wider libraries in this area, it has started earlier, and has more users.

view this post on Zulip Gaëtan Gilbert (Dec 21 2021 at 21:54):

In the appendix we present a computer formalisation of Dickson's lemma

??

view this post on Zulip Sergei Meshveliani (Dec 21 2021 at 21:57):

In the appendix we present a computer formalisation of Dickson's lemma

I missed this point !!
Thank you very much. I would look there.

view this post on Zulip Alexander Gryzlov (Dec 21 2021 at 22:31):

I think the code they have is for Agda1, which is probably quite different from modern Agda2

view this post on Zulip Karl Palmskog (Dec 22 2021 at 08:37):

the Coq proof of Dickson's lemma is here: https://github.com/coq-community/buchberger/blob/master/theories/Dickson.v

view this post on Zulip Karl Palmskog (Dec 22 2021 at 08:43):

but the state of the art in formalization of polynomial algebra is MathComp, so for Gröbner bases this is more modern (but doesn't aim for extraction): https://github.com/thery/grobner

view this post on Zulip Sergei Meshveliani (Dec 22 2021 at 10:13):

Thanks to people for the notes. All of these notes are helpful.

view this post on Zulip Karl Palmskog (Dec 22 2021 at 10:19):

maybe you've already seen:

view this post on Zulip Laurent Théry (Dec 22 2021 at 11:26):

I believe, this proof is implemented somewhere in Coq

Nop the initial development was in Agda (it is what the paper describes) and Henrik ported it to Coq later when he was post-doc at INRIA. This is what is in Dickson.v

view this post on Zulip Karl Palmskog (Dec 22 2021 at 13:17):

probably, the porting of the proof to Coq is what made it possible to have it maintained and working with recent Coq today. First, the proof was included in a Coq contrib and now fully maintained in coq-community. I think Agda code from the early 2000s is going to be difficult to port.


Last updated: Jan 29 2023 at 01:02 UTC