A Rocq Formalization of Monomial and Graded Orders

TL;DR

This paper formalizes monomial and graded orders within Rocq, providing a comprehensive library with definitions, properties, and proofs to support finite element method formalization.

Contribution

It introduces a detailed Rocq library for monomial and graded orders, including definitions, operators, and proofs, with over 700 lemmas, enhancing formalization tools.

Findings

Formalization of monomial orders and their properties

Definition and proof of properties for graded orders

Development of a comprehensive Rocq library with extensive lemmas

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.