# Bar Inductive Predicates for Constructive Algebra in Rocq

Dominique Larchey-Wendling

► To cite this version:

Dominique Larchey-Wendling. Bar Inductive Predicates for Constructive Algebra in Rocq. CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Kathrin Stark; Yannick Zakowski; Nikhil Swamy; Nicolas Tabareau, Jan 2026, Rennes, France. pp.15-28, 10.1145/3779031.3779103. hal-05458206

HAL Id: hal-05458206

https://hal.science/hal-05458206v1

Submitted on 14 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

Latest updates: https://dl.acm.org/doi/10.1145/3779031.3779103

RESEARCH-ARTICLE

Bar Inductive Predicates for Constructive Algebra in Rocq

<figure><img src="image_3.png" /></figure>

Published: 08 January 2026

Citation in BibTeX format
# Bar Inductive Predicates for Constructive Algebra in Rocq

Dominique Larchey-Wendling

Université de Lorraine, CNRS, LORIA
Vandoeuvre-lès-Nancy, France
dominique.larchey-wendling@univ-lorraine.fr

## Abstract

In constructive commutative algebra, we revive the bar inductive characterization of Noetherian rings. We contribute the first constructive (axiom free) implementation of Hilbert's basis theorem, in the Rocq proof assistant. We show that the polynomial ring $R[X]$ is Noetherian when the ring $R$ is Noetherian, without assuming any additional condition on $R$, like coherence or else strong discreteness. We also contribute and implement a new result, that Noetherian rings are closed under direct products, again without assuming any supplementary condition on rings. We study induction principles for Noetherian rings, and relate bar Noetherianity with some other constructive characterizations.

**CCS Concepts: • Theory of computation → Constructive mathematics; Type theory; Logic and verification.**

**Keywords:** Constructive algebra, Noetherian rings, bar inductive predicates, Hilbert's basis theorem, Rocq

**ACM Reference Format:**

Dominique Larchey-Wendling. 2026. Bar Inductive Predicates for Constructive Algebra in Rocq. In *Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '26)*, January 12–13, 2026, Rennes, France. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3779031.3779103

## 1 Introduction

Bar inductive predicates, which are linked to but should not be conflated with bar induction, are siblings to Acc(cessibility) predicates, the de facto approach to well-foundedness in the (constructive) Rocq standard library. Bar inductive predicates have been used successfully to give constructive and axiom free<fnref n="1" /> accounts of the FAN theorem [5, 9], Ramsey's theorem and Higman's lemma [8], and more generally of well quasi order (WQO) theory through the equivalent notion of inductive almost full (AF) relation [15, 30]. The accessibility

predicate and more generally, bar and cover inductive predicates, give a way to quantify over arbitrary sequences, including “lawless” sequences which are (constructively) beyond the reach of the type $N \to A$ of “lawlike” sequences, that are used in ascending (or descending) chain conditions [5, 16].

Using those predicates, one can work constructively, avoiding excluded middle (XM) and dependent choice (DC). Coquand&Persson [7] exploit bar inductive predicates beyond WQO theory and apply them to constructive algebra, giving a bar predicate characterization of Noetherian rings. This allows them to prove Hilbert's Basis Theorem (HBT) constructively, moreover *free of any further assumption on the rings* like coherence or else strong discreteness (or both) [6], or variants of these notions [13, 18–20, 24]. The focus of [7] is a certified algorithm for Gröbner bases and the proof of the HBT was only outlined on paper, and not implemented. Despite this initial promising result – a nice and short constructive proof of the HBT, – the bar predicate approach to Noetherianity apparently did not get much traction later on. And, up to now, despite many constructive variants of the HBT, it seems that none of them have actually been implemented in constructive theorem provers, as opposed to classical versions of the theorem, see e.g. [22] but the HBT can also be found in the Mathlib Lean library<fnref n="2" />.

In this work, we propose to follow those footsteps [7] and revive the bar predicate approach to Noetherian rings with a first constructive implementation of the HBT in Rocq, revisiting their pen&paper proof, and also explaining why, in our opinion, that implementation work might have been out of reach at the time [21]. As a second contribution, we adapt the bar inductive proof of Ramsey's theorem [8] and derive a new result: Noetherian rings are closed under direct products, constructively, *without assuming strong discreteness*, as opposed to e.g. [24]. With a Rocq implementation as well.

### 1.1 Noetherian Rings in Constructive Algebra

We work with commutative rings of which we assume the theory for now. Recall that ideals are subsets of rings closed under linear combinations. An ideal is *finitely generated* if there is a list of its members generating the whole ideal by linear combinations. An ideal is *principal* if it is generated by a singleton. We focus our work on those properties of ideals.

<figure><img src="image_4.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

CPP '26, Rennes, France

© 2026 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-2341-4/2026/01

https://doi.org/10.1145/3779031.3779103

<footnote n="1">¹in particular, without assuming “Brouwer’s thesis” [29].</footnote>

<footnote n="2">²https://leanprover-community.github.io/mathlib-overview.html</footnote>
In classical algebra, a *principal ring* has only principal
ideals: typical examples include the ring of integers $\mathbb{Z}$ or the
ring $\mathcal{F}[X]$ of univariate polynomials over a field $\mathcal{F}$. However
$\mathcal{F}[X, Y]$ or $\mathbb{Z}[X]$ are not principal rings. They are nonethe-
less *Noetherian rings* where every ideal is finitely generated.
The original statement of the HBT was:

$\mathcal{F}[X_1, \dots, X_n]$ is a Noetherian ring if $\mathcal{F}$ is a field

and its initial proof, given by David Hilbert [12], was al-
legedly qualified as “theology” by Paul Gordan<fnref n="3" /> because of
its nonconstructive nature. Later on the HBT was given the
following, more general form:

if $\mathcal{R}$ is a Noetherian ring then so is $\mathcal{R}[X]$

and it became the usually accepted formulation of the HBT
in constructive algebra, however with a mandatory update
of the definition of “Noetherian ring.”

Indeed, to convert the HBT to constructive algebra, one
has first to acknowledge that the notions of principal or
of Noetherian ring, as defined classically above, are *useless*
when interpreted in constructive contexts. In intuitionistic
logic (w/o XM), there are too many propositions and hence,
too many subsets and ideals. And with such classical defini-
tions, if one can show that the ring $\mathbb{Z}$ (or even just $\mathbb{Z}/2\mathbb{Z}$) is
Noetherian (all the more principal), then this entails XM. This
observation is often recalled in papers about constructive
algebra, and can be made in Bishop's constructive mathemat-
matics [18] or in type theory, as we explain in Section 2.2.
So one cannot prove that those basic rings are principal or
even Noetherian unless one assumes XM. When working in
an anticlassical setting, where XM is actually refuted by the
assumption of other axioms, one can even show that $\mathbb{Z}$ and
$\mathbb{Z}/2\mathbb{Z}$ are not Noetherian.

Hence, constructively, the classical characterizations of
principal and Noetherian rings are usually considered flawed
and this has given rise to a large body of work with several
competing definitions. The notion of principal ring can be
replaced by the notion of Bezout domain: every finitely gen-
erated ideal is principal, see e.g. [6]. The constructive notion
of Noetherian ring has been given several variations:

**RS-Noetherian:** any infinite increasing sequence of finitely generated ideals pauses, by Richman [23] and Seidenberg [25];

**ML-Noetherian:** strict reverse inclusion is (Martin-Löf) well-founded on finitely generated ideals [13];<fnref n="4" />

**Strongly Noetherian:** finitely generated ideals ordered by strict inclusion are (explicitly) embedded into an well-ordered set [18];

**Bar Noetherian:** growing finite sequences of finitely generated ideals unavoidably reach a pause, expressed using a bar inductive predicate [7], the one we work with herein;

not claiming exhaustivity for this list.

All these characterizations of Noetherian rings are equiv-
alent to the classical one in a classical context, e.g. assum-
ing XM and DC, but in constructive contexts, they are not
equivalent although they may be related modulo some extra
hypotheses on rings like coherence or strong discreteness:

* a *coherent ring* is one where the ideal of solutions of systems of linear equations is generated by finitely many such solutions, see e.g. [6, 18];

* a *discrete ring* is one where 0 can be discriminated from the other elements. Equivalently, any two elements can be proved either identical or different;

* a *strongly discrete ring* is one where membership in finitely generated ideals is (constructively) decidable, see e.g. [24]. A stronger requisite is to assume that those rings have a “membership algorithm” [13] (for finitely generated ideals), or, in the terminology of [18], that they have “detachable ideals.” Strongly discrete rings are automatically discrete.<fnref n="5" />

Considering the HBT, [23, 25] show that “if $\mathcal{R}$ is coherent and RS-Noetherian then so is $\mathcal{R}[X]$.” [13] proves that “if $\mathcal{R}$ is ML-Noetherian, coherent and strongly discrete then so is $\mathcal{R}[X]$.” On the other hand, [7] gives a proof that “if $\mathcal{R}$ is bar Noetherian then so is $\mathcal{R}[X]$.” Moreover, there, they do not even assume discreteness of the ring.

We see that bar inductive predicates allow an orthogonal
treatment of Noetherianity and coherence or strong discrete-
ness, at least with respect to the HBT. We confirm this ob-
servation with a original proof that (bar) Noetherian rings
are closed under direct products, again w/o assuming strong
discreteness, contrary to the Proposition 13 and Theorem 14
of [24] where a similar result is obtained for strongly discrete
RS-Noetherian rings. With this work, we hope to revive the
interest for bar inductive predicates in constructive algebra
and beyond.

## 1.2 Contents of the Paper

In Section 2, we define rings using setoids, types equipped
with a pending quotient, so we can confirm by an implemen-
tation the most general form of the HBT stated in [7]. Indeed,
when we do not assume discreteness for rings, polynomials
cannot be given a normal form, so we work with rings up to
the equivalence relation given in the setoid. We define ideals,
and give two characterizations of finitely generated ideals.
We discuss the shortcomings of the classical characteriza-
tions of Noetherian rings and of principal rings in construc-
tive type theory. We introduce bar inductive predicates and,
based on the definition of pausing lists, following [7], we
characterize (bar) Noetherian rings. Using Bezout, we show
that $\mathbb{Z}$, the ring of integers, is Noetherian.

In Section 3, we present our original proof that the direct product of two Noetherian rings is a Noetherian ring, that

