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

HAL
open science

# 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. RR-9604, INRIA. 2025, pp.17. hal-05396759

HAL Id: hal-05396759

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

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Ínria

A Rocq Formalization of
Monomial and Graded
Orders

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

RESEARCH
REPORT

Nº 9604

December 2025

Project-Teams Toccata and
Serena
<figure><img src="image_3.png" /></figure>
<figure><img src="image_4.png" /></figure>

# A Rocq Formalization of Monomial and Graded Orders

Sylvie Boldo*, François Clément†, Vincent Martin‡, Micaela Mayero§

Project-Teams Toccata and Serena

Research Report n° 9604 — December 2025 — 17 pages

**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.

**Key-words:** Rocq proof assistant, formalization of mathematics, formal library, orders

This work was partly supported by the European Research Council (ERC) under the European Union's Horizon 2020 Research and Innovation Programme – Grant Agreement n°810367.

* Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France.sylvie.boldo@inria.fr

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

b. CERMICS, École des Ponts, 77455 Marne-la-Vallée, France.francois.clement@inria.fr

‡ Université de technologie de Compiègne, LMAC, 60203 Compiègne, France. vincent.martin@utc.fr

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

mayero@lipn.univ-paris13.fr

RESEARCH CENTRE
Centre Inria de Saclay

Bâtiment Alan Turing
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
91120 Palaiseau
Une formalisation en Rocq des ordres monomiaux et
gradués

**Résumé** : Même si les relations binaires et les ordres sont un sujet de formalisation courant, nous avons besoin de formaliser des ordres spécifiques (à savoir monomial et gradué) dans le processus de la formalisation en Rocq de la méthode des éléments finis. Cet article traite donc des définitions, des opérateurs et des preuves des propriétés des relations et des ordres, fournissant ainsi une bibliothèque Rocq complète. Nous nous concentrons tout particulièrement sur les ordres monomiaux, qui sont des ordres totaux compatibles avec l'opération de monoïde. Au-delà de la définition et des propriétés prouvées, nous en définissons plusieurs, dont les ordres lexicographique et grevlex. Par souci de généricité, nous formalisons la gradation d'un ordre, un opérateur de haut niveau qui transforme une relation binaire en une autre, et nous prouvons que la gradation d'un ordre conserve bon nombre de ses propriétés, telle que celle d'ordre monomial. Cela nous mène à la définition et aux propriétés de quatre ordres gradués différents, avec des preuves très factorisées. Nous mettons donc à disposition une bibliothèque Rocq sur les ordres complète et facile à utiliser, incluant les ordres monomiaux et gradués, qui contient plus de 700 lemmes.

**Mots-clés** : Assistant de preuve Rocq, formalisation des mathématiques, bibliothèque formelle, ordres
# Contents

<table><tr><td>1 Introduction</td><td>3</td></tr><tr><td>2 State of the Art</td><td>4</td></tr><tr><td>3 Basic Operators and Properties of Binary Relations</td><td>7</td></tr><tr><td>4 Lexicographic Orders</td><td>8</td></tr><tr><td>4.1 Lexicographic Order</td><td>8</td></tr><tr><td>4.2 Colexicographic Order</td><td>9</td></tr><tr><td>4.3 Symmetrical Lexicographic Order</td><td>10</td></tr><tr><td>4.4 Reverse Lexicographic Order</td><td>10</td></tr><tr><td>5 Monomial and Graded Orders</td><td>11</td></tr><tr><td>5.1 Monomial Order Definition</td><td>11</td></tr><tr><td>5.2 Graded Orders</td><td>11</td></tr><tr><td>Mathematical Definitions of Graded Orders</td><td>12</td></tr><tr><td>Formal Definitions of Graded Orders</td><td>14</td></tr><tr><td>6 Application, Conclusion & Perspectives</td><td>15</td></tr><tr><td>6.1 Application: Ordering of A<sub>k</sub><sup>d</sup></td><td>15</td></tr><tr><td>6.2 Conclusion</td><td>15</td></tr><tr><td>6.3 Weighted Orders</td><td>15</td></tr></table>

# List of Figures

<table><tr><td>1 Examples of multi-indices</td><td>5</td></tr><tr><td>2 Lex, colex, symlex, and revlex orderings in 2D</td><td>10</td></tr><tr><td>3 Grlex, grcolex, grsymlex, and grevlex orderings in 2D</td><td>12</td></tr><tr><td>4 Grlex, grcolex, grsymlex, and grevlex orderings in 3D</td><td>13</td></tr></table>

# 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].

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

