# A Rocq Formalization of Monomial and Graded Orders

Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero

► To cite this version:

Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. A Rocq Formalization of Monomial and Graded Orders. 2025. hal-05396788

HAL Id: hal-05396788

https://inria.hal.science/hal-05396788v1

Preprint submitted on 3 Dec 2025

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 Attribution 4.0 International License
# A Rocq Formalization of Monomial and Graded Orders

Sylvie Boldo

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

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

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

Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France.

François Clément

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

a. Centre Inria de Paris, 48 rue Barrault, CS 61534, 75647 Paris Cedex, France.

b. CERMICS, École des Ponts, 77455 Marne-la-Vallée, France.

Vincent Martin

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

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

Université de technologie de Compiègne, LMAC, 60203 Compiègne, France.

Micaela Mayero

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

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

LIPN, Université Paris 13 - USPN, CNRS UMR 7030, 93430 Villetaneuse, France.

## Abstract

Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article is therefore definitions, operators, and proofs of properties about relations and orders, thus providing a comprehensive Rocq library. We especially focus on monomial orders, that are total orders compatible with the monoid operation. More than its definition and proved properties, we define several of them, among them the lexicographic and grevlex orders. For the sake of genericity, we formalize the grading of an order, a high-level operator that transforms a binary relation into another one, and we prove that grading an order preserves many of its properties, such as the monomial order property. This leads us to the definition and properties of four different graded orders, with very factorized proofs. We therefore provide a comprehensive and user-friendly library in Rocq about orders, including monomial and graded orders, that contains more than 700 lemmas.

**2012 ACM Subject Classification** Theory of computation → Logic and verification; Mathematics of computing; Software and its engineering → Formal software verification

**Keywords and phrases** Rocq proof assistant, formalization of mathematics, formal library, orders.

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.2016.23

## Supplementary Material

Git repository: https://lipn.univ-paris13.fr/rocq-num-analysis/-/tree/2.1/

Documentation: https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.1/

Opam packages: https://rocq-prover.org/p/rocq-num-analysis/2.1.0

# 1 Introduction

Orders are underlying fundamental objects in both mathematics and computer science. Moreover, they are a common formalization topic, due to their inherent generality and usefulness. Monomial orders are useful for tackling multivariate polynomials. The most common applications are in commutative algebra and algorithmic algebraic geometry. For example, they are central to the calculation of Gröbner bases, where they are used to define the dominant term of a polynomial, thereby facilitating the application of Buchberger's algorithm [9, 5, 12] or Faugère (F4 and F5) algorithms, e.g. see [7]. Division algorithms in multivariate polynomial rings also exploit these orders to efficiently reduce polynomials to a simplified form [6].

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

<figure><img src="image_11.png" /></figure>
23:2 A Rocq Formalization of Monomial and Graded Orders

Some orders, such as the lexicographic order, are used for the elimination of variables in the resolution of systems of polynomial equations or for the projection of algebraic varieties [7]. Other applications include triangulation or ideal decomposition, in connection with combinatorial geometry and the properties of polytopes [15]. The choice of an order also influences the performance of symbolic computation software such as Macaulay2,<fnref n="1" /> Singular<fnref n="2" /> or SageMath,<fnref n="3" /> directly affecting the complexity of calculations and the structure of objects [10].

Monomial orders are also underlying in the field of numerical analysis for polynomial approximations, even if it is not explicitly stated. Our motivation is the formalization in Rocq of (parts of) the Finite Element Method, see [1, 2, 3], that is popular to solve partial differential equations. In the process, it is needed to represent *d*-multivariate polynomials of bounded total degree *k*, often called $\mathbb{P}_k^d$, see for instance [3]. Indeed, in the Finite Element Method, it is very common to search the approximation to an unknown function by continuous and piecewise $\mathbb{P}_k^d$ functions. It is thus necessary to deal with multi-indices whose sum is at most *k*. The following mathematical definition offers numerous possibilities for formalization:

**Definition.** Let $d \ge 1$. Let $k \in \mathbb{N}$. The set of multi-indices of sum at most $k$ is denoted $\mathcal{A}_k^d$, and is defined by

$$ \mathcal{A}_k^d \stackrel{\text{def.}}{=} \{\alpha \in \mathbb{N}^d \mid |\alpha| \le k\}, \quad \text{where } \forall \alpha \in \mathbb{N}^d, \mid\alpha\mid \stackrel{\text{def.}}{=} \sum_{i=0}^{d-1} \alpha_i. $$

When implementing in a program or when formalizing in Rocq,<fnref n="4" /> one needs to order these multi-indices, as they are lists/vectors of lists/vectors. For more on the chosen ordering and Rocq implementation of $\mathcal{A}_k^d$, see Section 6.1.

In order to illustrate an order on $\mathbb{N}^d$, we use the representation of the multi-indices on the frame $(O, x_0, \dots, x_{d-1})$ of $\mathbb{R}^d$ ($d = 2$ or 3), see Figure 1. Note that the vector variables are noted with bold letters (such as $\boldsymbol{\alpha}$). The zero vector is denoted by $\mathbf{0}$.

One of the objectives of this article is to provide a comprehensive and user-friendly library that formalizes in Rocq various orders on $\mathbb{N}^d$ to order the multi-index set $\mathcal{A}_k^d$ (or more generally on $\mathbb{M}^d$, for any ordered commutative monoid $\mathbb{M}$). Such a multi-index can be used for instance as the multi-exponent of the $d$-multivariate monomial $\mathbf{X}^{\boldsymbol{\alpha}} \stackrel{\text{def.}}{=} \prod_{i=0}^{d-1} X_i^{\alpha_i}$ (whose total degree is $|\boldsymbol{\alpha}|$). Any polynomial in $\mathbb{P}_k^d$ of total degree at most $k$ is a linear combination of these monomials. Then, for instance to define a leading term, it is interesting to use an order on monomials that is compatible with the multiplicative monoid structure of monomials, or equivalently to use an order on multi-indices that is compatible with the additive monoid structure of multi-indices. Such total orders are said *monomial*, and the mapping $(\boldsymbol{\alpha} \mapsto \mathbf{X}^{\boldsymbol{\alpha}})$ becomes a monotonic ordered monoid morphism. Namely, we consider a total order “<” on multi-indices that satisfies: for all $\boldsymbol{\alpha}, \boldsymbol{\beta}, \gamma \in \mathbb{N}^d$, $\boldsymbol{\alpha} < \boldsymbol{\beta}$ implies $\boldsymbol{\alpha} + \gamma < \boldsymbol{\beta} + \gamma$. Or equivalently, we consider a total order “<” on monomials that satisfies $\mathbf{X}^{\boldsymbol{\alpha}} < \mathbf{X}^{\boldsymbol{\beta}}$ implies $\mathbf{X}^{\boldsymbol{\alpha}}\mathbf{X}^{\boldsymbol{\gamma}} < \mathbf{X}^{\boldsymbol{\beta}}\mathbf{X}^{\boldsymbol{\gamma}}$. It is also generally required that for all nonzero $\boldsymbol{\alpha}, 1 = \mathbf{X}^0 < \mathbf{X}^{\boldsymbol{\alpha}}$, or equivalently $\mathbf{0} < \boldsymbol{\alpha}$. Moreover, it can be of interest to have a *graded* monomial order, i.e. that respects $|\boldsymbol{\alpha}| < |\boldsymbol{\beta}|$ (in $\mathbb{N}$) implies $\boldsymbol{\alpha} < \boldsymbol{\beta}$ (in $\mathbb{N}^d$). Note also that monomial orders are usually defined as strict orders, but our formalization is more generic, as it encompasses strict and nonstrict orders, with adequate definitions.

