Stream: Coq users

Topic: question on paper by Coquand & Persson

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.

Gaëtan Gilbert (Dec 21 2021 at 20:48):

is this coq related?

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.

Gaëtan Gilbert (Dec 21 2021 at 21:44):

doesn't the paer already have an agda proof?

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.

Gaëtan Gilbert (Dec 21 2021 at 21:54):

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

??

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.

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

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

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

Sergei Meshveliani (Dec 22 2021 at 10:13):

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

Karl Palmskog (Dec 22 2021 at 10:19):

maybe you've already seen:

• An Integrated Development of Buchberger's Algorithm in Coq by Persson
• A machine checked implementation of Buchberger's algorithm by Théry, overview of what is in the buchberger repo

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

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: Oct 13 2024 at 01:02 UTC