<footnote n="3">³b.t.w. Paul Gordan was also the later advisor of Emmy Noether.</footnote>

<footnote n="4">⁴recall the Definition 3.4 of ML-Noetherian rings in [13] additionally assumes that those rings are coherent with a membership algorithm.</footnote>

<footnote n="5">⁵One discriminates 0 using the ideal generated by the empty set.</footnote>
we obtain by reworking and adapting a former proof of a constructive interpretation of Ramsey's theorem [8]. We explain this adaptation and where the two proofs diverge.

In Section 4, we explain how we implement the polynomial ring, discuss alternatives, and give the categorical characterizations of polynomial rings. We formulate and show a critical observation that allows updates on finitely generated ideals of univariate polynomial rings, used in base case of the short (but sophisticated) inductive proof of the HBT.

In Section 5, we detail the first implementation of a constructive proof of the HBT, revisiting the pen&paper outline of [7]. We use the above updates and a tailored lexicographic induction principle.

In Section 6, we derive well-founded induction principles for (bar) Noetherian rings and compare that notion with the alternate constructive characterizations of RS- and ML-Noetherian rings, when assuming strongly discrete rings.

In Section 7, we focus on implementation choices. From our experience, we elaborate on why the implementation work for the HBT might have been unsuccessful (or avoided) at the time of [7, 21]. We also discuss recent approaches for uni- and multivariate polynomials over rings, as possible alternatives to our own setoid based implementation.

The results contained in this paper are backed by an axiom free RocQ artifact distributed under the MPL v2.0 free software license at:

https://github.com/DmxLarchey/Hilbert-Basis-Theorem/blob/1.0

Consult the README.md file for compile and code review instructions.

## 1.3 RocQ Preliminaries

We briefly recall the basics of RocQ's inductive type theory which distinguishes (logical) propositions in the type Prop (denoted $\mathbb{P}$ for short) and computational contents in the type hierarchy Type. We assume arithmetic using the type of Peano natural numbers $\mathbb{N}$ and lists in list A, polymorphic over a carrier type A. Using $a, b$ for values of type A and $l, m$ for values in list A, we write $[]$ for the empty list, $a::l$ (resp. $l+m$) for the consing of a head element (resp. appending lists) as defined in the List module. We write $[a_0; \dots ; a_{n-1}]$ for enumerated lists, and $[a]$ for singletons<fnref n="6" />. Recall the identity $a::l = [a] + l$ that holds by definition. We write $|l|$ for the length of the list $l$, and $a \in l$ for the membership predicate, with which we define the carrier of a list $[l] : A \to \mathbb{P}$ as $[l] := \lambda a, a \in l$, and which collects its elements in a subset.

We denote $P, Q$ for subsets viewed as predicates in $A \to \mathbb{P}$, and $R, T$ for binary relations in $A \to B \to \mathbb{P}$. We use the standard $\subseteq$ notation for either unary or binary predicate inclusion, and write $\equiv$ for extensional equivalence, hence for instance, $[l] \subseteq P$ means that all the members of $l$ satisfy property $P$, and $[l] \equiv [m]$ means that the two lists have the

same members. We use the same notations in the RocQ code, there possibly subscripted by arities like in $\subseteq_2$ or $\equiv_1$.

We manipulate finite sets as predicates $P: A \to \mathbb{P}$ s.t. $P = [l]$ holds for some list $l$, i.e. listable predicates. In the prose, when we define inductive predicates, we use visual rules, as premises above a conclusion, instead of RocQ's Inductive statements, hoping they are easier to grasp in this form. Free named parameters (or indices) should then be understood as universally quantified over.

# 2 Rings and Ideals in Constructive Algebra

We work in commutative algebra and do not consider the non-commutative case herein. We recall the definition of rings and ideals, and discuss the shortcomings of the classical characterizations of principal and Noetherian rings in constructive type theory. We introduce bar inductive predicates and define (bar) Noetherian rings with them.

To avoid foundational issues related to quotients in RocQ, or else avoid assuming rings to be discrete, we use the Setoid framework [26] for generalized rewriting and hence use a congruence in place of the identity relation to represent ring equations. We will discuss this choice in more details in Section 4 when dealing with polynomial rings.

A ring is a structure $\mathcal{R} = (\mathcal{R}, +, -, \times, 0, 1, \sim)$ where $\mathcal{R}$ is a type, $(\mathcal{R}, +, -, 0, \sim)$ is a commutative group forming the additive part of the ring ($-$ is the additive inverse operator), while $(\mathcal{R}, \times, 1, \sim)$ is a commutative monoid forming the multiplicative part of the ring. Last, $\times$ distributes over $+$. A (discrete) field is a ring where every value is either equivalent to 0 or has a multiplicative inverse.<fnref n="7" /> Notice the equivalence relation $\sim$ that is required to be a congruence for $+, -, \times$, and moreover, the monoids laws and the distributivity law should be understood up to this equivalence. So for instance the distributivity law becomes $z \times (x+y) \sim z \times x + z \times y$, with the usual precedence of $\times$ over $+$ for these infix notations.

RocQ allows to define such a dependent type ring as Record structure and overload the notation $\mathcal{R}$ which can be interpreted both as a ring structure or as the carrier type for the elements of the ring $\mathcal{R}$ and we make use of the facility in the file ring.v. In our implementation, we decorate the ring operators and the equivalence with a suffix "r" as in e.g. $+_r$ to avoid ambiguity with operations on natural numbers. We do not do this in the paper and hope ambiguities can easily be avoided. RocQ however might need to infer which ring do the operators refer to. Often this is solved by the context and unification: if $x: \mathcal{R}$ then RocQ infers that $+$ and $0$ refer to the ring $\mathcal{R}$ in the expression $x+0$. However, the expression $0+1 \sim 1$ is ambiguous for RocQ and we sometimes have to hint it to the proper ring through type annotations like e.g. $(0: \mathcal{R}) + 1 \sim 1$, provided $\mathcal{R}: \text{ring}$ belongs to the context.

Additionally, we exploit the instruments of the Ring and Setoid modules (which where designed to work together),

<footnote n="6">⁶Enumerated lists are mostly used in the prose for reader friendliness.</footnote>

<footnote n="7">⁷The assumption $\forall x, x \sim 0 \lor \exists i, i \times x \sim 1$ entails discreteness.</footnote>
so that solving ring equations $e_1 \sim e_2$ and rewriting expressions up to $\sim$ becomes effortless. One simply declares ring operators as Morphisms and subscribes rings to the Ring module to exploit these instruments in the local context.

A ring homomorphism is a map between two rings preserving congruences, addition and multiplication operators, and the multiplicative unit 1. As a consequence, they also preserve $-$ and 0. ring sub-homomorphisms have a relaxed definition and do not have to preserve the unit 1, but instead they preserve the unit 0 (hence also $-$). Forming a quotient ring in the context of setoids is straightforward: for the ring $(\mathcal{R}, +, -, \times, 0, 1, \sim)$, one simply picks up a new congruence $\sim'$ which over approximates $\sim$ (i.e. $\sim \subseteq \sim'$), and then one updates $\sim$ with $\sim'$ in the structure. The identity map $(\mathcal{R}, +, -, \times, 0, 1, \sim) \to (\mathcal{R}, +, -, \times, 0, 1, \sim')$ automatically becomes a surjective ring homomorphism on the quotient.

## 2.1 Ring Ideals

Ring ideals are a fundamental notion of algebra. They are the kernels of ring homomorphisms. An ideal of a ring $\mathcal{R}$ is a subset $\mathcal{I} : \mathcal{R} \to \mathbb{P}$ of $\mathcal{R}$ containing 0 (i.e. $\mathcal{I} 0$) and closed under $\sim$ (i.e. $\forall x y : \mathcal{R}, x \sim y \to \mathcal{I} x \to \mathcal{I} y$), addition/$+$ (i.e. $\forall x y : \mathcal{R}, \mathcal{I} x \to \mathcal{I} y \to \mathcal{I} (x + y)$) and scalar products (i.e. $\forall a x : \mathcal{R}, \mathcal{I} x \to \mathcal{I} (a \times x)$). We skip the obvious RocQ definition here but we denote ideal $\mathcal{I}$ for the proposition stating that $\mathcal{I}$ is an ideal of the ring $\mathcal{R}$.<fnref n="8" /> That definition and the constructions and results we describe and claim below are implemented in the file ideal.v.

We are especially interested in ideals that are generated by some elements, in particular finitely many of them, and how to handle these. Given a subset $P : \mathcal{R} \to \mathbb{P}$ of $\mathcal{R}$, we define $\mathrm{idl} P : \mathcal{R} \to \mathbb{P}$ inductively using the following rules:

$$ \begin{array}{ccc} \frac{x \sim y}{\mathrm{idl} P y} & \mathrm{idl} P x & \frac{P x}{\mathrm{idl} P x} \\ \frac{\mathrm{idl} P x}{\mathrm{idl} P (x+y)} & \mathrm{idl} P y & \frac{\mathrm{idl} P x}{\mathrm{idl} P (a \times x)} \end{array} $$

and we (obviously) obtain the smallest ideal containing $P$, i.e. the ideal generated by $P$. Notice that the definition of $\mathrm{idl} P x$ proceeds by analysis of the algebraic structure of $x$.

Alternatively, for a list $l : \mathrm{list} \mathcal{R}$, we define $\mathrm{lc} l : \mathcal{R} \to \mathbb{P}$ ($\mathrm{lc}$ stands for linear combination) inductively with the rules:

$$ \frac{0 \sim x}{\mathrm{lc} [] x} \qquad \frac{a \times x + z \sim y}{\mathrm{lc} (x :: l) y} \qquad \mathrm{lc} l z $$

following the structure of the list $l$ (rather than that of $x$) and then $\mathrm{lc} l$ is the smallest ideal containing the members of $l$. Indeed, we show the (extensional) identity

$$ \mathrm{idl} [l] \equiv \mathrm{lc} l \quad \text{for any } l : \mathrm{list} \mathcal{R} \quad (1) $$

i.e. the subsets $\mathrm{idl} [l]$ and $\mathrm{lc} l$ of $\mathcal{R}$ contain the same members. They are finitely generated ideals, as they are generated by the members of a (finite) list of values. As a side remark, we can generalize the correspondence between $\mathrm{idl}$ and $\mathrm{lc}$ to a subset $P : \mathcal{R} \to \mathbb{P}$ with the following equivalence