<footnote n="1">¹ https://macaulay2.com/</footnote>

<footnote n="2">² https://www.singular.uni-kl.de/</footnote>

<footnote n="3">³ https://www.sagemath.org/</footnote>

<footnote n="4">⁴ https://rocq-prover.org</footnote>
This development is freely available as part of Opam<fnref n="5" /> packages, the Git repository is at
https://lipn.univ-paris13.fr/rocq-num-analysis/-/tree/2.1/
and the Rocq code and the documentation are also browsable at
https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.1/

In the following, ⌜ after a definition, a lemma or a file name is the corresponding hyperlink to the documentation.

Section 2 is devoted to some state of the art about binary relations, and lexicographic, monomial and graded orders. In Section 3, we briefly recall and formalize the necessary properties on binary relations. The Section 4 is dedicated to lexicographic orders, while Section 5 deals with the formalization in Rocq of graded and monomial orders. In Section 6, we detail the ordering of $A_k^d$ and give some conclusive remarks and perspectives.

<figure><img src="image_12.png" /><figcaption>Figure 1 Multi-indices $A_k^d$ for $d \in \{2, 3\}$ and $k = 3$. Each multi-index is depicted as a colored ball. The colors correspond to constant sums of multi-indices. For instance, in blue, we depict multi-indices whose sum is 3.</figcaption></figure>

## 2 State of the Art

Homogeneous binary relations such as order relations are fundamental objects in mathematics, just as functions, and are closely related to naive set theory. Moreover, the lexicographic order, or dictionary order, is a popular way to extend an order on items to an order on vectors (or homogeneous tuples). Therefore, they are formalized in most proof systems. Note that several concepts can be found under different names in the literature, and therefore also in formalizations. For example, preorder and quasi-order are usually synonymous, as well as total order and linear order on the one hand, and converse, dual, transpose, flip and inverse relation on the other hand. We first describe, ordered by proof assistant, some formalizations on the order properties, before going into the vector orders, including the lexicographic and monomial ones.

In Isabelle/HOL,<fnref n="6" /> there is support for abstract binary relations (HOL/Relation) and orders (HOL/Order_Relation). Relations are represented either as sets of pairs, or as binary predicates. Most elementary properties are defined: (ir)reflexivity, (a,anti)symmetry, transitivity, and totality. Orders are defined as conjunctions of elementary properties: preorder, partial order,

<footnote n="5">⁵ https://rocq-prover.org/p/rocq-num-analysis/2.1.0</footnote>

<footnote n="6">⁶ https://isabelle.in.tum.de/library/HOL/</footnote>
23:4 A Rocq Formalization of Monomial and Graded Orders

and (strict) linear order. Moreover, two implementations provide support for ordered struc-
tures as type classes, either embedding both strict and nonstrict versions (HOL/Orderings),
or not (HOL-Lattice/Orders, where lattices are also obviously covered). Many results are pro-
vided about the converse/dual operator (see Section 3). In addition, the lexicographic order
is defined on pairs as an operator on relations on both item (HOL-Library/Product.Lexorder),
with a specific definition for the strict version and for the nonstrict version. This operator is
shown to transport preorders, partial and linear orders.
111
112
113
114
115
116
117

In Lean, the mathlib library has a strong corpus on order theory, including lattices.<fnref n="7" /> Relations are represented as binary predicates, and elementary properties, including trichotomous, as well as conjunctive properties, including strict weak order, are defined as type classes (Order/Defs/Unbundled). There is also specific support for ordered structures embedding both strict and nonstrict versions (Order/Defs/PartialOrder and Order/Defs/LinearOrder). The support for lexicographic order is rather versatile in Lean. For instance, it is provided for pairs (Data/Prod/Lex), for lists (Data/List/Lex), but also for finitely supported functions (Data/Finsupp/Lex). And there is also support for generic lexicographic orders on sigma-types (Sigma/Lex) and pi-types (Order/PiLex), taking as arguments relations on the indices and on each summand/item.
118
119
120
121
122
123
124
125
126
127

In Rocq, at least three formalizations are present in the standard library.<fnref n="8" /> (i) The Sets standard library provides basic support for some of the usual definitions; it is quite old-fashioned. (ii) The Relations standard library also provides some support for elementary properties such as reflexivity, (anti)symmetry, and transitivity. Then, (pre)order is defined as a record collecting the appropriate elementary properties. An inductive definition provides the lexicographic order on pairs. This formalization is used in several parts of the standard library such as Sorting, Wellfounded and micromega (for Lra). (iii) The Classes standard library uses the type relation from Relations, then redefines elementary and conjunctive properties as type classes, including irreflexivity and asymmetry, strict and partial orders. There are lemmas for interactions of the flip operator with all elementary and conjunctive properties. This formalization is used to implement the generalized rewrite tactic for setoids. It is also used in several parts of the standard library such as Logic, MSets, NArith, PArith and Reals.
128
129
130
131
132
133
134
135
136
137
138
139
140

The main definitions are also provided in the SSReflect part of the standard library. This
is extended in the MathComp library [11],<fnref n="9" /> which provides the usual aspects of order theory
with full support for types equipped with partial or total orders, and lattices. Each algebraic
structure is equipped with both the nonstrict and strict variants of the order.
141
142
143
144

Monomial orders (also called admissible orders or term orders) and graded orders (also called degree orders) can be found as a part of formal developments about the computation of Gröbner bases in polynomial rings. Note that the well-order property can be included in the definition of monomial order, in particular when the termination of multivariate polynomial division algorithms is at stake.
145
146
147
148
149

In the isabelle Archive of Formal Proofs,<fnref n="10" /> lexicographic orders are defined from any
well-founded order and degree orders are defined from any scalar linear order and any relation
on vectors. Then, degree-lexicographic orders and degree-reverse-lexicographic orders are
defined.
150
151
152
153

<footnote n="7">⁷ https://github.com/leanprover-community/mathlib4/tree/3c3f56a/Mathlib/</footnote>

<footnote n="8">⁸ https://rocq-prover.org/doc/V8.20.0/stdlib/</footnote>

<footnote n="9">⁹ https://math-comp.github.io/htmldoc_2.4.0/mathcomp.ssreflect.order.html</footnote>