<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>
of) the Finite Element Method, see [2, 3, 4], 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 [4]. 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, |\alpha| \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 $\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}^\alpha \stackrel{\text{def.}}{=} \prod_{i=0}^{d-1} X_i^{\alpha_i}$ (whose total degree is $|\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 $(\alpha \mapsto \mathbf{X}^\alpha)$ becomes a monotonic ordered monoid morphism. Namely, we consider a total order “<” on multi-indices that satisfies: for all $\alpha, \beta, \gamma \in \mathbb{N}^d$, $\alpha < \beta$ implies $\alpha + \gamma < \beta + \gamma$. Or equivalently, we consider a total order “<” on monomials that satisfies $\mathbf{X}^\alpha < \mathbf{X}^\beta$ implies $\mathbf{X}^\alpha \mathbf{X}^\gamma < \mathbf{X}^\beta \mathbf{X}^\gamma$. It is also generally required that for all nonzero $\alpha$, $1 = \mathbf{X}^0 < \mathbf{X}^\alpha$, or equivalently $\mathbf{0} < \alpha$. Moreover, it can be of interest to have a *graded* monomial order, i.e. that respects $|\alpha| < |\beta|$ (in $\mathbb{N}$) implies $\alpha < \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.

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, $\varepsilon$ 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 $\mathcal{A}_k^d$ and give some conclusive remarks and perspectives.

## 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,

<footnote n="4">⁴https://rocq-prover.org</footnote>

<footnote n="5">⁵https://rocq-prover.org/p/rocq-num-analysis/2.1.0</footnote>
<figure><img src="image_5.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>

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, and (strict) linear order. Moreover, two implementations provide support for ordered structures 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 provided 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.

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.

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

<footnote n="6">⁶https://isabelle.in.tum.de/library/HOL/</footnote>

<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>
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*.

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.

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.

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.

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 non-strict 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).

<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>

<footnote n="11">¹¹https://github.com/thery/grobner/</footnote>
## 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.<fnref n="12" />

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