$$ \mathrm{idl} P x \leftrightarrow \exists l, [l] \subseteq P \wedge \mathrm{lc} l x \quad \text{for any } x : \mathcal{R} $$

but we will not use it herein. We generally favor writing $\mathrm{idl} [l]$ over the equivalent $\mathrm{lc} l$ because it is more evocative.

**Definition 2.1.** Let $\mathcal{I} : \mathcal{R} \to \mathbb{P}$ be an ideal of the ring $\mathcal{R}$. $\mathcal{I}$ is a finitely generated ideal when there exists $l : \mathrm{list} \mathcal{R}$ such that $\mathcal{I} \equiv \mathrm{idl} [l]$. It is a principal ideal when there exists $g : \mathcal{R}$ such that $\mathcal{I} \equiv \mathrm{idl} [[g]]$.

A ring is Bezout if all finitely generated ideals are principal. A ring is strongly discrete if finitely generated ideals are (logically) decidable sets, i.e. $\forall l x$, $\mathrm{idl} [l] x \lor \neg \mathrm{idl} [l] x$.

Notice that the definition we give for strong discreteness is weaker than the generally understood one, which interprets “decidable” in a computational way (see Sections 1.1 and 6).

## 2.2 Shortcomings of Classical Definitions

In classical contexts (e.g. under XM and DC), all the ideals of $\mathbb{Z}$ and $\mathcal{F}[X]$ (for a field $\mathcal{F}$) are principal. But, $(\mathbb{Z}/m\mathbb{Z})[X]$ (with $m$ composite), $\mathbb{Z}[X]$ and $\mathcal{F}[X, Y]$ all have non-principal ideals. They are however classically Noetherian in the sense that all their ideals are finitely generated. In this section, we explain why the classical characterizations of principal and Noetherian rings are inappropriate in constructive type theory, see file noetherian_nc.v.

Consider any ring $\mathcal{R}$ which is discrete (i.e. $\forall x : \mathcal{R}, x \sim 0 \lor x \not\sim 0$), and non-trivial (i.e. $0 \not\sim 1$). Typically, the ring $\mathbb{Z}$ (or even just $\mathbb{Z}/2\mathbb{Z}$) fits these two requirements. Let us fix an arbitrary proposition $P : \mathbb{P}$ and form the ideal $\mathcal{I}_P : \mathcal{R} \to \mathbb{P}$ defined by $\mathcal{I}_P x := x \sim 0 \lor P$. If $\mathcal{I}_P$ is finitely generated (a fortiori principal), then one can show $P \lor \neg P$. Indeed, let us assume a list $l$ s.t. $\mathcal{I}_P \equiv \mathrm{idl} [l]$. We discriminate between $\forall x, x \in l \to x \sim 0$ and $\exists x, x \in l \land x \not\sim 0$, which is possible because $\mathcal{R}$ is discrete and $l$ is a (finite) list. In the former case, we have $\mathcal{I}_P x \leftrightarrow \mathrm{idl} [l] x \leftrightarrow x \sim 0$, hence $\neg \mathcal{I}_P 1$. As a consequence, $\neg P$ holds. In the later case, there is $x \in l$ s.t. $x \not\sim 0$, hence $\mathcal{I}_P x$ holds, so $x \sim 0 \lor P$ and this entails $P$.

So if the ring $\mathcal{R}$ is classically Noetherian (a fortiori principal), then the ideal $\mathcal{I}_P$ is finitely generated and thus $P \lor \neg P$ holds. And this for any proposition $P : \mathbb{P}$. If we can prove that e.g. the ring of integers $\mathbb{Z}$ is Noetherian or principal in the classical understanding, then XM must hold and we are out of constructive logic. This renders these classical understandings inappropriate in constructive algebra.

## 2.3 Bar Noetherian Rings

The above observation led to a wide range of alternative characterizations of Noetherian rings to fit constructive contexts, see e.g. [18]. We do not discuss them in detail here, see

<footnote n="8">⁸The first argument $\mathcal{R}$ of ideal $\{\mathcal{R} : \mathrm{ring}\} (\mathcal{I} : \mathcal{R} \to \mathbb{P})$ is implicit.</footnote>
Section 6 for some comparisons. We rather directly introduce the bar predicate characterization used in [7].

**2.3.1 Bar Inductive Predicates.** Given a type A and a predicate P : listA → P, we define bar P : listA → P with the two inductive rules/constructors:

$$ \frac{\mathit{Pl}}{\mathit{bar} \mathit{Pl}} \qquad \frac{\forall a, \mathit{bar} \mathit{P} (a :: l)}{\mathit{bar} \mathit{Pl}} $$

bar predicates are linked to bar induction but do not require extra axioms by themselves, unlike Brouwer's bar theorem (see below). We recall the induction principle associated with bar predicates because we are going to use it extensively:

**Proposition 2.2 (Induction on bar predicates).** Assume P : listA → P and a property K : listA → P. To establish

$$ \forall l, \mathit{bar} \mathit{Pl} \to Kl $$

it is sufficient to prove:

1. $\forall l, \mathit{Pl} \to Kl$;

2. $\forall l, (\forall a, \mathit{bar} \mathit{P} (a :: l)) \to (\forall a, K (a :: l)) \to Kl$.

Rocq generates the principle on its own as a Fixpoint structural on the proof of bar P l. The first induction hypothesis $\forall a, \mathit{bar} \mathit{P} (a :: l)$ of item 2 is rarely needed, except in the proof in the mutual principle of Proposition 2.3. In the file bar.v, we collect basic results about bar predicates and highlight some of these below, where P, Q : list_ → P.

We give an intuitive understanding of bar P [] with

$$ \mathit{bar} \mathit{P} [] \to \forall \rho : \mathbb{N} \to A, \exists n, P [\rho_{n-1}; \dots; \rho_0] \quad (2) $$

In plain english, bar P [] entails that any sequence of shape $n \mapsto [\rho_{n-1}; \dots; \rho_0]$ unavoidably meets P, regardless of how it is extended by adding elements at its head. In the terminology of bar induction, P is barred. The characterization by sequences<fnref n="9" /> in $\mathbb{N} \to A$ is called Brouwer's bar theorem [5] and can be proved using XM and DC, or alternatively with the weaker intuitionistic principle called Brouwer's thesis [29]. Constructively however, universal quantification over sequences is weaker than bar P [] because the type $\mathbb{N} \to A$ does not account for lawless sequences [5, 16].

We show that bar is a mono(tonic) operator

$$ \forall P Q, P \subseteq Q \to \mathit{bar} P \subseteq \mathit{bar} Q \quad (3) $$

by a straightforward induction on bar P_; more generally, bar is a closure operator. We show the following equivalence

$$ \forall lr, \mathit{bar} \mathit{P} (l \oplus r) \leftrightarrow \mathit{bar} (\lambda p, \mathit{P} (p \oplus r)) l. \quad (4) $$

A predicate Q is monotone if $\forall al, Ql \to Q (a :: l)$. The bar operator preserves monotone predicates:

$$ \text{if } P \text{ is monotone then so is bar } P. \quad (5) $$

One observation that was made in [7] and which is used in the proof of the HBT in Section 5.3 is the following: if P is closed under insertion then so is bar P, or more formally:

$$ \begin{aligned} & (\forall lr, P (l \oplus r) \to P (l \oplus m \oplus r)) \\ & \to (\forall lr, \mathit{bar} P (l \oplus r) \to \mathit{bar} P (l \oplus m \oplus r)) \end{aligned} \quad (6) $$

for any $m : listA$, which is a generalization of the preservation of monotone predicates (5) by bar above.

In the Section 3, we will reason by mutual induction on two bar predicates using the following induction principle:

**Proposition 2.3 (Mutual induction on bar predicates).** Assume P : listA → P and Q : listB → P and a (mutual) property K : listA → listB → P. To establish

$$ \forall lm, \mathit{bar} \mathit{Pl} \to \mathit{bar} \mathit{Qm} \to Klm $$

it is sufficient to show:

1. $\forall lm, Pl \to Klm$;

2. $\forall lm, Qm \to Klm$;

3. $\forall lm, (\forall a, K (a :: l) m) \to (\forall b, K l (b :: m)) \to Klm$.

*Proof.* By nested induction, on bar P l, then on bar Qm. □

**2.3.2 Pausing Sequences.** Consider a sequence of finitely generated ideals $I_n := \text{idl} [[\rho_{n-1}; \dots; \rho_0]]$ of a ring $\mathcal{R}$. This sequence is increasing: $\forall n, I_n \subseteq I_{n+1}$. A pause in the sequence is an index $n$ where the associated ideal does not grow, i.e. $I_{n+1} \subseteq I_n$, or equivalently $\text{idl} [[\rho_{n-1}; \dots; \rho_0]] \rho_n$. By Equation (1), at that point, $\rho_n$ is a linear combination of the previous values in the sequence.<fnref n="10" />

**Definition 2.4 (Pausing lists).** Given a list $m : list\mathcal{R}$, we say that $m$ pauses and write PAm if:

$$ \mathrm{PAm} := \exists l x r, m = l \oplus [x] \oplus r \wedge \mathrm{idl} [r] x. $$

Looking for the pause $x$ in the middle of $m$ rather than just at its head ensures that PA is a monotone predicate. In the file noetherian.v, we favor an inductive definition for PA for shorter Rocq proofs, but we nevertheless establish the equivalence with the above given (first order) Definition 2.4 of PA. We study the PAm property when $m$ already has a given structure, e.g. PA ($l \oplus [x] \oplus r$) holds iff

* either $l = l' \oplus [y] \oplus m$ and $\text{idl} [m \oplus [x] \oplus r] y$ hold for some $l', m : list\mathcal{R}$ and $y : \mathcal{R}$, meaning that the pause occurs in $l$;

* or $\text{idl} [r] x$ (the pause occurs at $x$);

* or PAr (the pause occurs in $r$).

We show that PA is closed under arbitrary insertions:

$$ \forall l m r, \mathrm{PA} (l \oplus r) \to \mathrm{PA} (l \oplus m \oplus r) $$

which by (6) entails the same property for bar PA:

$$ \forall l m r, \mathit{bar} \mathit{PA} (l \oplus r) \to \mathit{bar} \mathit{PA} (l \oplus m \oplus r) \quad (7) $$