<footnote n="10">¹⁰ https://www.isa-afp.org/sessions/polynomials/#Power Products.html</footnote>
In Lean, the mathlib library provides support for monomial orders that embed the well-founded property (Data/Finsupp/MonomialOrder). Then, the degree lexicographic order is defined as the lexicographic order applied to pairs formed by the sum of the vector and the vector itself (Data/Finsupp/MonomialOrder/DegLex).

In Mizar, Schwarzweller [14] uses an abstract term order for the reduction of polynomials and the building of Gröbner bases.

In Rocq, we can cite the work by Perez [13] in which Gröbner bases needed some developments on polynomial rings using a generic order relation. We can also cite the works by Théry [16] and grobner.<fnref n="11" /> The former is based on the Relations standard library. The main order definition combines a well-founded preorder with compatibility with some monoid law; it is instantiated with the multiplication of monomials. A lexicographic order is defined for monomials only (or equivalently on tuples of natural numbers). The latter is based on the MathComp library.

For comparison, we do not cover lattices, or well-founded orders, but we provide many definitions including uncommon ones such as the union and intersection operators for binary relations, the connected, trichotomous and negatively transitive elementary properties, strict total order and strict weak order. We also provide many equivalent definitions, and a fairly comprehensive exploration of interactions between operators, elementary properties and conjunctive properties, resulting in about 300 lemmas (see Section 3). We place particular emphasis on providing definitions and properties that are close to standard mathematics. Furthermore, as this work is part of our rocq-num-analysis library, we cannot, for example, use MathComp canonical structures that are not compatible with those of Coquelicot and our library.

An original feature is our definition for the lexicographic order that unifies the strict and nonstrict cases, while taking care of the empty tuple. And the definition for graded orders is not restricted to the sole graded lexicographic order, graded is a generic operator that takes any scalar relation to compare sums, and any vector relation to then compare vectors. Again, we provide a fairly comprehensive corpus of lemmas about the various flavors of lexicographic orders, graded orders, monomial orders, and their interactions with basic operators and properties. This results in nearly 400 additional lemmas (see Sections 4 and 5).

# 3 Basic Operators and Properties of Binary Relations

Before dealing with monomial and graded orders, we first need to define the basics of order theory with some operators and properties about binary relations. The simplest example that comes to mind is the usual order on natural numbers, but this can be source of misleading intuition since that order actually possess many more properties than a mere (partial) order. For instance, it is a total order, and such that its complementary is also a total order. Instead, it can be preferable to take the inclusion in the power set of some set as mental image. It is not total, and its complementary is not an order since it is not transitive. We used [8] as reference, but we also took some inspiration from the related Wikipedia pages.¹²

In the file Binary_relation, given any type T and a relation R: T → T → Prop, we first define operators taking R and outputting a relation such as

<footnote n="11">¹¹https://github.com/thery/grobner/
¹²https://en.wikipedia.org/w/index.php?title=Binary_relation&oldid=1299977865
https://en.wikipedia.org/w/index.php?title=Homogeneous_relation&oldid=1289819519</footnote>
23:6 A Rocq Formalization of Monomial and Graded Orders

196
197
198
199

**Definition converse** $\checkmark$: $T \to T \to \text{Prop} := \lambda x y \Rightarrow R y x$.

**Definition complementary** $\checkmark$: $T \to T \to \text{Prop} := \lambda x y \Rightarrow \neg R x y$.

**Definition br_or_eq** $\checkmark$: $T \to T \to \text{Prop} := \lambda x y \Rightarrow x = y \lor R x y$.

200
201

Then, we define the following elementary properties that are used for the various flavors of orders

202
203
204
205
206
207
208
209
210
211
212
213

**Definition transitive** $\checkmark$: $\text{Prop} := \forall x y z, R x y \to R y z \to R x z$.

**Definition negatively_transitive** $\checkmark$: $\text{Prop} := \forall x y z, \neg R x y \to \neg R y z \to \neg R x z$.

**Definition reflexive** $\checkmark$: $\text{Prop} := \forall x, R x x$.

**Definition irreflexive** $\checkmark$: $\text{Prop} := \forall x, \neg R x x$.

**Definition antisymmetric** $\checkmark$: $\text{Prop} := \forall x y, R x y \to R y x \to x = y$.

**Definition asymmetric** $\checkmark$: $\text{Prop} := \forall x y, R x y \to \neg R y x$.

**Definition connected** $\checkmark$: $\text{Prop} := \forall x y, x \neq y \to R x y \lor R y x$.

**Definition strongly_connected** $\checkmark$: $\text{Prop} := \forall x y, R x y \lor R y x$.

**Definition trichotomous** $\checkmark$: $\text{Prop} :=$
$\forall x y, (x = y \land \neg R x y \land \neg R y x) \lor (x \neq y \land R x y \land \neg R y x) \lor (x \neq y \land R y x \land \neg R x y)$.

214
215

Note that connected and strongly connected respectively mean that the complementary is antisymmetric and asymmetric. Finally, we define conjunctive properties such as

216
217
218
219
220
221
222
223
224
225
226

**Definition total_order** $\checkmark$: $\text{Prop} :=$
transitive $R \land$ reflexive $R \land$ antisymmetric $R \land$ strongly_connected $R \land$
negatively_transitive $R \land$ connected $R$.

**Definition strict_total_order** $\checkmark$: $\text{Prop} :=$
transitive $R \land$ irreflexive $R \land$ asymmetric $R \land$ connected $R \land$
negatively_transitive $R \land$ antisymmetric $R \land$ trichotomous $R$.

**Definition strict_weak_order** $\checkmark$: $\text{Prop} :=$
negatively_transitive $R \land$ irreflexive $R \land$ asymmetric $R \land$
transitive $R \land$ antisymmetric $R$.

227
228
229
230

The latter actually means that the complementary is a total preorder (i.e. lacking the antisymmetry property). Note that these definitions are stated for usability in the form of conjunctions of relevant elementary properties. Then, equivalences with less hypotheses are provided as lemmas for shorter proofs, such as

231
232
233
234
235
236
237
238

**Lemma sto correct** $\checkmark$:
strict_total_order R $\leftrightarrow$ transitive R $\land$ irreflexive R $\land$ asymmetric R $\land$ connected R.

**Lemma sto equiv no asym** $\checkmark$:
strict_total_order R $\leftrightarrow$ transitive R $\land$ irreflexive R $\land$ connected R.

**Lemma sto equiv no irrefl** $\checkmark$:
strict_total_order R $\leftrightarrow$ transitive R $\land$ asymmetric R $\land$ connected R.

239
240
241

Besides equivalent definitions, we also provide a fairly comprehensive corpus of lemmas on interactions between operators, elementary properties, and conjunctive properties. For instance, the converse operator is compatible with all properties, such as

242
243
244
245

**Lemma conv_asym** $\checkmark$: asymmetric $R \to$ asymmetric (converse $R$).

**Lemma conv_to** $\checkmark$: total_order $R \to$ total_order (converse $R$).

246
247
248

And since converse is involutive, equivalences also hold. We also strived to provide the minimal hypotheses to obtain some specific property from another, or some equivalence. For instance, we have

249
250
251

