Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Rocq Formalization of Monomial and Graded Orders

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

TL;DR

The paper develops a Rocq-based formalization of monomial and graded orders to support finite element method formalization, establishing a library of definitions, operators, and proofs for binary relations and several vector orders. It builds from core binary-relations theory to lex, colex, symlex, and revlex, then introduces monomial orders and a general graded-operator framework that yields four graded monomial orders. The work includes detailed mathematical and Rocq-specific definitions for graded orders (grlex, grcolex, grsymlex, grevlex) and proves their monomial-order properties, along with applications to ordering multi-indices $ abla A^{d}_{k}$ and a discussion of weighted orders. Overall, it delivers a large, modular, and reusable Rocq library with hundreds of lemmas to facilitate formal reasoning in algebraic and numerical contexts, notably for Gröbner-bases-related computations and FEM discretizations.

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.

A Rocq Formalization of Monomial and Graded Orders

TL;DR

The paper develops a Rocq-based formalization of monomial and graded orders to support finite element method formalization, establishing a library of definitions, operators, and proofs for binary relations and several vector orders. It builds from core binary-relations theory to lex, colex, symlex, and revlex, then introduces monomial orders and a general graded-operator framework that yields four graded monomial orders. The work includes detailed mathematical and Rocq-specific definitions for graded orders (grlex, grcolex, grsymlex, grevlex) and proves their monomial-order properties, along with applications to ordering multi-indices and a discussion of weighted orders. Overall, it delivers a large, modular, and reusable Rocq library with hundreds of lemmas to facilitate formal reasoning in algebraic and numerical contexts, notably for Gröbner-bases-related computations and FEM discretizations.

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.

Paper Structure

This paper contains 17 sections, 19 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. State of the Art
  3. Basic Operators and Properties of Binary Relations
  4. Lexicographic Orders
  5. Lexicographic Order
  6. Colexicographic Order
  7. Symmetrical Lexicographic Order
  8. Reverse Lexicographic Order
  9. Monomial and Graded Orders
  10. Monomial Order Definition
  11. Graded Orders
  12. Mathematical Definitions of Graded Orders
  13. Formal Definitions of Graded Orders
  14. Application, Conclusion & Perspectives
  15. Application: Ordering of $\mathcal{A}^{d}_{k}$
  16. ...and 2 more sections

Figures (4)

  • Figure 1: Multi-indices $\mathcal{A}^{d}_{k}$ 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$.
  • Figure 2: Lex, colex, symlex, and revlex orderings (from left to right) of $\mathcal{A}^{d}_{k}\subset\mathbb{N}^d$ when $d=2$ and $k=3$. The increase in the order is represented by dashed arrows. For $\mathcal{A}_3^2$, we have 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)$.
  • Figure 3: Grlex, grcolex, grsymlex, and grevlex orderings of $\mathcal{A}^{d}_{k}$ 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 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)$
  • Figure 4: Grlex, grcolex, grsymlex, and grevlex orderings of $\mathcal{A}^{d}_{k}$ when $d=k=3$. The increase in the order is represented by dashed arrows, only when the sum $l=3$ (see Figure \ref{['f:lag-k3-d2-d3']}). The four orders are different. For the multi-indices of sum 3, we have grlex$(0,0,3)<(0,1,2)<(0,2,1)<(0,3,0)<(1,0,2)<(1,1,1)<(1,2,0)<(2,0,1)< (2,1,0)<(3,0,0)$grcolex$(3,0,0)<(2,1,0)<(1,2,0)<(0,3,0)<(2,0,1)<(1,1,1)<(0,2,1)<(1,0,2)< (0,1,2)<(0,0,3)$grsymlex$(3,0,0)<(2,1,0)<(2,0,1)<(1,2,0)<(1,1,1)<(1,0,2)<(0,3,0)<(0,2,1)< (0,1,2)<(0,0,3)$grevlex$(0,0,3)<(0,1,2)<(1,0,2)<(0,2,1)<(1,1,1)<(2,0,1)<(0,3,0)<(1,2,0)< (2,1,0)<(3,0,0)$The restriction of grsymlex to the last two components when the sum is 3, is exactly grsymlex for $d=2$ (see Figure \ref{['f:tria_k3_graded']}, right).

Theorems & Definitions (1)

  • Definition