Additionally PA is closed under ring sub-homomorphisms.

<footnote n="9">⁹meaning, as a logical equivalence instead of an implication in Equation (2).</footnote>

<footnote n="10">¹⁰Richman [23] and Seidenberg [25] characterize RS-Noetherian rings this way: any increasing sequence of finitely generated ideals contains a pause.</footnote>
**Proposition 2.5.** Let $\mathcal{R}$ and $\mathcal{T}$ be two rings and $\varphi : \mathcal{R} \to \mathcal{T}$ be a sub-homomorphism. The entailment $\mathbf{PA} l \to \mathbf{PA}(\varphi l)$ holds for any $l : \mathbf{list} \mathcal{R}$, where we simply write $\varphi l$ for map $\varphi l$.

**2.3.3 Noetherian Rings.** Following [7], we characterize the pausing of increasing sequences of finitely generated ideals using a bar predicate. The definitions and results below can be reviewed in the file noetherian.v.

**Definition 2.6 (Noetherian ring).** We say that a ring $\mathcal{R}$ is (bar) Noetherian and write noetherian $\mathcal{R}$ if:

$$ \text{noetherian } \mathcal{R} := \text{bar} (@\mathbf{PA}\mathcal{R}) \text{ ]} $$

where @PA$\mathcal{R}$ is a RocQ notation to specify the otherwise implicit argument $\mathcal{R}$ of PA.

Notice that [7] employs the term “Good” instead “pauses” but we favor terminology from constructive algebra rather than importing one we find a bit specific to WQO theory.

Since bar PA [] entails that PA is barred (2), any sequence $n \mapsto \text{idl} \llbracket \rho_{n-1} : \dots : \rho_0 \rrbracket$ pauses in a Noetherian ring.<fnref n="11" /> Finite rings are Noetherian. Noetherian rings are closed under surjective homomorphisms and quotients. In particular,

(bar) Noetherian rings are closed under isomorphism.

To show that $\mathbb{Z}$ is Noetherian, we prove the following:

**Theorem 2.7.** Consider a Bezout ring $\mathcal{R}$ where divisibility is (logically) decidable and strict divisibility is a well-founded relation. Then $\mathcal{R}$ is (bar) Noetherian.

*Proof.* In a Bezout ring every finitely generated ideal is generated by a singleton. We write $x | y := \exists k, k \times x \sim y$ for divisibility and $x |_s y := x | y \land y \nparallel x$ for strict divisibility which are both logically decidable binary relations. We show

$$ \forall gl, \text{idl}[l] \equiv \text{idl}[\llbracket g \rrbracket] \to \text{bar PA}l \quad (8) $$

by induction on $g$ using the well-founded strict divisibility relation $|_s$. The induction hypothesis is:

$$ IH : \forall e, e |_s g \to \forall l, \text{idl}[l] \equiv \text{idl}[e] \to \text{bar PA}l $$

and assuming $l$ s.t. $\text{idl}[l] \equiv \llbracket g \rrbracket$, we need to prove bar PA $l$. We apply the second constructor of bar and hence pick any $x$ and the goal becomes bar PA ($x :: l$). By Bezout, we get $e$ s.t. $\text{idl}[x :: l] \equiv \llbracket e \rrbracket$. From $\text{idl}[x :: l]g$ we deduce $e | g$. We discriminate between $g | e$ or $g \nparallel e$:

* in the former case, we have $\text{idl}[x :: l] \equiv \text{idl}[e] \equiv \text{idl}[\llbracket g \rrbracket] \equiv \text{idl}[l]$ and then $\text{idl}[l]x$, so $x :: l$ pauses;

* in the later case, we have $e |_s g$ and we apply $IH$ and immediately get the goal bar PA ($x :: l$).

Having proved Statement (8), we then instantiate it on $g := 0$ and $l := []$, and derive that bar PA [] holds. □

**Corollary 2.8.** The ring $\mathbb{Z}$ of integers is (bar) Noetherian.

# 3 The Direct Product is a Noetherian Ring

As we consider it an original theoretical contribution of our work, we give a quite detailed account for the below result:

**Theorem 3.1.** If $\mathcal{R}$ and $\mathcal{T}$ are Noetherian rings then so is their direct product $\mathcal{R} \times \mathcal{T}$.

## 3.1 The Origins of the Proof

In [24], a weaker result is established for RS-Noetherian rings; they further assume that $\mathcal{R}$ (or $\mathcal{T}$) is a strongly discrete ring. Their proof reminded us of that of Dickson's lemma, which itself classically follows from Ramsey's theorem. This translates constructively using a different statement of Ramsey's theorem: the direct product of two WQOs is a WQO, where WQOs are interpreted as AF relations [30].

We rather started from [8] because it is based on an equivalent bar characterization of AF relations for its statement of Ramsey's theorem. We simplified that proof in the hope of being able to adapt it to the context of algebra.<fnref n="12" /> It turned out that we could indeed convert this simplified proof and establish our intended result w/o assuming strong discreteness. The file product_noetherian.v mechanizes this new result and we now give an overview of the arguments. Of course we first need to give an explicit construction of the direct product ring $\mathcal{R} \times \mathcal{T}$ (in product.v) and show that this construction is correct in the sense of category theory, as the terminal object in the category of product diagrams (see category.v). We do not elaborate on these standard considerations here.

## 3.2 The Detailed Account

Turning to the statement of Theorem 3.1, we want to show

$$ \begin{align} \text{bar}(@\mathbf{PA}\mathcal{R}) \text{ ]} &\to \text{bar}(@\mathbf{PA}\mathcal{T}) \text{ ]} \nonumber \\ &\to \text{bar}(@\mathbf{PA}(\mathcal{R} \times \mathcal{T})) \text{ ]} \tag{9} \end{align} $$

but unfolded as such, induction would eventually lead to a dead end.<fnref n="13" /> So following the scheme of [8], we first generalize the statement to

$$ \forall lx ly, \text{bar PA}lx \to \text{bar PA}ly \to \text{bar} (\theta lx ly) \text{ ]} \quad (10) $$

where $\theta : \mathbf{list} \mathcal{R} \to \mathbf{list} \mathcal{T} \to \mathbf{list} (\mathcal{R} \times \mathcal{T}) \to \mathbb{P}$ must be wisely chosen. However [8] has an overly complex way of describing $\theta$ and a critical aspect of our work was to give it a much nicer form. Skipping the details, we ended up with the following simple definition for our adaptation:

$$ \theta lx ly l := \text{PA}(l + \varphi lx + \psi ly) $$

<footnote n="11">¹¹but this is not exactly the same as RS-Noetherian, see Section 6.</footnote>

<footnote n="12">¹²The auxiliary file ramsey.v records that reworked proof.</footnote>

<footnote n="13">¹³Because in bar (@PA$\mathcal{R}$) [], the non-uniform parameter is constrained, here as the particular list [], which the induction tactic would first generalize, thereby forgetting its specific shape. On the other hand, in statement (10), the parameter $lx$ is an unconstrained list corresponding to the default induction principle (of Proposition 2.2) for bar (@PA$\mathcal{R}$) $lx$, as well as the mutual one (of Proposition 2.3) that we end up using.</footnote>
where $\varphi(x : \mathcal{R}) := (x, 0)$ and $\psi(y : \mathcal{T}) := (0, y)$, both output values belonging to the ring $\mathcal{R} \times \mathcal{T}$. Clearly, $\varphi$ and $\psi$ are ring sub-homomorphisms. Additionally, we write $\pi_1 : \mathcal{R} \times \mathcal{T} \to \mathcal{R}$ and $\pi_2 : \mathcal{R} \times \mathcal{T} \to \mathcal{T}$ for the canonical projections $\pi_1(x, y) := x$ and $\pi_2(x, y) := y$ which are ring homomorphisms.

The predicate $\theta lx ly$ being based on PA, it is monotone and so is bar $(\theta lx ly)$. When $lx$ and $ly$ are empty lists then $\theta [] [] l$ is identical to PA $l$. Hence statement (10) instantiates to statement (9) with that empty assignment for $lx$ and $ly$, exactly the unfolding of Theorem 3.1.

To prove statement (10), we proceed by mutual induction using Proposition 2.3. It is enough to show:

1. bar $(\theta lx ly) []$ assuming PA $lx$;

2. bar $(\theta lx ly) []$ assuming PA $ly$;

3. bar $(\theta lx ly) []$ assuming $\forall x$, bar $(\theta (x :: lx) ly) []$ and $\forall y$, bar $(\theta lx (y :: ly)) []$.

For item 1, if $lx$ pauses then so does $[] :: \varphi lx :: \psi ly$ because $\varphi$ is a sub-homomorphism. Hence $\theta lx ly []$ holds and we get bar $(\theta lx ly) []$ using the first constructor for bar. A similar argument applies when $ly$ pauses (item 2).

The difficult case is item 3 for which we need to show bar $(\theta lx ly) []$ under two induction hypotheses. We first apply the second constructor for bar. We fix an arbitrary $z : \mathcal{R} \times \mathcal{T}$ and we now need to establish the goal bar $(\theta lx ly) [z]$. We instantiate our two induction hypotheses on $\pi_1 z / \pi_2 z$ as

$$IH_1 : \bar{\text{bar}}(\theta(\pi_1 z :: lx) ly) [] \quad IH_2 : \bar{\text{bar}}(\theta(lx \pi_2 z :: ly)) []$$

and, to achieve the goal bar $(\theta lx ly) [z]$, we prove the generalized statement

$$\forall m, \bar{\text{bar}}(\theta lx (\pi_2 z :: ly)) m \to \bar{\text{bar}}(\theta (\pi_1 z :: lx) ly) m \\ \to \bar{\text{bar}}(\theta lx ly) (m \oplus [z]) \quad (11)$$

that, for $m := []$, in combination with our two instances $IH_1$ and $IH_2$, delivers us the required conclusion bar $(\theta lx ly) [z]$ for completing the proof of item 3.

So far, we followed a script similar to our adaptation of the proof of Ramsey's theorem [8], except of course for our definition of $\theta$ which is novel. However, the arguments we now use to establish (11) largely diverge from that script.

**Proof of statement (11).** In a first phase, we observe that