**Lemma asym-equiv_irrefl_antisym** $\checkmark$: asymmetric $R \leftrightarrow$ irreflexive $R \land$ antisymmetric $R$.

**Lemma irrefl_asym Equiv** $\checkmark$: transitive $R \to$ irreflexive $R \leftrightarrow$ asymmetric $R$.
Lemma tricho Equiv_asym_conn: trichotomous R $\leftrightarrow$ asymmetric R $\wedge$ connected R.

252

Lemma conn_str_conn: reflexive R $\rightarrow$ connected R $\rightarrow$ strongly_connected R.

253

Lemma trans_neg_trans: connected R $\rightarrow$ transitive R $\rightarrow$ negatively_transitive R.

254

Lemma sto Equiv_swo: strict_total_order R $\leftrightarrow$ strict_weak_order R $\wedge$ connected R.

255

# 4 Lexicographic Orders

257

From a scalar order on a set $T$, we want to build a vector order on $T^d$, while retaining the properties of the initial scalar order. The notation $T^d$ refers to homogeneous tuples of size $d$, formalized as finite families (see below). When $T$ has enough properties or by abuse, elements of $T^d$ are also called vectors.

258

259

260

261

We first recall the well-known lexicographic order on $T^d$, and some others that can be derived easily. These are proved to be monomial orders under conditions in Section 5.

262

263

In the sequel, $\alpha$ and $\beta$ denote any finite families in $T^d$. We use the following notations when $d \ge 2$: the check notation $\check{\alpha} \in T^{d-1}$ denotes the last $d-1$ components of $\alpha$, and the tilde notation $\tilde{\alpha} \in T^{d-1}$ denotes the first ones. Thus, when $\alpha \stackrel{\text{def.}}{=} (\alpha_0, \dots, \alpha_{d-1})$, we have $\alpha = (\alpha_0, \tilde{\alpha}) = (\tilde{\alpha}, \alpha_{d-1})$. We also note $\bar{\alpha} \stackrel{\text{def.}}{=} (\alpha_{d-1}, \dots, \alpha_0)$. The Rocq development can be found in the file Lex.\#.

264

265

266

267

268

## 4.1 Lexicographic Order

269

In the case of a strict order, we have the following definition of the usual lexicographic order,

270

