Hilbert Basis Theorem constructivelly in Coq/Rocq

The repository contains a constructive proof of Hilbert's Basis Theorem (a.k.a. HBT below) partly following the outline given in Coquand & Persson 98 (see refs below).

Rings and ideals (constructivelly)

We assume some basic knowledge about rings , ring ideals and polynomial rings [X]: - rings are tuples (,+,*,0,1) where addition + forms a commutative group with 0 as a neutral, and multiplication * forms a commutative monoid with 1 as neutral. There is also a distributivity law of * over +. Notice that rings need not have commutative multiplication * (typically, matrices form non-commutative rings), but for our purpose here, we assume commutativity; - ideals are non-empty additive sub-groups of rings furthermore stable under scalar products, i.e. ` x , y , x*y `; - the polynomial ring `[X]` is usually presented via its canonical representation (see below) but also has a categorical characterization as the initial ring in the category of pointed extensions of, i.e. the ring freely generated by adding an unknown X to ``.

Notice that polynomials over a ring are a bit tricky to implement if one __does not__ assume that has decidable equality. Indeed, in that case, even the notion of degree of a polynomial cannot be defined (as a total function): what is the degree of a.X if one cannot discriminate whether a is 0 or not?

Hence the usual canonical representation of [X] as finite formal sequences a.X+...+a.X (where the head coefficent a is not 0) is not workable because one cannot normalise addition (or multiplication for non-integral rings) to ensure that the head coefficient not 0.

Instead we build the theory of polynomial rings using setoids, i.e. equality on `is relaxed to be a congruence and the polynomial 0.X+0.X+1.Xhas alternate equivalent representations such as eg0.X+0.X+1.X+0.X` that we identify under a well chosen congruence.

Of course, to ensure that we indeed build [X] and not an arbitrary pointed extension of ``, we show that our construction satisfies the categorical initiality condition.

Hilbert Basis Theorem in classical settings

Classically, ring ideals can (possibly) be: - principal: i.e. = { x*g | x } is generated by a single generator g; - finitely generated: i.e. = { x*g+...+x*g | x,...,x } is generated by finitely many generators g,...,g;

and in a principal ring, all the ideals are principal. Typically, because of Euclidean division, [X] is principal when `is a _field_ (a ring where*forms a group over non-zero values). However principality is not preserved by the construction of polynomial rings. Typically, neitherZ[X]nor(Z/4Z)[X]` are principal rings.

A Noetherian ring is a ring where all ideals are finitely generated. Hence principal rings are Noetherian but, unlike principality, Noetherianess is preserved by the construction of polynomials rings. And as a consequence, for any field `,[X]is Noetherian but more generally, also[X,...,X]` is Noetherian which is original the statement of the HBT.

Hilbert Basis Theorem in constructive settings

The definition of Noetherian ring (or principal ring btw) in anti-classical settings, where the law of excluded middle is refuted, are mostly useless. Indeed, given a proposition P : Prop and any non trivial ring (i.e. where `0 1`) which has decidable equivalence (possibly this is equality, e.g. for the ring of integers `Z`), then ` := { x | x = 0 P }` is an ideal of, and if it is finitely generated (a fortiori principal) then one can prove P P. This observation is already made in the discussion [2].

As consequence, no non trivial ring with decidable equivalence can be Noetherian unless the law of excluded middle holds, which is by definition refuted in anti-classical settings. So neither Z nor Z/nZ (n > 1) can be Noetherian with that definition of Noetherianess based on the existence of a finite set of generators for all ideals.

There are many possible alternate characterizations of Noetherian rings that better suit constructive or anti-classical settings, see e.g. [2], or [4] for a more in depth analysis.

The usually favored (constructive) formulation of the HBT is [X] is Noetherian when the ring `` is, i.e. Noetherianess is preserved by the polynomial ring construction. This of course constructivelly implies the initial formulation of the HBT as [X,...,X] is Noetherian. However, a good definition of Noetherianess will not constructivelly imply the existence of finite basis for any ideal (because of the argumentation above).

We use the definition proposed in [1], using bar inductive predicates, with a revisited terminology. For a given ring , let us define `pauses` (denoted `PA`) for a list of values in as coq Definition PA [x;...;x] := i, x idl {x;...;x}. where idl P is the smallest ideal containing a subset P of ``.

Then, following [1], we characterize Noetherianess as coq Definition noetherian ( : ring) := bar (PA ) []. i.e. the empty list [] : list unavoidably pauses after finitely many steps, however you extend it by adding elements at its head. As a consequence there cannot exist a strictly increasing infinite sequence of finitely generated ideals. But constructivelly, this does not imply that ideals always have finite sets of generators.

