## 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.