$$\mathrm{idl} [ly] (\pi_2 z) \to \theta (\pi_1 z :: lx) ly m \to \theta lx ly (m \oplus [z]) \quad (12)$$

holds. Indeed, the second hypothesis states that there is a pause in $m \oplus [\varphi(\pi_1 z) :: \varphi lx :: \psi ly]$ and we analyze this situation. If the pause occurs in either $m$ or $\varphi lx$ or $\psi ly$, then there is a corresponding pause in $m \oplus [z] :: \varphi lx :: \psi ly$ because $\varphi(\pi_1 z) \sim (1, 0) \times z$. If the pause occurs at $\varphi(\pi_1 z)$ (the delicate case), then we have $\mathrm{idl} [\varphi lx :: \psi ly] \varphi(\pi_1 z)$. But since we assume $\mathrm{idl} [ly] (\pi_2 z)$, we get $\mathrm{idl} [\psi ly] \psi(\pi_2 z)$ by Proposition 2.5. We deduce $\mathrm{idl} [\varphi lx :: \psi ly] \psi(\pi_2 z)$ by inclusion of lists. From the equation $z \sim \varphi(\pi_1 z) + \psi(\pi_2 z)$ we finally get $\mathrm{idl} [\varphi lx :: \psi ly] z$ and thus $m \oplus [z] :: \varphi lx :: \psi ly$ pauses. This concludes the proof of statement (12).

Because bar is monotonic (3), we derive

$$\mathrm{idl} [ly] (\pi_2 z) \to \bar{\text{bar}} (\theta (\pi_1 z :: lx) ly) m \\ \to \bar{\text{bar}} (\theta lx ly) (m \oplus [z]) \quad (13)$$

from Observation (12), also using Equivalence (4).

In a second phase, we can deal with the proof of (11). We proceed by induction on bar $(\theta lx (\pi_2 z :: ly)) m$:

* in the base case, we have the hypotheses

$$H_1 : \theta lx (\pi_2 z :: ly) m \\ H_2 : \bar{\text{bar}} (\theta (\pi_1 z :: lx) ly) m$$

and we target the goal bar $(\theta lx ly) (m \oplus [z])$. We analyze the pause $H_1$ in $m \oplus \varphi lx \oplus [\psi(\pi_2 z) :: \psi ly]$. If the pause occurs in either $m$ or $\varphi lx$ or $\psi ly$ then there is a corresponding pause in $m \oplus [z] :: \varphi lx \oplus \psi ly$, which entails $\theta lx ly (m \oplus [z])$ hence our goal using the first constructor of bar.

While we omit some details about how to transfer the above pause, we instead put the focus on the delicate case where the pause is at $\psi(\pi_2 z)$, and in that case we have $\mathrm{idl} [\psi ly] \psi(\pi_2 z)$. Since $\pi_2 \circ \psi$ is the identity map, we deduce $\mathrm{idl} [ly] (\pi_2 z)$ by Proposition 2.5 (using $\pi_2$ as a sub-homomorphism). The situation now corresponds to Statement (13) that we established in the first phase, first phase which de facto implements a nested recursive call on bar $(\theta (\pi_1 z :: lx) ly) m$;

* in the recursive case, we have an hypothesis

$$H_2 : \bar{\text{bar}} (\theta (\pi_1 z :: lx) ly) m$$

and an additional induction hypothesis