We establish the two following results: coq Theorem HBT : noetherian noetherian (poly_ring ). Theorem Hilbert_Basis_Theorem n : noetherian R noetherian (multivariate_ring n).

where poly_ring is (isomorphic to) [X] and multivariate_ring n is (isomorphic to) [X,...,X].

Examples of Noetherian rings

As explained in the previous paragraph, the classical definition of principal ring (as having only mono-generated/principal ideals) is not suited in anti-classical settins because again, the ring of integers Z would not be principal. Instead we define Bezout rings as: coq Definition bezout_ring ( : ring) := g, idl l = { x*g | x }. i.e. every finitely generated ideal is a principal ideal. Notice that this definition of Bezout ring does not implies Noetherianess but however the two properties are linked in some way, e.g. we show: coq Theorem wf_sdiv_bezout_noetherian ( : ring) : bezout_ring ( x y : , x | y x | y) well_founded ( x y : , x | y y | x) noetherian . meaning that any Bezout ring with (logically) decidable divisibility, and well-founded strict divisibility is Noetherian.

In addition to the HBT above, with these definitions, we can show that: - (discrete) fields are Bezout and Noetherian rings; - the ring of integers Z is a Bezout ring and Noetherian ring (via wf_sdiv_bezout_noetherian above); - finite rings are Noetherian (e.g Z/nZ for n > 0); - the quotient of a Bezout (resp. Noetherian) ring is Bezout (resp. Noetherian).

The direct product is Noetherian

Additionally, we remarked classical proofs of the Noetherianess of the direct product of two rings was using Ramsey like arguments. Hence, we wondered whether a constructive form of Ramsey's theorem, based on bar inductive predicates, could be adapted to derive the closure of Noetherianess under direct products, w/o assuming further properties on rings (such as e.g. strong discreteness).

And indeed, it turns out that D. Fridlender's proof of Ramsey's theorem [5], simplified and reworked in Rocq, was a good starting point to derive the Noetherianess of the direct products: coq Theorem product_noetherian : noetherian noetherian noetherian (product_ring ).

Further comments on that new proof will come later on.

Induction principles derived from Noetherianess

We show that several instances of witnessed strict reverse inclusion are (constructivelly) well-founded for Noetherian ring: coq Notation "P Q" := Q P x, x P x Q. Given a Noetherian ring : - the relation is well-founded when restricted to the ideals of `; - the relation P Q, idl P idl Qis well-founded on Prop; - the relation l m, idl l idl m)is well-founded onlist `

where [x;...;x] := {x,...,x} (mapping a list to a subset of ) and `idl P` is smallest ideal containing the subset `P` of.

Obtaining finite bases

Using one of the previous induction principles, it is possible to show the existence of a basis for an ideal, under certain conditions. We finish with the construction of a finite basis for ideals satisfying the condition that they can be compared for inclusion with any finitely generated ideal: coq Theorem find_basis ( : ring) ( : Prop) : noetherian ideal ( l : list , (x, x idl l x) idl l) b, = idl b. The property l, (x, x idl l x) idl l states that for any list l (of generators), either `contains a element outside of the ideal generated byl`, or is included into it. It is of course is a trivial consequence of the law of excluded middle, but we do not assume excluded middle in here.

Remarks on the proof

• the largest part of the proof, though not the most difficult, is the construction of the polynomial ring [X], based on the Setoid rewriting and Ring frameworks of Coq which allows us to micro-manage ring computations, see poly.v; Without those two frameworks, that construction could become quite tricky and unsurprisingly, this part was avoided in the implementation proposed in [1].
• the open induction principle of [1] is reinterpreted as a well-founded induction over the projection of a lexicographic product.
• The proof of the HBT stated above is quite small (20-25 loc) in hbt.v but relies on the theorem update_lead_coef from poly.v which states that if x is the head coefficent of p and is a linear combination of the head coefficents of v, a list of polynomials of length less than p, then p::v can be updated into q::v where q := p+lc is of length strictly less than p and lc is a linear combination of the values in v.
• Updating preserves PA (pauses) and thus also bar PA.

References

• [1]. Grbner Bases in Type Theory by Coquand & Persson 1998.
• [2]. The following discussion is interesting (https://mathoverflow.net/questions/222923/alternate-proofs-of-hilberts-basis-theorem).
• [3]. Strongly Noetherian rings and constructive ideal theory by Herv Perdry 2004.
• [4]. See also the Buchberger repository.
• [5]. Higman's lemma in type theory by Fridlender 1996.