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.

is this coq related?

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.

doesn't the paer already have an agda proof?

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.

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

??

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

I missed this point !!

Thank you very much. I would look there.

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

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

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

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

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

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

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: Sep 30 2023 at 05:01 UTC