**Definition converse**\texttt{: T → T → Prop := λ x y ⇒ R y x.**

**Definition complementary**\texttt{: T → T → Prop := λ x y ⇒ ¬ R x y.**

**Definition br_or_eq**\texttt{: T → T → Prop := λ x y ⇒ x = y ∨ R x y.**

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

**Definition transitive**\texttt{: Prop := ∀ x y z, R x y → R y z → R x z.**

**Definition negatively_transitive**\texttt{: Prop := ∀ x y z, ¬ R x y → ¬ R y z → ¬ R x z.**

**Definition reflexive**\texttt{: Prop := ∀ x, R x x.**

**Definition irreflexive**\texttt{: Prop := ∀ x, ¬ R x x.**

**Definition antisymmetric**\texttt{: Prop := ∀ x y, R x y → R y x → x = y.**

**Definition asymmetric**\texttt{: Prop := ∀ x y, R x y → ¬ R y x.**

**Definition connected**\texttt{: Prop := ∀ x y, x ≠ y → R x y ∨ R y x.**

**Definition strongly_connected**\texttt{: Prop := ∀ x y, R x y ∨ R y x.**

**Definition trichotomous**\texttt{: Prop := ∀ x y, (x = y ∧ ¬ R x y ∧ ¬ R y x) ∨ (x ≠ y ∧ R x y ∧ ¬ R y x) ∨ (x ≠ y ∧ R y x ∧ ¬ R x y).**

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

**Definition total_order**\texttt{: Prop := transitive R ∧ reflexive R ∧ antisymmetric R ∧ strongly_connected R ∧ negatively_transitive R ∧ connected R.**

**Definition strict_total_order**\texttt{: Prop := transitive R ∧ irreflexive R ∧ asymmetric R ∧ connected R ∧ negatively_transitive R ∧ antisymmetric R ∧ trichotomous R.**

**Definition strict_weak_order**\texttt{: Prop := negatively_transitive R ∧ irreflexive R ∧ asymmetric R ∧ transitive R ∧ antisymmetric R.**

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

**Lemma sto correct**\texttt{: strict_total_order R ↔ transitive R ∧ irreflexive R ∧ asymmetric R ∧ connected R.**

**Lemma sto-equiv_no_asym**\texttt{: strict_total_order R ↔ transitive R ∧ irreflexive R ∧ connected R.**

**Lemma stoequiv_no_irrefl**\texttt{: strict_total_order R ↔ transitive R ∧ asymmetric R ∧ connected R.**

<footnote n="12">¹²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>
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

**Lemma conv_asym**$\check{\wedge}$: asymmetric R $\rightarrow$ asymmetric (converse R).

**Lemma conv_to**$\check{\wedge}$: total_order R $\rightarrow$ total_order (converse R).

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

**Lemma asym Equiv Irrefl Antisym**$\check{\wedge}$: asymmetric R $\leftrightarrow$ irreflexive R $\wedge$ antisymmetric R.

**Lemma Irrefl Asym Equiv**$\check{\wedge}$: transitive R $\rightarrow$ irreflexive R $\leftrightarrow$ asymmetric R.

**Lemma trichotomy**$\check{\wedge}$: trichotomous R $\leftrightarrow$ asymmetric R $\wedge$ connected R.

**Lemma conn str conn**$\check{\wedge}$: reflexive R $\rightarrow$ connected R $\rightarrow$ strongly_connected R.

**Lemma trans neg trans**$\check{\wedge}$: connected R $\rightarrow$ transitive R $\rightarrow$ negatively_transitive R.

**Lemma sto equiv swo**$\check{\wedge}$: strict_total_order R $\leftrightarrow$ strict_weak_order R $\wedge$ connected R.

# 4 Lexicographic Orders

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.

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.

In the sequel, α and β denote any finite families in T^d. We use the following notations when d ≥ 2: the check notation $\tilde{\alpha} \in T^{d-1}$ denotes the last d − 1 components of α, 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\check{\wedge}.

## 4.1 Lexicographic Order

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

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

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

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

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 $<$ on T, the lexicographic order, or simply “lex” order, noted $<^{\text{lex}}$, can be recursively defined by

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

In Rocq, following Section 3, we consider any type T (defined as implicit Context in Rocq) and any binary relation R: T $\rightarrow$ T $\rightarrow$ 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 `lex R : ∀ n, 'T^n → 'T^n → 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.

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

**Lemma lex_nilsym : ∀ (x y : 'T^0), lex x y ↔ reflexive R**

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_Ssym : ∀ {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{ord0}$ and $y \text{ord0}$), 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 `skipF0Sym`).

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

$$ (4) \qquad \alpha \prec^{\text{colex}} \beta \quad \overset{\text{def.}}{\rightleftharpoons} \quad \bar{\alpha} \prec^{\text{lex}} \bar{\beta}. $$

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 → 'T^n → Prop$,

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

and `revFα := α`.
## 4.3 Symmetrical Lexicographic Order

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

$$ (5) \qquad \alpha \prec^{\text{symlex}} \beta \quad \overset{\text{def.}}{\iff} \quad \beta \prec^{\text{lex}} \alpha. $$

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** $\text{symlex}^\square \{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

$$ (6) \qquad \alpha \prec^{\text{revlex}} \beta \quad \overset{\text{def.}}{\iff} \quad \beta \prec^{\text{colex}} \alpha. $$

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** $\text{revlex}^\square \{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_6.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 [1]. 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*.

## 5.1 Monomial Order Definition

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

**Definition** `br_PLUSCompR` : `Prop` := $\forall x x_1 x_2, R x_1 x_2 \rightarrow R (x_1 + x) (x_2 + x)$.

Then, a monomial order is both a strict total order and `br_PLUSCompR`. 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** `lexmo` : `plus_is_reg_r G \rightarrow \forall \{R : G \rightarrow G \rightarrow Prop\}`, monomial_order $R \rightarrow \forall (n : nat)$, 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><tr><td>grlex &lt;</td><td>Z<sup>3</sup></td><td>Y<sup>3</sup></td><td>XYZ</td><td>XY<sup>2</sup></td><td>X<sup>3</sup></td></tr><tr><td>grcolex &lt;</td><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><td>grsymlex &lt;</td><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><td>grevlex &lt;</td><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></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 \underset{\text{def}}{\implies} \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 \begin{cases} |\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 \ \tilde{\alpha} <_{\text{grlex}} \tilde{\beta}. \end{cases} $$

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

<figure><img src="image_8.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>

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

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

$$ \alpha <_{\text{grcolex}} \beta \quad \underset{\text{def}}{\implies} \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

$$ (7) \qquad \alpha <_{\text{grsymlex}} \beta \quad \underset{\text{def}}{\implies} \quad \begin{cases} |\alpha| < |\beta|, & \text{or} \\ |\alpha| = |\beta|, & \alpha <_{\text{symlex}} \beta. \end{cases} $$

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.
<figure><img src="image_9.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).

We have an alternative recursive definition,

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

but it may be simplified,

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

as when $|\alpha| = |\beta|$ and $\beta_0 < \alpha_0$, we have $d \ge 2$ and $|\tilde{\alpha}| < |\tilde{\beta}|$, i.e. $\tilde{\alpha} <^{\text{grsymlex}} \tilde{\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| \wedge \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 \left\{ \begin{array}{l} |\alpha| < |\beta|, \text{ or} \\ |\alpha| = |\beta| \wedge \alpha <^{\text{revlex}} \beta. \end{array} \right. $$

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 \left\{ \begin{array}{l} |\alpha| < |\beta|, \text{ or} \\ |\alpha| = |\beta| \wedge d \ge 2 \wedge \tilde{\alpha} <^{\text{grevlex}} \tilde{\beta}, \end{array} \right. $$

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$,

**Definition grlex** $\mathscr{G} : (x, y : 'G^n) : \mathbf{Prop} := (\mathrm{sum} x \neq \mathrm{sum} y \wedge R (\mathrm{sum} x) (\mathrm{sum} y)) \vee (\mathrm{sum} x = \mathrm{sum} y \wedge 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** $\mathscr{G} := \text{graded } R$ (lex $R$).

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

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

**Definition grevlex** $\mathscr{G} := \text{graded } R$ (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,

**Lemma graded mo** $\mathscr{G} : \mathrm{plus\_is\_reg\_r} G \to \mathrm{monomial\_order} R \to \mathrm{monomial\_order} Rn \to \mathrm{monomial\_order} (\text{graded R Rn})$.

It is therefore straightforward to prove that `grsymlex lt` is a monomial order (`grsymlex lt mo`).

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

**Lemma graded idem** $\mathscr{G} : \forall \{R1\} R2 \{n\} \{Rn : 'G^n \to 'G^n \to \mathbf{Prop}\}$, $\text{graded R1 (graded R2 Rn)} = \text{graded R1 Rn}$.
When grading with respect to $\mathbb{R}_2$ (on $\mathbb{G}$) and then $\mathbb{R}_1$ (on $\mathbb{G}$ too), it is equivalent to only grading with respect to $\mathbb{R}_1$. This may allow us to remove one graded out of two. For instance, when $\mathbb{R}_1=\mathbb{R}_2$, it means that graded $\mathbb{R}$ (grsymlex $\mathbb{R}$) = grsymlex $\mathbb{R}$. And for different orders on $\mathbb{N}$, we can prove for instance that graded $\mathbb{gt}$ (grcolex $\mathbb{lt}$) = graded $\mathbb{gt}$ (colex $\mathbb{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{P}_k^d$, the $d$-multivariate polynomials of degree smaller or equal to $k$ (see file multi_index.c). 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 = \bigcup_{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 = \bigcup_{i=0}^{l} \{(i, \tilde{\beta}) \in \mathbb{N}^d | \tilde{\beta} \in C_{l-i}^{d-1}\} = \bigcup_{i=0}^{l} \{(\tilde{\beta}, i) \in \mathbb{N}^d | \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 = \bigcup_{i=0}^{l} \{(l - i, \tilde{\beta}) \in \mathbb{N}^d | \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 $\mathbb{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 irreflexivity), 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 = [\mathbf{w}_0 | W_{1...m-1}]$, where $\mathbf{w}_0 \in K^d$ and $W_{1...m-1}$ is in $K^{d,m-1}$,

$$ (10) \qquad \mathbf{x} <^W \mathbf{y} \quad \overset{\text{def.}}{\iff} \quad \left\{ \begin{array}{l} \mathbf{x} \cdot \mathbf{w}_0 <_K \mathbf{y} \cdot \mathbf{w}_0, \text{ or} \\ \mathbf{x} \cdot \mathbf{w}_0 = \mathbf{y} \cdot \mathbf{w}_0 \quad \wedge \quad \mathbf{x} <^{W_{1...m-1}} \mathbf{y}. \end{array} \right. $$

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, 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.

[2] 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.

[3] 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.

[4] 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/.

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

[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.

[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.

[8] Matthias Ehrgott. *Multicriteria Optimization*. Springer, Berlin, Heidelberg, 2nd edition, 2005. URL https://doi.org/10.1007/3-540-27659-9.
[9] Ralf Fröberg. *An Introduction to Gröbner Bases*. John Wiley & Sons, 1997.

[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.

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

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

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

[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/1161802720.

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

[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.
<figure><img src="image_10.png" /></figure>

RESEARCH CENTRE
Centre Inria de Saclay

Bâtiment Alan Turing
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
91120 Palaiseau

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399