$$\mathrm{IH} : \forall z', \bar{\text{bar}} (\theta (\pi_1 z :: lx) ly) (z' :: m) \\ \to \bar{\text{bar}} (\theta lx ly) (z' :: m \oplus [z])$$

and we have to establish the goal bar $(\theta lx ly) (m \oplus [z])$. We apply the second constructor of bar and hence we pick an arbitrary $z' : \mathcal{R} \times \mathcal{T}$ and prove

$$\bar{\text{bar}} (\theta lx ly) (z' :: m \oplus [z])$$

We apply the induction hypothesis $IH$ and the goal becomes bar $(\theta (\pi_1 z :: lx) ly) (z' :: m)$ which follows from hypothesis $H_2$ because bar $(\theta \_\_)$ is monotone.

This concludes our account of the proof of Theorem 3.1. $\square$

## 3.3 Discussion

The above proof might look a bit intricate, especially for those unfamiliar with inductive reasoning in general, or those troubled with the inductive formulation of bar predicates in particular. One might feel that it does not give a lot of intuition about what is going on. We argue that generalized inductive reasoning is hard to communicate on paper, especially for readers unused to its mechanics: many different statements, hypotheses or goals, need to be tracked down.

This feeling given by the pen&paper outline, reflecting the happy conclusion of a proof search process, is however quite
different from the experience of actually unfolding the proof
search process with the help of the RocQ proof assistant. In
particular, a lot of statements are inferred by the assistant
itself, which also largely supports the mechanics of apply-
ing induction principles. What remains difficult is to devise
which induction principle is best suited and which gener-
alization is required before performing induction. In the
dynamics of a proof, having an intuition about the “meaning”
of a specific bar statement is not as critical as being able to
pickup the “right” induction principle, reflecting some views
of John Von Neumann on the practice of mathematics.<fnref n="14" />

The proof script in the file product_noetherian.v was
designed to be human readable. Despite giving more details
than the above pen&paper account, it has a comparable size
and most sub proofs are shorter than 5 loc, with the excep-
tions of those of Statement (12) which is 12 loc (first phase),
and of Statement (11) which is 30 loc (second phase).

# 4 Construction of the Polynomial Ring

We now turn to the construction of the polynomial ring
which we discuss within this section. This construction is of
course critical in the implementation of the HBT because it
deals with polynomials. Notice that the choice we made for
our implementation of rings as setoids was also influenced by
the requirements of the construction of polynomial rings. See
also Section 7 for comparisons with alternative approaches
to polynomials over rings.

## 4.1 What is a Polynomial?

The notion of polynomial can be understood in contexts
much larger than ring algebra. In general, they can be viewed
as expressions built from values of the carrier algebra $\mathcal{A}$,
combined with (the syntactic counterparts of) algebraic op-
erators (given by a signature) and some unknowns in $U$. E.g.
for rings, an example could look like $(1 + X \times Y) \times (Y + Z)$.
One then defines the least congruence satisfying the alge-
braic laws (e.g. with an inductive predicate) and the quotient
forms the algebra of polynomials, denoted $\mathcal{A}[U]$. At this
level of abstraction there is no canonical representative of a
given expression: think of the Lindenbaum algebra for intu-
itionistic logic for instance. Even for rings where canonical
forms may exist, notions like degrees, head coefficients, or
monomials require *computing* canonical forms.

When introduced to students in algebra, polynomials in
the unknown $X$ over a ring $\mathcal{R}$ (often it is even a field) are
rather defined as formal expressions $x_0X^0 + x_1X^1 + \dots +
x_nX^n$, where $x_n$ must be nonzero.<fnref n="15" /> This gives a canonical
(and unique) form to the polynomial. But unless assuming
a discrete ring, it is not possible to ensure the existence of
a canonical form: computing the canonical representative

of the sum $P + Q$ where $P = \dots + aX^n$ and $Q = \dots + bX^n$
requires being able to discriminate $a + b$ from 0.

## 4.2 Polynomial Representations

This representation of polynomials as an ordered sequence
of monomials $x_0 + x_1 X + \dots + x_n X^n$ is assumed for the proof
of the HBT in [7], and generally, even classical proofs of the
HBT work with sum of (multivariate) monomials.

In our implementation file poly.v, instead of trying to
normalize arbitrary polynomial expressions into ordered
sequences, we view polynomial representations over a ring
$\mathcal{R}$ and (a single variable $X$) as lists $[x_0; \dots ; x_n]$ in $\mathcal{R}[X] :=
\text{list}\mathcal{R}$, however not requiring that $x_n$ is nonzero. That is
why we call them representations, and those are not unique.
E.g. $[x_0; x_1]$ and $[x_0; x_1; 0; 0]$ are two representations of the
same polynomial, but they are “identified” under a suit-
able congruence $\sim$. Using setoids is critical here because
we do not need to find the shortest representation, hence
the discreteness of $\mathcal{R}$ need not be assumed.<fnref n="16" /> Compared to
the C-CoRN library [17], we proceed similarly except that
they hardwire the list structure in the cpoly type: i.e. they
view the polynomial $x_0X^0 + x_1X^1 + x_2X^2$ in its Horner form
$x_0 + X(x_1 + X(x_2 + X.0))$. We favor lists in order to exploit
the generic tools of the List module, rather than having to
create a copy of that library specialized on cpoly.

The construction of the polynomials in $\mathcal{R}[X]$ as lists otherwise follows the same guideline as in the C-CoRN library: *if a coefficient is missing then pick 0 instead*. For instance, the equivalence $[x_0; x_1] \sim [x'_0]$ holds for polynomial representations when $x_0 \sim x'_0$ and $x_1 \sim 0$ hold in $\mathcal{R}$. We will not detail here how we implemented the algebraic structure over $\mathcal{R}[X] := (\text{list}\mathcal{R}, \dots)$. With the right tools, we view it as an “easy” exercise, but see also the discussion in Section 7.

## 4.3 The Categorical Characterization

How do we know that our implementation via a setoid of
polynomial representations is really the intended polyno-
mial ring $\mathcal{R}[X]$, and not an arbitrary ring? This is where
category theory helps: below we show that polynomial re-
presentations, together with its ring structure, form an initial
object in the category of pointed extensions of the ring $\mathcal{R}$.

We describe the categorical characterization of the poly-
nomial ring $\mathcal{R}[X]$, and more generally of the multivariate
polynomial ring $\mathcal{R}[U]$ where $U$ is an arbitrary type of un-
knowns, not just a singleton $\{X\}$. It might be less well known
than the characterization of the direct product $\mathcal{R} \times \mathcal{T}$ that
we encountered in Section 3.1. The corresponding file in the
code is still category.v.

**Definition 4.1** (Multivariate polynomial ring $\mathcal{R}[U]$). Let $\mathcal{R}$ be a ring and $U$ be a type. A multivariate extension of $\mathcal{R}$ with unknowns in $U$ is a tuple $(\mathcal{E}, \varphi, e)$ where $\mathcal{E}$ is a ring, $\varphi: \mathcal{R} \to \mathcal{E}$ is a ring homomorphism, and $e: U \to \mathcal{E}$ is

<footnote n="14">¹⁴As reported by Felix Smith, his quote was: “Young man, in mathematics you don’t understand things. You just get used to them.”</footnote>

<footnote n="15">¹⁵Formally, the expression is just a list `[x₀; ... ; xₙ]` of coefficients.</footnote>

<footnote n="16">¹⁶later allowing us to confirm the generality of the HBT as claimed in [7].</footnote>
simply a map. A homomorphism of multivariate extensions $(\mathcal{E}, \varphi, e)$ and $(\mathcal{F}, \psi, f)$ is a ring homomorphism $\gamma : \mathcal{E} \to \mathcal{F}$ s.t. $\gamma \circ \varphi \equiv \psi$ and $\gamma \circ e \equiv f$. Multivariate extensions of $\mathcal{R}$ with unknowns in $U$ form a category of which initial objects are called multivariate polynomial rings over $\mathcal{R}$ with unknowns in $U$, and are denoted by $\mathcal{R}[U]$.

As initial objects in a category, all multivariate polynomial rings over $\mathcal{R}$ with unknowns in $U$ are isomorphic, which somehow justifies denoting them all with $\mathcal{R}[U]$. Any bijective correspondence between the types $U$ and $V$ gives rises to an isomorphism between the rings $\mathcal{R}[U]$ and $\mathcal{R}[V]$.

**Definition 4.2** (Univariate polynomial ring $\mathcal{R}[X]$). Given a name $X$ for the unknown, a univariate polynomial ring is a multivariate polynomial ring for $U := \{X\}$, a singleton type, and is denoted $\mathcal{R}[X]$. Hence, they are the initial objects of the category of univariate (or pointed) extensions of $\mathcal{R}$.

Because there is a bijection between the singleton $\{X\}$ and the singleton $\{Y\}$ (and in fact any other singleton), the polynomial rings $\mathcal{R}[X]$ and $\mathcal{R}[Y]$ are isomorphic as well.

**Theorem 4.3.** Given a ring $\mathcal{R}$, one can compute a ring denoted poly\_ring $\mathcal{R} := (\text{list}\mathcal{R}, \dots)$ based on the carrier type list $\mathcal{R}$. Moreover the pointed extension

$$(\text{poly\_ring} \mathcal{R}, \varphi, [0; 1]) \quad \text{where } \varphi := \lambda x, [x]$$

is a (univariate) polynomial ring over $\mathcal{R}$, i.e. $\mathcal{R}[X]$.

*Proof.* We build the ring poly\_ring $\mathcal{R}$: ring based on the polynomial representation as described in Section 4.2. Recall that the ring record type is based on setoids which allows for several representations of the same polynomial. The named unknown $X$ is associated to the list $[0; 1]$ representing the polynomial $0.X^0 + 1.X^1$. The map $\varphi$ associates any value $x : \mathcal{R}$ to the polynomial $x.X^0$ represented by the list $[x]$. $\square$

In the sequel, we may denote $\mathcal{R}[X]$ for the particular implementation poly\_ring $\mathcal{R}$ of a univariate polynomial ring, which is standard practice. However, the statements and proofs of upcoming Theorems 4.4 and 5.2, and of Lemma 5.5 actually work only with this implementation of $\mathcal{R}[X]$, and not at the more abstract level of Definition 4.2.

## 4.4 Critical Observation for the HBT

We describe the critical observation that serves in the base case of the short but (somewhat) sophisticated bar inductive proof of the HBT [7]. For a simpler formulation, we abusively write “polynomial” instead of “polynomial representation” in its informal statement below:

**Theorem 4.4.** Given a polynomial $p : \mathcal{R}[X]$ and a list $m : \text{list}\mathcal{R}[X]$ of shorter polynomials s.t. the head coefficient of $p$ is a linear combination of the head coefficients in $m$, there is a polynomial $q : \mathcal{R}[X]$, strictly shorter than $p$ and s.t. $p - q$ is a linear combination of $m$.

Before we state it formally, we need some tools, in particular the length and head coefficients. It is important to remark that these notions are attached to polynomial representations, not to polynomials.<fnref n="17" /> Recall that $|l| : \mathbb{N}$ is the length and it applies in particular to polynomial representations which are lists. We capture the head coefficient of a polynomial representation with the inductive predicate $\text{is\_last}\{A\} : A \to \text{list}A \to \mathbb{P}$ defined by the single rule:

$$\overline{\text{is\_last } a \ (l \equiv [a])}$$

As an added remark, these notions are simple to define for the representation of polynomials as ordered lists of monomials, and much less so with polynomials as algebraic expressions (see Section 4.1).

We recall the $\text{Forall}_1\{A\} (P : A \to \mathbb{P}) : \text{list}A \to \mathbb{P}$ and $\text{Forall}_2\{AB\} (R : A \to B \to \mathbb{P}) : \text{list}A \to \text{list}B \to \mathbb{P}$ predicates that characterize finite universal quantification over one or two lists, as defined inductively in the List module of the standard library, with two rules each:

$$\frac{\text{Forall}_1 P \quad [\quad \frac{Pa}{\text{Forall}_1 P} \quad \text{Forall}_1 P \quad l]}{\text{Forall}_2 R \quad [\quad \frac{Rab}{\text{Forall}_2 R} \quad l \quad m}]}$$

With those definitions, the statement of Theorem 4.4 can be formalized as: for any $p : \text{poly\_ring} \mathcal{R}$ and any $m : \text{list}(\text{poly\_ring} \mathcal{R})$, if the two following conditions hold:

1. $\text{Forall}_1 (\lambda q, |q| \le |p|) m$;

2. $\exists x h, \text{is\_last} x p \wedge \text{Forall}_2 \text{is\_last} h m \wedge \text{lc} h x$; then $\exists q : \text{poly\_ring} \mathcal{R}, |q| < |p| \wedge \text{lc} m (p - q)$.

*Proof of Theorem 4.4.* First multiply each polynomial in $m$ by some suitable $X^k$ so that all the lengths in $m$ match that of $p$. We get a new list $m'$ with the same head coefficients as $m$, and all the polynomials in $m'$ have length $|p|$.

We replay the linear combination of the head coefficients of $m/m'$ on the polynomials in $m'$ themselves and obtain a polynomial $p'$ which has the same length and same head as $p$, and is moreover a linear combination of $m'$, hence of $m$.

Then we define $q := p - p'$ while removing its 0 head coefficient to ensure $|q| < |p|$. Moreover $p - q \sim p'$ holds. The mechanized statement is named update\_lead\_coef and its proof can be reviewed in poly.v. $\square$

# 5 Hilbert's Basis Theorem

We now switch to Hilbert's basis theorem which we state as:

**Theorem 5.1.** Let $\mathcal{R}$ be a Noetherian ring and $X_1, \dots, X_n$ be $n : \mathbb{N}$ different unknowns. Then the ring $\mathcal{R}[X_1, \dots, X_n]$ of multivariate polynomials is Noetherian.

<footnote n="17">¹⁷Polynomials have equivalent representations with different lengths/heads. The “degree” of polynomials as used in [7] only exists for discrete rings.</footnote>
Notice that the original statement of Hilbert assumes that $\mathcal{R}$ is a field (which is thus automatically Noetherian), but of course with the classical understanding of Noetherian ring that is not suitable in constructive setting, see Section 2.2.

We state it for (bar) Noetherian rings instead and it becomes a direct consequence of the restricted statement:

**Theorem 5.2.** For any ring $\mathcal{R}$ the following entailment holds:

noetherian $\mathcal{R} \to$ noetherian (poly\_ring $\mathcal{R}$).

*Proof of Theorem 5.1.* The ring $\mathcal{R}[X_1][X_2]\dots[X_n]$ is a multivariate polynomial ring for $\mathcal{R}$ with unknowns $\{X_1, \dots, X_n\}$ because it satisfies the categorical characterization of Definition 4.1. Moreover $\mathcal{R}'[X_i]$ and poly\_ring $\mathcal{R}'$ are isomorphic for any $\mathcal{R}' := \mathcal{R}[X_1][X_2]\dots[X_{i-1}]$. Hence an induction on $n$ combined with Theorem 5.2 gives a direct proof. The reader can consult the file hbt.v for details.

□

Concerning the proof of Theorem 5.2, we follow the outline given in [7] while reformulating some arguments. In particular, we abstract the notion of update in a finitely generated ideal, and we replace “open induction” by a lexicographic induction principle, deviating a bit from the minimal bad sequences argument that open induction emulates.

## 5.1 Updating Finitely Generated Ideals

In ideal.v, we characterize the update operation on list of elements of a ring $\mathcal{R}$ as an inductive binary relation update :

$$ \text{list} \mathcal{R} \to \text{list} \mathcal{R} \to \mathbb{P} \text{ defined by two rules:} $$

$$ \frac{\text{lc } l (y - x)}{\text{update } (x :: l) (y :: l)} \qquad \frac{\text{update } l m}{\text{update } (x :: l) (x :: m)} $$

The update relation is symmetric and preserves the generated ideal, i.e. $\forall l m$, update $l m \to idl [l] = idl [m]$. As a consequence, updating also preserves pauses and bar PA; see noetherian.v for proofs.

**Proposition 5.3.** For any $l, m : \text{list} \mathcal{R}$, the two following entailments hold:

1. update $l m \to PAl \to PAm$;

2. update $l m \to bar PAl \to bar PAm$.

In Theorem 4.4, we find a polynomial $q$ s.t. $\text{lc } m (p - q)$ which entails that update $(q :: m) (p :: m)$ (first rule), and as a consequence bar PA $(q :: m) \to$ bar PA $(p :: m)$ holds as well. We will use this in the proof of the upcoming Lemma 5.5.

## 5.2 A Tailored Lexicographic Induction Principle

Let $A : \text{Type}$ and $T : A \to A \to \mathbb{P}$ be a binary relation. We form a binary relation $<_T : \text{list} A \to \text{list} A \to \mathbb{P}$ defined inductively with two rules, where we write $<_T$ infix:

$$ \frac{\text{Tab}}{a :: m <_T b :: m} \qquad \frac{l <_T m}{l <_T b :: m} $$

Using a repeated application of the second rule, we show:

$$ l <_T m \to l <_T k \equiv m \quad \text{for any } k, l, m : \text{list} A $$

The relation $<_T$ is a kind of lexicographic product and is thus well-founded as soon as $T$ is. The proof of well-foundedness would proceed by nested induction but here, we can alternatively remark that $<_T$ is included into the shortlex lexicographic relation,<fnref n="18" /> which is itself well-founded.

We do not actually need this level of generality, and instead implement a tailored induction principle:

**Theorem 5.4.** Assume $T$ is well-founded. Let $k : \text{list} A$ be a list and $P : \text{list} A \to \mathbb{P}$ by a property of lists. To show $\forall a, P (a :: k)$ it is sufficient to establish:

1. $\forall l, l <_T k \to Pl$;

2. $\forall a, (\forall l, l <_T a :: k \to Pl) \to P (a :: k)$.

*Proof.* We prove $P (a :: k)$ by well-founded induction on $a$ using $T$ for the well-founded relation, hence we assume

$$ IH : \forall b, T b a \to P (b :: k). $$

We apply item 2 and the goal becomes $\forall l, l <_T a :: k \to Pl$. Let us pick $l$ s.t. $l <_T a :: k$ and let us show that $Pl$ holds. Inverting $l <_T a :: k$, we distinguish two cases: either $l = b :: k$ with $T b a$ for some $b$ (left rule), thus $P (b :: k)$ holds by IH, and we get $Pl$ as required; or else $l <_T k$ holds (right rule) and we get $Pl$ using item 1.

□

According to that tailored induction principle, when the goal $P (a :: k)$ presents itself, we just need to check: in the base case that $Pl$ holds for any $l <_T k$, and in the recursive case, we can further assume that $Pl$ holds for any $l <_T a :: k$.

## 5.3 The Main Inductive Proof

Let $\mathcal{R}$ be a ring and let $\mathcal{R}[X] := \text{poly\_ring} \mathcal{R}$ be its ring of univariate polynomials, implemented using lists (see Theorem 4.3). We define the relation $T : \mathcal{R}[X] \to \mathcal{R}[X] \to \mathbb{P}$ by $T p q := |p| < |q|$, i.e. $p$ is strictly shorter than $q$. As the strict natural order on $\mathbb{N}$ is well-founded then so is $T$ and we use this instance for $<_T : \text{list} \mathcal{R}[X] \to \text{list} \mathcal{R}[X] \to \mathbb{P}$ and activate the tailored lexicographic principle of Theorem 5.4.

**Lemma 5.5 (HBT, recursive).** Let $h : \text{list} \mathcal{R}$ be a list (of head coefficients). The following statement holds:

$$ \begin{array}{l} \text{bar PAh} \to \forall k, \text{Forall}_2 \text{ is\_lasth k} \\ \qquad \to (\forall m, m <_T k \to \text{bar PAm}) \to \text{bar PAk}. \end{array} $$

*Proof.* Notice the implicit type $k : \text{list} (\text{poly\_ring} \mathcal{R})$ in the statement, so RocQ knows that the members of $k$ belong to a (polynomial) ring, and are more than lists of values in $\mathcal{R}$. We proceed by induction on bar PAh. In the base case we have $H_1 : PAh$. Let us pick $k$ s.t.

$$ H_2 : \text{Forall}_2 \text{ is\_lasth k} \quad H_3 : \forall m, m <_T k \to \text{bar PAm} $$

<footnote n="18">¹⁸$\mathcal{I}$ is shortlex smaller than $m$ if $|\mathcal{I}| < |m|$, or if $|\mathcal{I}| = |m|$ and $\mathcal{I}$ is R-lexicographically smaller than $m$.</footnote>
because the empty list [] contains no pause and `[]` ⊆ P always holds. Said otherwise, we have proved:<fnref n="20" />

$$ \begin{array}{rcl} \text{noetherian} & \mathcal{R} & \\ \rightarrow & \text{well\_founded} & (\lambda P Q, P \supsetneq_w Q \wedge \text{ideal} Q). \end{array} $$

It follows that $\supsetneq_w$ is well-founded on the ideals of $\mathcal{R}$: we simply transfer well-foundedness using a surjective morphism. The same tool works to derive items 1, 2 and 3. □

Using the above well-foundedness results, we study the links between (bar) Noetherian rings and alternate constructive characterizations, see noetherian\_alt.v. We write $\subset$ infix for strict inclusion, i.e. $P \subset Q := P \subset Q \wedge Q \not\subset P$ and $\supset$ for the converse relation $\subset^{-1}$. Notice that $\subset$ is constructively weaker than witnessed strict inclusion $\subset_w$, but they coincide on the finitely generated ideals of strongly discrete rings.

**Definition 6.2** (Noetherian, constructive variants). A ring is *RS-Noetherian* if any infinite increasing sequence of finitely generated ideals pauses. A ring is *ML-Noetherian* if the relation $\supset$ is well-founded on its finitely generated ideals.

Notice that the original definition of ML-Noetherian in [13, Def. 3.4] further assumes a coherent ring, with a “membership algorithm.” There are other terminologies for this concept like “has detachable ideals” [18, p. 514] or “strongly discrete” [24, Def. 5] (or [6, p. 278]), all of them giving a computational interpretation (informative in RocQ terminology) of our (non-informative) Definition 2.1 of strongly discrete rings. We do not need the assumptions of coherence and computability for the results below.

**Theorem 6.3.** Let $\mathcal{R}$ be a strongly discrete ring. Then $\mathcal{R}$ is (bar) Noetherian iff it is ML-Noetherian.

*Proof.* The only if part follows from Theorem 6.1 (item 1) since strict inclusion and witnessed strict inclusion are equivalent for the finitely generated ideals of a strongly discrete ring. For the if part, we show that the predicate PA is (logically) decidable on strongly discrete rings, hence bar PA is equivalent to an Acc(essibility) predicate and, we conclude with a relational morphism. □

**Theorem 6.4.** Any strongly discrete ML-Noetherian ring is RS-Noetherian.

*Proof.* Assume a strongly discrete ML-Noetherian ring $\mathcal{R}$, and a sequence $\rho: \mathbb{N} \rightarrow \mathcal{R} \rightarrow \mathbb{P}$ s.t. $\rho_n \subseteq \rho_{n+1}$ (increasing) and $\rho_n$ is a finitely generated ideal, for any $n: \mathbb{N}$. The binary relation $T: \mathbb{N} \rightarrow \mathbb{N} \rightarrow \mathbb{P}$ defined by $T nm := \rho_m \subsetneq_w \rho_n$ is well-founded because $\mathcal{R}$ is ML-Noetherian. We show

$$ \forall n \exists m, n \le m \wedge \rho_{m+1} \subseteq \rho_m $$

by well-founded induction on $n$ using $T$. We get the pause using the instance where $n := 0$. □

However, even in the strongly discrete case, the universal quantification over sequences used in the ascending chain condition for RS-Noetherian rings is weaker than the inductive predicates bar and Acc used in the definitions of bar and ML-Noetherian rings, hence getting the converse implication involves assuming extra axioms [16]. Possibly one could here adapt to constructive algebra the counter example given by Blass [2] for WQO theory (see also [3]).

# 7 Remarks about Mechanization Choices

Such a delay for a mechanization that turned out to be of quite reasonable code size might seem long, which pops up the obvious question: *why*? We reflect on this situation, largely focusing on the issue of the construction of uni- and multivariate polynomials over rings. Then we discuss the pertinence of recent alternate approaches to this construction in the context of the proof of the HBT discussed herein.

## 7.1 Why the Delay?

One may wonder why an implementation of such a landmark result as the constructive HBT had been pending this long, considering that the pen&paper outline [7] is 25 years old, and that this work already contained AGDA code for Dickson’s lemma to be used in the certification of Buchberger’s algorithm. Moreover, several other constructive proofs precede (and succeed) the one we put the focus on, albeit with other characterizations of Noetherian rings.

We try to answer that question based on guesses informed by our own experience. First of all, most pen&paper constructive accounts of the HBT are not as short and synthetic as that of [7]. We attribute this feature to the characterization of Noetherian rings using bar inductive predicates.

In some followup work in CoQ, Persson [21] mentions some difficulties with the bar predicate that he seemingly needs to convert into an Acc(essibility) predicate (a singleton with one constructor only) before he can implement the proof of the HBT, and which he leaves as an “open problem” in his conclusions. We did not encounter that difficulty. He also imported the implementation of polynomials in Théry’s work [27, 28] on Buchberger’s algorithm, where (multivariate) polynomials are ordered lists of monomials in $\mathcal{F}[X_1, \dots, X_n]$ that need to be normalized, hence assuming the ring $\mathcal{F}$ to be discrete field. This makes sense for Buchberger’s algorithm but basing on this view of polynomials, one cannot follow the outline of [7] because it really needs the construction of $\mathcal{R}[X]$ for a ring $\mathcal{R}$ (and not for a field), to be able to iterate Theorem 5.2.

But why did Persson (apparently) not try to implement abstract rings and polynomial rings by himself? Because as discussed in Section 4.2, we did not find it to be an overwhelming task. Notice the work on the C-CoRN library [17] came somewhat later so he could not have relied on it, but we did not have to either. B.t.w. the focus of C-CoRN are

<footnote n="20">²⁰RocQ’s StdLib defines `well_founded` ($T: A \rightarrow A \rightarrow P$) := $\forall a$, Acc T a.</footnote>
constructive real numbers in Coq and, even thought this library contains a significant algebraic hierarchy, that it does not deal with Noetherian algebra.

We speculate that the difficulty may have come from the lack of versatile instruments in proof assistants at the time. Indeed, the construction of the polynomial ring in `poly.v` weights around 500 loc but that code makes heavy use of both the ring tactic [11] and setoid rewriting [26]. Both sets of tools were absent for AGDA, and w.r.t. Coq, they were either lacking or too embryonic at the time, and started to mature only several years later.

These are however essential tools in our implementation, avoiding us to painfully solve ring equations by hand. Also notice that $R[X]$ forms a ring (as required by the ring tactic) only once the structure has been proved to satisfy the ring axioms. So there is a part of the code, in fact most of `poly.v`, which deals with polynomial representations not as elements of a ring, but exclusively as lists of coefficients. Setoid rewriting is key in this temporary situation.

## 7.2 Alternate Approaches to Polynomials over Rings

We compare our approach to recent mechanizations of the handling of uni- and multivariate polynomials over rings in constructive frameworks.

For instance, in [1] they build multivariate polynomials rings basing on the Mathematical Components library [10], with the goal of mechanizing the proof of transcendence of the Euler number $e$, and of $\pi$. There [1, Sect. 3.2.2], multivariate polynomials are viewed as the members of the free Abelian group with coefficient in $R: ringType$ and multivariate monomials (e.g. $XY^2$) as generators, using a quotient which in turn requires a `choiceType` structure to be provided, inherited by `ringType`. Moreover Mathematical Components was designed from the ground up on `eqType`, i.e. types equipped with a decidable equality (to allow for *reflection*), which `ringType` inherits as well. These implementation choices directly clash with our aim: to give to the HBT the most general statement possible, avoiding a discreteness assumption. Specifically, we need polynomials over rings that do not have a decidable equality. W.r.t. multivariate polynomials over finitely many variables, we manipulate those only at the very abstract level of category theory, e.g. proving that $R[X, Y]$ is isomorphic to $(R[X])[Y]$ (because they are both initial), and this turns out to work smoothly in the proof of Theorem 5.1.

Another recent approach is to use Higher Inductive Types (HIT) as in [14, Sect. 4.2] where there is a relevant discussion of the role played by decidable equality in the implementation of polynomial rings, also pointing out the requirement of discreteness in the Mathematical Components library. In [14], they instead use a HIT to identify polynomials modulo their trailing zeros. In a nutshell, a HIT is an inductive type where additional equality paths are declared simultaneously with the inductive constructors. And indeed, using HITs one can

build “real” quotients (as opposed to setoids), even for some non-decidable equivalence relations. That design choice is particularly elegant, although it does not allow to compute the degree or the head coefficient of polynomials, as pointed out by the authors of [14]. This is another reminder that these notions are only available for polynomial representations in the non-discrete case (see Section 4.4). But the proof of the HBT that we mechanize [7] is critically dependent on them: in fact, our choice to drop the discreteness assumption made us realize that this proof works on polynomial representations, not on polynomials. Hence, using a HIT for the quotient, though certainly possible, would probably be of no extra help here, compared to the setoid approach. In addition, unlike in CUBICAL AGDA [4], (axiom free) Rocq does not presently have the theoretical foundations required for HITs, although that might change in the future.

# 8 Conclusion and Perspectives

We emphasize bar inductive predicates as a constructive foundation for Noetherian rings worthy of renewed interest. Without any other assumption on rings like e.g. coherence or (strong) discreteness, we mechanize a pen&paper proof of Hilbert's basis theorem. Additionally we show that Noetherian rings are closed under direct products, with an implementation as well. We derive well-foundedness principles for bar Noetherian rings and compare with other constructive approaches like RS- and ML-Noetherianity. All the claimed results are sustained by an axiom free Rocq artifact.

There are many questions open for some follow up work. The strong similarity between the proofs of Ramsey's theorem, i.e. the closure of WQOs under direct products, and the closure of Noetherianity under direct products, make us wonder whether one result may be derived from the other? Or whether they both derive from a more abstract statement? In the same vein, one may wonder what could be the counterpart of the HBT in WQO theory (if any)? The bar inductive predicate proofs of Higman's lemma that we are aware of seem to differ largely from that of the HBT.

Since the results we implement work for non-discrete rings, what about constructive real numbers, the primary example of a non-discrete field: classically, the zero test function is not continuous. Can we find a field of constructive real numbers that would be Bezout? Bar Noetherian?

Finally, the termination of Buchberger's algorithm that computes Gröbner bases is usually grounded on Dickson's lemma [7, 21, 28]. Can we alternatively justify its termination using the HBT? There are other algorithms [20] for the same task. May be the HBT could be of some help there as well?

# Acknowledgments

We thank the anonymous CPP '26 reviewers for their detailed and helpful comments. This work was partially supported by the NARCO project ANR-21-CE48-0011.
References

[1] S. Bernard, Y. Bertot, L. Rideau, and P.-Y. Strub. 2016. Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric Polynomials. In *Conference on Certified Programs and Proofs (CPP 2016)*. Association for Computing Machinery, New York, NY, USA, 76–87. doi:10.1145/2854065.2854072

[2] A. Blass. 1986. Well-Ordering and Induction in Intuitionistic Logic and Topoi. In *Mathematical Logic and Theoretical Computer Science*. Taylor&Francis Group, Boca Raton, 29–48.

[3] G. Buriola, P. Schuster, and I. Blechschmidt. 2023. A Constructive Picture of Noetherian Conditions and Well Quasi-orders. In *Unity of Logic and Computation (CiE 2023)*. Springer, Cham, 50–62. doi:10.1007/978-3-031-36978-0_5

[4] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In *Types for Proofs and Programs (TYPES 2015) (LIPIcs, Vol. 69)*. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 5:1–5:34. doi:10.4230/LIPIcs.TYPES.2015.5

[5] T. Coquand. 2004. About Brouwer's Fan Theorem. *Revue internationale de philosophie* 58, 230 (4) (2004), 483–489. http://www.jstor.org/stable/23955601

[6] T. Coquand, A. Mörtberg, and V. Siles. 2012. Coherent and Strongly Discrete Rings in Type Theory. In *Certified Programs and Proofs (CPP 2012)*. Springer Berlin Heidelberg, 273–288. doi:10.1007/978-3-642-35308-6_21

[7] T. Coquand and H. Persson. 1999. Gröbner Bases in Type Theory. In *Types for Proofs and Programs (TYPES '98)*. Springer Berlin Heidelberg, 33–46. doi:10.1007/3-540-48167-2_3

[8] D. Fridlender. 1998. Higman's Lemma in Type Theory. In *Types for Proofs and Programs (TYPES '96)*. Springer Berlin Heidelberg, 112–133. doi:10.1007/BFb0097789

[9] D. Fridlender. 1999. An Interpretation of the Fan Theorem in Type Theory. In *Types for Proofs and Programs (TYPES '98)*. Springer Berlin Heidelberg, 93–105. doi:10.1007/3-540-48167-2_7

[10] G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. O. Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, and L. Théry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In *Interactive Theorem Proving (ITP 2013)*. Springer Berlin Heidelberg, 163–179. doi:10.1007/978-3-642-39634-2_14

[11] B. Grégoire and A. Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In *Theorem Proving in Higher Order Logics (TPHOLs 2005)*. Springer Berlin Heidelberg, 98–113. doi:10.1007/11541868_7

[12] D. Hilbert. 1890. Ueber die Theorie der algebraischen Formen. *Math. Ann.* 36 (1890), 473–534. doi:10.1007/BF01208503

[13] C. Jacobsson and C. Löfwall. 1991. Standard bases for general coefficient rings and a new constructive proof of Hilbert's basis theorem. *Journal of Symbolic Computation* 12, 3 (1991), 337–371. doi:10.1016/S0747-7171(08)80154-X

[14] T. Lamiaux, A. Ljungström, and A. Mörtberg. 2023. Computing Cohomology Rings in Cubical Agda. In *Certified Programs and Proofs (CPP 2023)*. Association for Computing Machinery, New York, NY, USA, 239–252. doi:10.1145/3573105.3575677

[15] D. Larchey-Wendling. 2024. The Coq-Kruskal project. https://github.com/DmxLarchey/Coq-Kruskal, Formal proof development.

[16] D. Larchey-Wendling. 2025. Constructive Substitutes for König's Lemma. In *Types for Proofs and Programs (TYPES 2024) (LIPIcs, Vol. 336)*. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2:1–2:23. doi:10.4230/LIPIcs.TYPES.2024.2

[17] E. Makarov et al. 2006. Constructive Coq Repository at Nijmegen. https://github.com/rocq-community/corn.

[18] H. Perdry. 2004. Strongly Noetherian rings and constructive ideal theory. *Journal of Symbolic Computation* 37, 4 (2004), 511–535. doi:10.1016/j.jsc.2003.02.001

[19] H. Perdry. 2008. Lazy bases: a minimalist constructive theory of Noetherian rings. *Mathematical Logic Quarterly* 54, 1 (2008), 70–82. doi:10.1002/malq.200710042

[20] H. Perdry and P. Schuster. 2014. Constructing Gröbner bases for Noetherian rings. *Mathematical Structures in Computer Science* 24, 2 (2014), e240206. doi:10.1017/S0960129513000509

[21] H. Persson. 2001. *An Integrated Development of Buchberger's Algorithm in Coq*. Technical Report RR-4271. INRIA. https://inria.hal.science/inria-00072316

[22] B. Puyobro, B. Ballenghien, and B. Wolff. 2025. A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series. *Archive of Formal Proofs* (2025). https://isa-afp.org/entries/Hilbert_Basis.html, Formal proof development.

[23] F. Richman. 1974. Constructive Aspects of Noetherian Rings. *Proc. Am. Math. Soc.* 44 (1974), 436–441. doi:10.2307/2040452

[24] P. Schuster and I. Yengui. 2025. An iterative constructive Hilbert basis theorem. *Journal of Algebra* 676 (2025), 56–68. doi:10.1016/j.jalgebra.2025.03.027

[25] A. Seidenberg. 1974. What is Noetherian? *Rend. Sem. Mat. Fis. Milano* 44 (1974), 55–61. doi:10.1007/BF02925651

[26] M. Sozeau. 2009. A New Look at Generalized Rewriting in Type Theory. *Journal of Formalized Reasoning* 2, 1 (2009), 41–62. doi:10.6092/issn.1972-5787/1574

[27] L. Théry. 1998. A Certified Version of Buchberger's Algorithm. In *Conference on Automated Deduction (CADE-15)*. Springer Berlin Heidelberg, 349–364. https://dl.acm.org/doi/10.5555/648234.753471

[28] L. Théry. 2001. A Machine-Checked Implementation of Buchberger's Algorithm. *Journal of Automated Reasoning* 26 (2001), 107–137. doi:10.1023/A:1026518331905

[29] W. Veldman. 2006. Brouwer's Real Thesis on Bars. *Philosophia Scientiæ* (2006), 21–42. doi:10.4000/philosophiascientiae.404

[30] D. Vytiniotis, T. Coquand, and D. Wahlstedt. 2012. Stop When You Are Almost-Full. In *Interactive Theorem Proving (ITP 2012)*. Springer Berlin Heidelberg, 250–265. doi:10.1007/978-3-642-32347-8_17

Received 2025-09-11; accepted 2025-11-13