$$ \alpha <^{\text{lex}} \beta \stackrel{\text{def.}}{\iff} \left\{ \begin{array}{l} \alpha_0 < \beta_0, \text{ or} \\ \alpha_0 = \beta_0 \wedge d \ge 2 \wedge \check{\alpha} <^{\text{lex}} \beta. \end{array} \right. \qquad (1) $$

271

We have $\alpha <^{\text{lex}} \beta$ iff $\alpha_i < \beta_i$ for the first index $i$ for which $\alpha_i$ and $\beta_i$ differ. See a 2D example with multi-indices ($T = \mathbb{N}$) in Figure 2. And in the nonstrict case, a simple mathematical definition can be

272

273

274

$$ \alpha \le^{\text{lex}} \beta \stackrel{\text{def.}}{\iff} \alpha = \beta \lor \alpha <^{\text{lex}} \beta. \qquad (2) $$

275

Neither Equation (1) nor (2) is the chosen definition in Rocq as we have preferred to combine $<^{\text{lex}}$ and $\leq^{\text{lex}}$ into a single definition, and this is (3) we specify in Rocq. Given a scalar order $\prec$ on $T$, the lexicographic order, or simply “lex” order, noted $\prec^{\text{lex}}$, can be recursively defined by

276

277

278

279

$$ \alpha <^{\text{lex}} \beta \stackrel{\text{def.}}{\iff} \left\{ \begin{array}{l} \alpha_0 \neq \beta_0 \wedge \alpha_0 \prec \beta_0, \text{ or} \\ \alpha_0 = \beta_0 \wedge d \ge 2 \wedge \check{\alpha} <^{\text{lex}} \beta. \end{array} \right. \qquad (3) $$

280

In Rocq, following Section 3, we consider any type $T$ (defined as implicit Context in Rocq) and any binary relation $R: T \to T \to \text{Prop}$ (defined as Variable), which does not need to be an order. The type of $n$-families on $T$ is $[0..n) \to T$, denoted $T^n$ (see file Finite_family.\#), where $[0..n)$ denotes the finite type ordinal $n$ from MathComp [11]. Then, the application of the lex operator is of type $\text{lex } R: \forall n, T^n \to T^n \to \text{Prop}$. The recursive definition (provided in file Lex.\#) uses a Fixpoint. It is rather tedious, and instead, we present here the two specification lemmas that describe the base case and the recursive case and are more readable.

281

282

283

284

285

286

287

The base case, where $T^0$ is the unit type of empty families, is specified by

288

289

Lemma lexNil: $\forall (x y: T^0), \text{lex } x y \leftrightarrow \text{reflexive } R$

290
23:8 A Rocq Formalization of Monomial and Graded Orders

This means that for equal family arguments, the result of lex R x x depends on whether or not R is reflexive. With this generalization, we can deal with empty arguments, and with both strict and nonstrict orders for R, while keeping the same property for lex R.

The recursive case (for nonempty families) is specified by

Lemma lex_S[ ] : ∀ {n} {x y : 'T^n.+1}, lex x y ↔ (x ord0 ≠ y ord0 ∧ R (x ord0) (y ord0)) ∨ (x ord0 = y ord0 ∧ lex R (skipF0 x) (skipF0 y)).

Note that the type 'T^n.+1 (where the notation n.+1 stands for the successor of n) structurally grants that the family arguments are nonempty. There are two possibilities, exactly corresponding to (3):

either the first items $x_0$ and $y_0$ differ (in Rocq, $x \text{ord} 0$ and $y \text{ord} 0$), and then they must be related by R;

or the first items are equal, and then lex R is recursively called on the remaining of the families where the first item is skipped (in Rocq, using skipF0[]).

Then, for example, to use lex with the strict and nonstrict orders on natural numbers, we simply define the notations `lex_lt := (lex lt)` and `lex_le := (lex le)`. And, we prove the connection between (1) and (2) in this case,

Lemma lex_le_lt[ ] : ∀ {n}, @lex _ le n = br_or_eq (lex lt).

Then, three variants of this lex operator can be defined by either reverting the order of the items of the family arguments (colex order), or by swapping the arguments (symlex order), or both (revlex order). As mentioned in the introduction, the choice for a specific order depends on the goal pursued.

## 4.2 Colexicographic Order

The *colexicographic order*, or “*colex*” order, is defined by

$$ \alpha \prec_{\text{colex}} \beta \iff_{\text{def}} \bar{\alpha} \prec_{\text{lex}} \bar{\beta}. \qquad (4) $$

It is similar to the lex order, but starting from the right. For a strict order, we have $\alpha <_{\text{colex}} \beta$ iff $\alpha_i < \beta_i$ for the last index $i$ for which $\alpha_i$ and $\beta_i$ differ. This amounts to start from the left on $\bar{\alpha}$ and $\bar{\beta}$. It is also called *inverse lexicographic order*, or “*invlex*” order, e.g. see [7, p. 61].

In Rocq, we define the colex operator as

Definition colex[ ] {n} : 'T^n → 'T^n → Prop := reverse lex.

where, given any vector relation $Rn : 'T^n \to 'T^n \to Prop$,

Definition reverse[ ] (x y : 'T^n) : Prop := Rn (revF x) (revF y).

and `revF[ ] α := $\bar{\alpha}$`.

## 4.3 Symmetrical Lexicographic Order

We design the *symmetrical lexicographic order*, or simply “*symlex*” order, defined by

$$ \alpha \prec_{\text{symlex}} \beta \iff_{\text{def}} \beta \prec_{\text{lex}} \alpha. \qquad (5) $$

It is the symmetrical of the lex order. For a strict order, we have $\alpha <_{\text{symlex}} \beta$ iff $\beta_i < \alpha_i$ for the first index $i$ for which $\alpha_i$ and $\beta_i$ differ. We have found no mention of this variant in the literature.

In Rocq, we define the symlex operator as
**Definition symlex**$\check{\{n\}}$: $T^n \to T^n \to \text{Prop} := \text{converse lex.}$

where converse is the swapping of the arguments of binary relations (see Section 3).

## 4.4 Reverse Lexicographic Order

The reverse lexicographic order, or “revlex” order, is defined by

$$ \alpha \prec_{\text{revlex}} \beta \iff_{\text{def.}} \beta \prec_{\text{colex}} \alpha. \qquad (6) $$

It is the symmetrical of the colex order. For a strict order, we have $\alpha <_{\text{revlex}} \beta$ iff $\beta_i < \alpha_i$ for the last index $i$ for which $\alpha_i$ and $\beta_i$ differ. It is also called reverse inverse lexicographic order, or “rinvlex” order, e.g. see [7, p. 61].

In Rocq, we define the revlex operator as

**Definition revlex**$\check{\{n\}}$: $T^n \to T^n \to \text{Prop} := \text{converse colex.}$

In Section 5, the four lex-like operators are proved to transport the monomial order property of their scalar relation argument. Note also that lex and colex are obviously equivalent when $d = 1$ (and so are symlex and revlex).

Additionally, we also have $\bar{\alpha} \prec_{\text{symlex}} \bar{\beta} \iff \alpha \prec_{\text{revlex}} \beta$ and $\bar{\alpha} \prec_{\text{revlex}} \bar{\beta} \iff \alpha \prec_{\text{symlex}} \beta$. All these properties are proved in Rocq.

<figure><img src="image_13.png" /><figcaption>■ **Figure 2** Lex, colex, symlex, and revlex orderings (from left to right) of $A_k^d \subset \mathbb{N}^d$ when $d = 2$ and $k = 3$. The increase in the order is represented by dashed arrows. For $A_3^2$, we have</figcaption></figure>

lex (0, 0) < (0, 1) < (0, 2) < (0, 3) < (1, 0) < (1, 1) < (1, 2) < (2, 0) < (2, 1) < (3, 0)

colex (0, 0) < (1, 0) < (2, 0) < (3, 0) < (0, 1) < (1, 1) < (2, 1) < (0, 2) < (1, 2) < (0, 3)

The symlex order is the symmetrical of the lex order, and the revlex order is the symmetrical of the colex order. In view of graded orders, note that when the sum of multi-indices is 3 (hypotenuse of the triangles, blue nodes), we have $(0, 3) <_{\text{lex}} (1, 2) <_{\text{lex}} (2, 1) <_{\text{lex}} (3, 0)$, and also $(0, 3) <_{\text{revlex}} (1, 2) <_{\text{revlex}} (2, 1) <_{\text{revlex}} (3, 0)$.

The lex order and its variants are not very convenient in practice for multinomial ordering, as they do not sort the monomials according to their total degree. For instance, for $d = 2$, let $p \stackrel{\text{def.}}{=} X_0^0 X_1^8$ and $q \stackrel{\text{def.}}{=} X_0^1 X_0^2$. We have $p <_{\text{lex}} q$ (as $0 < 1$), but $\text{deg}(p) = 8 > 3 = \text{deg}(q)$. Thus, it can be useful to introduce *graded* monomial orders.

## 5 Monomial and Graded Orders

Now let us consider our basic type G to be an Abelian monoid, meaning we have an identity element denoted by 0 and an operator denoted by + that is both associative and commutative.

It corresponds to the AbelianMonoid canonical structure of Coquelicot [4]. On this type, we define what a monomial order is in Section 5.1, and define what a graded order is, and its properties, in Section 5.2. The Rocq development can be found in the file Monomial_order.
23:10 A Rocq Formalization of Monomial and Graded Orders

5.1 Monomial Order Definition

Given an Abelian monoid $G$, a relation $R$ is compatible with $+$ on the right when

Definition br_PLUS_COMPAT_r : Prop := ∀ x x1 x2, R x1 x2 → R (x1 + x) (x2 + x).

Then, a monomial order is both a strict total order and `br_PLUS_COMPAT_r`. We have a similar definition for nonstrict monomial orders. For instance, the standard strict and nonstrict orders on $\mathbb{N}$ are obviously monomial (see `Nat.add_{lt, le}_mono_r`), even if there is no total subtraction. As explained in Section 1, this compatibility property formalizes the expected assumptions on orders on monomials. Indeed, we expect that $X^\alpha < X^\beta$ implies $X^{\alpha+\gamma} = X^\alpha X^\gamma < X^\beta X^\gamma = X^{\beta+\gamma}$.

We then relate it to the previous definitions and operators. For instance, a monomial nonstrict order is antisymmetric (`mons_antisym`) and strongly connected (`mons_str_conn`). We also prove that `converse R` is a monomial order iff $R$ is one, and how it relates to the complementary. We also have definitions and lemmas on monomial orders where zero is comparable on the left to all nonzero elements (such as on $\mathbb{N}$).

We prove that the lexicographic orders defined in Section 4 (`lex`, `colex`, `symlex`, and `revlex`) are monomial orders, provided the initial scalar order is a monomial order and the addition is regular on the right (so that we may simplify).

Lemma `lex mo : plus is reg_r G` →
$\forall \{R: G \to G \to \text{Prop}\}, \text{monomial_order R} \to \forall (n: \text{nat}), \text{monomial_order (lex R)}.$

There is a simplification above for readability (as `lex R` cannot guess its $n$ implicit parameter).

5.2 Graded Orders

From the monomial orders (`lex`, `colex`, `symlex`, and `revlex`) based on the lexicographic order, see Section 4 and Figure 2, it is possible to generate graded monomial orders: `grlex`, `grcolex`, `grsymlex`, `grevlex`, see below. The principle is to compare first the sum of the families (that is to say the sum of the items of the vectors), with a given scalar relation on $G$, and then in case of equality use another given vector relation on $G^n$. These four orders are commonly defined recursively, after the consideration of the first index (`grlex` and `grsymlex`), or of the last index (`grcolex` and `grevlex`), and then, in the case of equality, the treatment of the rest of the family. Some of these orders are well-known (such as `grevlex` [7, p. 58]), other less common (`grsymlex` for instance).

These four orders are different when $d \ge 3$. Table 1 illustrates the differences between these four graded monomial orders on a few monomials of the same total degree.

<table><caption>Table 1 Ordering example on monomials with the strict order on $\mathbb{N}$ for the four graded orders presented here, with a constant total degree (=3). Increase from left to right.</caption><thead><tr><th>grlex &lt;</th><th>Z<sup>3</sup></th><th>Y<sup>3</sup></th><th>XYZ</th><th>XY<sup>2</sup></th><th>X<sup>3</sup></th></tr></thead><tbody><tr><th>grcolex &lt;</th><td>X<sup>3</sup></td><td>XY<sup>2</sup></td><td>Y<sup>3</sup></td><td>XYZ</td><td>Z<sup>3</sup></td></tr><tr><th>grsymlex &lt;</th><td>X<sup>3</sup></td><td>XY<sup>2</sup></td><td>XYZ</td><td>Y<sup>3</sup></td><td>Z<sup>3</sup></td></tr><tr><th>grevlex &lt;</th><td>Z<sup>3</sup></td><td>XYZ</td><td>Y<sup>3</sup></td><td>XY<sup>2</sup></td><td>X<sup>3</sup></td></tr></tbody></table>
Mathematical Definitions of Graded Orders

For the sake of readability, the mathematical definitions are given assuming the scalar order is strict.

The graded lexicographic order, or simply “grlex” order, is defined by

$$ \alpha <_{\text{grlex}} \beta \quad \overset{\text{def.}}{\iff} \quad \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha <_{\text{lex}} \beta. \end{cases} $$

This amounts to first compare the sum of families, and in case of equality, use the standard lex order (3). Thus, when $|\alpha| = |\beta|$, we have $\alpha <_{\text{grlex}} \beta$ iff $\alpha_i < \beta_i$ for the first index $i$ for which $\alpha_i$ and $\beta_i$ differ. See 2D and 3D examples in Figures 3 and 4. It is also called degree lexicographic order, or “deglex” order.

By inlining (1) (we are in the strict case), we actually obtain the following equivalence, which may be seen as an alternative recursive definition,

$$ \alpha <_{\text{grlex}} \beta \iff \left\{ \begin{array}{ll} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha_0 < \beta_0, \text{ or} \\ |\alpha| = |\beta|, & \alpha_0 = \beta_0 \quad \wedge \ d \ge 2 \quad \wedge \ \check{\alpha} <_{\text{grlex}} \check{\beta}. \end{array} \right. $$

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

<figure><img src="image_15.png" /><figcaption>■ Figure 3 Grlex, grcolex, grsymlex, and grevlex orderings of $\mathcal{A}_k^d$ when $d=2$ and $k=3$. The increase in the order is represented by dashed arrows. For $\mathcal{A}_3^2$, grlex and grevlex are equivalent, and so are grcolex and grsymlex. We have</figcaption></figure>

grlex/grevlex (0,0) < (0,1) < (1,0) < (0,2) < (1,1) < (2,0) < (0,3) < (1,2) < (2,1) < (3,0)

grcolex/grsymlex (0,0) < (1,0) < (0,1) < (2,0) < (1,1) < (0,2) < (3,0) < (2,1) < (1,2) < (0,3)

We design the graded colexicographic order, or simply “grcolex” order, defined by

$$ \alpha <_{\text{grcolex}} \beta \quad \overset{\text{def.}}{\iff} \quad \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha <_{\text{colex}} \beta. \end{cases} $$

This amounts to first compare the sum of families, and in case of equality, use the colex order (4). Thus, when $|\alpha| = |\beta|$, we have $\alpha <_{\text{grcolex}} \beta$ iff $\alpha_i < \beta_i$ for the last index $i$ where $\alpha_i$ and $\beta_i$ differ. As before, we have an alternative recursive definition. Compare on the same 2D and 3D examples the grcolex and grlex orders in Figure 3.

We also design the graded symmetric lexicographic order, or simply “grsymlex” order, defined by

$$ \alpha <_{\text{grsymlex}} \beta \quad \overset{\text{def.}}{\iff} \quad \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha <_{\text{symlex}} \beta. \end{cases} \qquad (7) $$
23:12 A Rocq Formalization of Monomial and Graded Orders

<figure><img src="image_16.png" /><figcaption>Figure 4 Grlex, grcolex, grsymlex, and grevlex orderings of $\mathcal{A}_k^d$ when $d = k = 3$. The increase in the order is represented by dashed arrows, only when the sum $l = 3$ (see Figure 1). The four orders are different. For the multi-indices of sum 3, we have</figcaption></figure>

<table><tr><td>grlex</td><td>(0, 0, 3) &lt; (0, 1, 2) &lt; (0, 2, 1) &lt; (0, 3, 0) &lt; (1, 0, 2) &lt; (1, 1, 1) &lt; (1, 2, 0) &lt; (2, 0, 1) &lt; (2, 1, 0) &lt; (3, 0, 0)</td></tr><tr><td>grcolex</td><td>(3, 0, 0) &lt; (2, 1, 0) &lt; (1, 2, 0) &lt; (0, 3, 0) &lt; (2, 0, 1) &lt; (1, 1, 1) &lt; (0, 2, 1) &lt; (1, 0, 2) &lt; (0, 1, 2) &lt; (0, 0, 3)</td></tr><tr><td>grsymlex</td><td>(3, 0, 0) &lt; (2, 1, 0) &lt; (2, 0, 1) &lt; (1, 2, 0) &lt; (1, 1, 1) &lt; (1, 0, 2) &lt; (0, 3, 0) &lt; (0, 2, 1) &lt; (0, 1, 2) &lt; (0, 0, 3)</td></tr><tr><td>grevlex</td><td>(0, 0, 3) &lt; (0, 1, 2) &lt; (1, 0, 2) &lt; (0, 2, 1) &lt; (1, 1, 1) &lt; (2, 0, 1) &lt; (0, 3, 0) &lt; (1, 2, 0) &lt; (2, 1, 0) &lt; (3, 0, 0)</td></tr></table>

The restriction of grsymlex to the last two components when the sum is 3, is exactly grsymlex for $d = 2$ (see Figure 3, right).

This amounts to first compare the sum of families, and in case of equality, use the symlex order (5). Thus, when $|\alpha| = |\beta|$, we have $\alpha <^{\text{grsymlex}} \beta$ iff $\beta_i < \alpha_i$ for the first index $i$ where $\alpha_i$ and $\beta_i$ differ.

We have an alternative recursive definition,

$$ \alpha <^{\text{grsymlex}} \beta \iff \left\{ \begin{array}{l} |\alpha| < |\beta|, \text{ or} \\ |\alpha| = |\beta| \quad \wedge \quad \beta_0 < \alpha_0, \text{ or} \\ |\alpha| = |\beta| \quad \wedge \quad \beta_0 = \alpha_0 \quad \wedge \quad d \ge 2 \quad \wedge \quad \check{\alpha} <^{\text{grsymlex}} \check{\beta}, \end{array} \right. \quad (8) $$

but it may be simplified,

$$ \alpha <^{\text{grsymlex}} \beta \iff \left\{ \begin{array}{l} |\alpha| < |\beta|, \text{ or} \\ |\alpha| = |\beta| \quad \wedge \quad d \ge 2 \quad \wedge \quad \check{\alpha} <^{\text{grsymlex}} \check{\beta}, \end{array} \right. \quad (9) $$

as when $|\alpha| = |\beta|$ and $\beta_0 < \alpha_0$, we have $d \ge 2$ and $|\check{\alpha}| < |\check{\beta}|$, i.e. $\check{\alpha} <^{\text{grsymlex}} \check{\beta}$. Note that this simplification is made possible by the symmetric aspect of symlex.
More precisely, grsymlex and grevlex (see below) have three equivalent definitions (by grading, recursive, and simplified recursive) while grlex and grcolex have only two: indeed, for instance for grlex, $|\alpha| = |\beta| \land \alpha_0 < \beta_0$ implies $|\tilde{\beta}| < |\tilde{\alpha}|$, i.e. $\tilde{\beta} <^{\text{grlex}} \tilde{\alpha}$, but not $\tilde{\alpha} <^{\text{grlex}} \tilde{\beta}$.

Note that the grcolex and grsymlex orders are identical when $d = 1$ or 2, but differ as soon as $d \ge 3$. Compare on the same 2D and 3D examples in Figure 3.

The graded reverse lexicographic order, or simply “grevlex” order, is defined by

$$ \alpha <^{\text{grevlex}} \beta \quad \overset{\text{def.}}{\iff} \quad \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha <^{\text{revlex}} \beta. \end{cases} $$

This amounts to first compare the sum of families, and in case of equality, use the revlex order (6). Thus, when $|\alpha| = |\beta|$, we have $\alpha <^{\text{grevlex}} \beta$ iff $\beta_i < \alpha_i$ for the last index $i$ where $\alpha_i$ and $\beta_i$ differ. It is also called degree reverse lexicographic order, or simply “degrevlex” order. As before, we have a simplified recursive definition,

$$ \alpha <^{\text{grevlex}} \beta \iff \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & d \ge 2 \land \tilde{\alpha} <^{\text{grevlex}} \tilde{\beta}, \end{cases} $$

as when $|\alpha| = |\beta|$ and $\beta_{d-1} < \alpha_{d-1}$ (with $d \ge 2$), we have $|\tilde{\alpha}| < |\tilde{\beta}|$, i.e. $\tilde{\alpha} <^{\text{grevlex}} \tilde{\beta}$.

Note that the grlex and grevlex orders are identical when $d = 1$ or 2, but differ as soon as $d \ge 3$. Compare on the same 2D and 3D examples in Figure 3.

Formal Definitions of Graded Orders

All these definitions share the same pattern. We have therefore formalized how to grade any binary relation. More precisely, given an Abelian monoid $G$, a scalar relation $R$ on $G$ and a vector relation $Rn$ on $G^n$, we define another vector relation on $G^{n+1}$,

**Definition graded** $\mathcal{G}$ (x y : $\mathcal{G}^n$) : $\text{Prop} := (\text{sum x} \neq \text{sum y} \land R(\text{sum x})(\text{sum y})) \lor (\text{sum x} = \text{sum y} \land Rn x y)$.

Note that, similarly to the lexicographical order definition of Section 4.1, this definition encompasses both strict and nonstrict cases for $R$.

The previous definitions are then straightforward,

**Definition grlex** $\mathcal{G}$ := graded $R$ ($\text{lex } R$).

**Definition grcolex** $\mathcal{G}$ := graded $R$ ($\text{colex } R$).

**Definition grsymlex** $\mathcal{G}$ := graded $R$ ($\text{symlex } R$).

**Definition grevlex** $\mathcal{G}$ := graded $R$ ($\text{revlex } R$).

We also provide all the various recursive definitions as equivalences, with some hypotheses on $G$ and $R$ when needed (such as `grsymlex_S` for (8) and `grsymlex_S.mo` for (9)).

More interesting, many properties hold about the graded operator, making a large factorization of proofs on all the wanted lemmas on the graded lexicographic orders. For instance, the reflexivity or irreflexivity of the relation graded $R$ $Rn$ is that of $Rn$ (e.g. see `graded_irrefl Equiv`), while the symmetry, antisymmetry and asymmetry needs the ones of both $R$ and $Rn$ (e.g. see `graded_asym`). A comprehensive study of the properties of Section 3 is formalized.

To get back to monomial orders, we prove that the graded of monomial orders is a monomial order,
23:14 A Rocq Formalization of Monomial and Graded Orders

**Lemma graded_mo**<sup>q</sup> : plus_is_reg_r G →
monomial_order R → monomial_order Rn → monomial_order (graded R Rn).

It is therefore straightforward to prove that grsymlex lt is a monomial order (grsymlex_lt_mo<sup>q</sup>).

An unexpected lemma is about the idempotence of the graded operator with respect to its scalar relation argument,

**Lemma graded_idem**<sup>q</sup> : ∀ {R1} R2 {n} {Rn : 'G^n → 'G^n → Prop},
graded R1 (graded R2 Rn) = graded R1 Rn.

When grading with respect to R2 (on G) and then R1 (on G too), it is equivalent to only grading with respect to R1. This may allow us to remove one graded out of two. For instance, when R1=R2, it means that graded R (grsymlex R) = grsymlex R. And for different orders on $\mathbb{N}$, we can prove for instance that graded gt (grcolex lt) = graded gt (colex lt).

# 6 Application, Conclusion & Perspectives

## 6.1 Application: Ordering of $\mathcal{A}_k^d$

As explained in Section 1, we are interested in defining and ordering $\mathcal{A}_k^d \stackrel{\text{def.}}{=} \{\alpha \in \mathbb{N}^d \mid |\alpha| \le k\}$, that corresponds to the exponents of $\mathbb{F}_k^d$, the $d$-multivariate polynomials of degree smaller or equal to $k$ (see file multi_index.q). As we want the corresponding family to be ordered by degree, we rely on a graded order and we construct $\mathcal{A}_k^d$ by slices of increasing degrees,

$$ \mathcal{A}_k^d = \bigsqcup_{l=0}^{k} C_l^d, \quad \text{with } C_l^d \stackrel{\text{def.}}{=} \{\alpha \in \mathbb{N}^d \mid |\alpha| = l\}. $$

Surprisingly, there are several ways to construct the slices of degree $l$, by induction on either the right or left and by the order of the sub-calls,

$$ C_l^d = \bigsqcup_{i=0}^{l} \{(i, \tilde{\beta}) \in \mathbb{N}^d \mid \tilde{\beta} \in C_{l-i}^{d-1}\} = \bigsqcup_{i=0}^{l} \{(\tilde{\beta}, i) \in \mathbb{N}^d \mid \tilde{\beta} \in C_{l-i}^{d-1}\}. $$

The first equality makes the family ordered by lex and the second one by colex, therefore making $\mathcal{A}_k^d$ ordered by grlex or grcolex.

In order to have monomials ordered by decreasing exponents on the successive variables $X_0, \dots, X_{d-1}$, we choose

$$ C_l^d = \bigsqcup_{i=0}^{l} \{(l - i, \tilde{\beta}) \in \mathbb{N}^d \mid \tilde{\beta} \in C_i^{d-1}\}, $$

which orders $C_l^d$ by symlex. And so we prove that $\mathcal{A}_k^d$ is ordered by (grsymlex lt).

## 6.2 Conclusion

We have presented a Rocq comprehensive formalization of many properties on orders, especially on monomial orders. The initial motivation was the ordering of multi-indices (on $\mathbb{N}^d$) for the formalization of multivariate polynomials, but we end with a comprehensive formalization of properties and lemmas about generic orders. Even if some part is really well-known (such as transitivity or irrelevance), we focus on proof engineering, we then bring up some subtleties about definitions, and we end up with a very usable and comprehensive library of
properties and how they are linked, that amounts to more than 50 definitions and nearly 700 lemmas. Moreover, the definition of graded orders as a high-level operator has led us to elegant and factorized proofs.

Thanks to our well-chosen definitions, there is no particularly difficult proof. Note also that it is not easy to have a reference of all these statements, especially as formal lemmas must encompass unintuitive cases, for instance nontotal orders or what happens on empty vectors. A difficulty is the handling in a single setting of both strict and nonstrict orders, especially in degenerate cases.

## 6.3 Weighted Orders

The main perspective of this work are the weighted orders [7]. We assume we have a ring $K$ (and not only a monoid as before) so that we have a dot product denoted by “.”. We also assume that the strict order $<_K$ is compatible not only with $+$, but with $\times \ell$ for positive $\ell \in K$. Then, there is a generalization of orders on $K^d$: a weighted order is characterized by an order $<_K$ on $K$ and a matrix $W$ of type $K^{d,m}$. Then if we denote the blocks of the matrix as $W = [w_0 | W_{1...m-1}]$, where $w_0 \in K^d$ and $W_{1...m-1}$ is in $K^{d,m-1}$,

$$ x <^W y \iff_{\text{def.}} \begin{cases} x \cdot w_0 <_K y \cdot w_0, \text{ or} \\ x \cdot w_0 = y \cdot w_0 \wedge x <^{W_{1...m-1}} y. \end{cases} \qquad (10) $$

This matrix vision encompasses all the defined orders (lex, grsymlex, and so on) and also provides generic lemmas. For instance for a square matrix on $\mathbb{R}$, the order is total if and only if the matrix is invertible. The graded operator corresponds to creating a block matrix with the first column filled with ones and the initial matrix.

The fact that the matrix may be rectangular adds to the generality of the definition, but also to the redundancy, as several matrices correspond to the same order. An interesting point is that we can relate some matrices to the alternative definitions: for instance, for grsymlex, three matrices correspond to (7), (8), and (9) (the first and last matrices being square).

More generally, for an order with a real invertible square matrix $W$, if we right-multiply $W$ by a square upper-triangular matrix with positive diagonal terms, then the corresponding order is the same. Thus, using a $QR$ decomposition of a matrix of an order $W (=QR)$, it is therefore possible to take $Q$ as a canonical form of the order.

Even if appealing, our formalization attempts have not been that successful. In particular, mathematics mostly consider square matrices for $W$, which is easier for invertibility, equivalence, and so on. But it makes it difficult to use the induction underlying (10). There is work left to precisely understand in which cases the matrix should be rectangle or square and have a usable formalization of weighted orders.

## References

1. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In *Proc. of the 6th ACM SIGPLAN Internat. Conf. on Certified Programs and Proofs (CPP 2017)*, pages 79–89, New York, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018625.

2. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. *J. Autom. Reason.*, 66(2):175–213, 2022. URL: https://doi.org/10.1007/s10817-021-09612-0.
23:16 A Rocq Formalization of Monomial and Graded Orders

556

3 Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Rocq formalization of simplicial Lagrange finite elements. Research Report RR-9590, Inria, 2025. URL: https://inria.hal.science/hal-05128905/.

557

558

559

4 Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. *Math. Comput. Sci.*, 9(1):41–62, 2015. URL: https://doi.org/10.1007/s11786-014-0181-1.

560

561

562

5 Bruno Buchberger and Franz Winkler, editors. *Gröbner Bases and Applications*. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9780511565847.

563

564

6 Arjeh M. Cohen, Hans Cuypers, and Hans Sterk, editors. *Some Tapas of Computer Algebra. Algorithms and Computation in Mathematics*. Springer, Berlin, Heidelberg, 1999. URL: https://doi.org/10.1007/978-3-662-03891-8.

565

566

567

7 David A. Cox, John Little, and Donal O'Shea. *Ideals, Varieties, and Algorithms*. Undergraduate Texts in Mathematics. Springer, Cham, 4th edition, 2015. URL: https://doi.org/10.1007/978-3-319-16721-3.

568

569

570

8 Matthias Ehrgott. *Multicriteria Optimization*. Springer, Berlin, Heidelberg, 2nd edition, 2005. URL: https://doi.org/10.1007/3-540-27659-9.

571

572

9 Ralf Fröberg. *An Introduction to Gröbner Bases*. John Wiley & Sons, 1997.

573

10 Jürgen Herzog, Takayuki Hibi, Freyja Hreinsdóttir, Thomas Kahle, and Johannes Rauh. Binomial edge ideals and conditional independence statements. *Adv Appl Math*, 45:317–333, 2010. URL: https://doi.org/10.1016/j.aam.2010.01.003.

574

575

576

11 Assia Mahboubi and Enrico Tassi. *Mathematical Components*. Zenodo, Genève, 2020. URL: https://doi.org/10.5281/zenodo.7118596.

577

578

12 Laurence Marcotte. Les bases de Groebner et les ordres monomiaux. Master's thesis, Université du Québec à Montréal, 2008. In French. URL: https://archipel.uqam.ca/1309/.

579

580

13 Gilberto Pérez Vega. *Bases de Gröbner: Desarrollo formal en Coq*. PhD thesis, Universidade da Coruña, 2004. In Spanish. URL: http://hdl.handle.net/2183/1148.

581

582

14 Christoph Schwarzweller. Gröbner bases — Theory refinement in the Mizar system. In M. Kohlhase, editor, *Proc. of the 4th Internat. Conf. on Mathematical Knowledge Management (MKM 2005)*, volume 3863 of LNCS, pages 299–314, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11618027_20.

583

584

585

586

15 Bernd Sturmfels. *Gröbner Bases and Convex Polytopes*. Number 8 in University Lecture Series. American Mathematical Society, 1996.

587

588

16 Laurent Théry. A machine-checked implementation of Buchberger's algorithm. *J. Autom. Reason*, 26:107–137, 2001. URL: https://doi.org/10.1023/A:1026518331905.

589