Bar Inductive Predicates for Constructive Algebra in Rocq

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.