Certified algorithms for numerical semigroups in Rocq
Massimo Bartoletti, Stefano Bonzio, Marco Ferrara
TL;DR
This work addresses the verification gap in numerical semigroup computations by providing a Rocq formalization that represents a semigroup via its gaps and implements certified algorithms for key invariants, including the multiplicity, Apéry set, and a generator-to-semigroup construction. It develops a pipeline from generators to the small elements and gaps, supported by formal proofs of correctness within Rocq and informal proof sketches, and introduces two Apéry-set algorithms with proofs of equivalence. The contribution is the first formalization of numerical semigroups in a proof assistant and a substantial set of verified procedures (approximately 3000 lines of Rocq code) that lay groundwork for future certified algorithms in this domain. The work has potential practical impact by enabling reliable, machine-checked computations and counterexample generation in algebraic contexts that rely on numerical semigroups.
Abstract
A numerical semigroup is a co-finite submonoid of the monoid of non-negative integers under addition. Many properties of numerical semigroups rely on some fundamental invariants, such as, among others, the set of gaps (and its cardinality), the Apéry set or the Frobenius number. Algorithms for calculating invariants are currently based on computational tools, such as GAP, which lack proofs (either formal or informal) of their correctness. In this paper we introduce a Rocq formalization of numerical semigroups. Given the semigroup generators, we provide certified algorithms for computing some of the fundamental invariants: the set of gaps, of small elements, the Apéry set, the multiplicity, the conductor and the Frobenius number. To the best of our knowledge this is the first formalization of numerical semigroups in any proof assistant.