CoLoR, a Rocq library on rewriting theory and termination

CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory, λ-calculus and termination whose correctness has been mechanically checked by the Rocq proof assistant. See this paper for some presentation. More papers are provided at the end of this file.

Some developments using CoLoR: Rainbow, HA-Spiral, Spi, ATBR, CPV.

Installation:

Installation with opam:

opam repo -a --set-default add rocq-released https://rocq-prover.org/opam/released # once
opam install rocq-color

You can browse the definitions and statements by doing in the source directory make doc and read doc/index.html in your browser.

Scripts:

CoLoR provides also useful scripts for doing statistics:

• do make time to record the compilation time of each file (then time_coqc is used instead of coqc)
• do ./stat_time to get statistics on compilation time
• ./stat_coq [<directory>] (default is .) provides the number of definitions, lemmas, etc.
• ./stat_color provides the number of Rocq lines (including newlines and comments) for the various kinds of formalizations (mathematical structures, data structures, etc.)

Library contents:

• Logic: libraries providing basic meta-theorems and tactics (e.g. irreflexivity) on propositions and equality, both for intuitionistic and classical logic, the statement of the axiom of dependent choice, etc.

• Mathematical structures:

  • finite and infinite sets: cardinal of a finite set, infinite pigeon-hole principle, infinite Ramsey theorem
  • infinite relations/graphs: an extensive library of definitions and theorems on relations including basic operations like union/intersection/composition/iteration or reflexive/transitive/symmetric closure, their relations, the notions of finite path, cycle, strongly connected component, infinite path/rewrite sequence, etc.
  • finite relations/graphs: adjacency matrix, computation and topological sorting of strongly connected components, etc.
  • (quasi) orderings: linear extension of a finite acyclic relation, Tarski's fixpoint theorem (in a complete lattice, any monotone function has a least/greatest fixpoint), etc.
  • well-founded relations: preservation of termination for commuting relations, maximal reduction length of an element wrt a well-founded finitely branching relation, relation between the classical notion of termination (absence of infinite paths) and the intuitionistic one (inductive accessibility), etc.
  • (ordered) semi-rings: a library on semi-rings and ordered semi-rings, and its instantiation on various number data structures (natural numbers, integers, arctic/tropical numbers, etc.)

• Data structures:

  • libraries extending the Rocq standard library on various data structures: booleans, natural numbers, integers, pairs, lists, vectors, finite sets, finite maps, sets, relations, etc.
  • natural numbers: list of natural numbers smaller than some bound, least natural number satisfying some property, logarithmic to base 2, decidability of equality on bigN, maximum/minimum of a list of natural numbers, etc.
  • lists: an extensive library extending the Rocq standard library on lists including many functions and theorems on lists including for instance the number of occurrences of an element, lists with no duplicated elements, a constructive proof of the pigeon-hole principle, lemmas on the permutation of elements, etc.
  • vectors: an extensive library on vectors including many basic functions and theorems on vector manipulation, vector product/lexicographic ordering, vector arithmetic, vector components filtering and permutation
  • matrices: a library on matrices including basic functions and theorems on matrix arithmetic
  • finite multisets: a library on finite multisets including a proof that the multiset extension of a well-founded relation is well-founded
  • polynomials with multiple variables: a library on integer polynomials with multiple variables including basic functions and theorems on polynomial arithmetic, positivity and monotony
  • finite graphs: a library on finite graphs including a certified algorithm for computing its transitive closure (using a successor function representation) or its strongly connected components (using the adjacency matrix representation)

• Term structures:

  • strings/words: definition of basic notions like context and rewriting
  • varyadic terms (first-order terms with function symbols taking an arbitrary number of arguments): definition of basic notions like substitution, context, rewriting on varyadic terms
  • algebraic terms with function symbols of fixed arity: this is the most developed library on terms including many definitions and theorems on terms and term rewrite relations like the basic notions of substitution, context, subterm, position, cap and aliens, dependency pair, etc.; the notion of model/interpretation (universal algebra); a certified algorithm for matching; a certified algorithm for unification; etc.
  • simply typed λ-terms with de Bruijn indices
  • pure and simply typed λ-terms with named variables and explicit α-equivalence: definitions and properties of the basic notions of (higher-order) substitution, α-equivalence, β-reduction, etc.; the equivalence of various definitions of α-equivalence (Curry-Feys, Church, Krivine, Gabbay-Pitts); Girard computability predicates; computability closure; strong normalization of β-reduction and higher-order rewrite systems (e.g. Gödel' system T)

• Transformation techniques:

  • conversion string → algebraic term → varyadic term (CoLoR provides in particular a translation from CoLoR algebraic terms to Coccinelle terms to allow the reusability of Coccinelle results in CoLoR)
  • reversal of SRSs and unary TRSs
  • arguments filtering
  • dependancy pairs transformation
  • dependency graph decomposition
  • semantic labeling
  • flat context closure

• (Non-)Termination criteria:

  • first and higher order recursive path ordering (RPO and HORPO)
  • integer polynomial interpretations
  • integer/arctic/tropical matrix interpretations
  • computability closure for higher-order rewrite systems
  • loops (a decision procedure for verifying that a given rewrite sequence is a loop)

The directory Coccinelle is not part of CoLoR. It contains an adaptation of the Coccinelle library which is used in Conversion/Coccinelle.v. See Coccinelle/README for more information.

Contributors:

Maintainer: Frédéric Blanqui (INRIA, France)

Contributors: Kim-Quyen Ly (INRIA), Sidi Ould-Biha (INRIA, France), Adam Koprowski (Radboud University, The Netherlands), Johannes Waldmann (Leipzig HTWK, Germany), Sorin Stratulat (Université Paul Verlaine, Metz, France), Julien Bureaux (ENS Paris, France), Pierre-Yves Strub (INRIA, France), Wang Qian (Tsinghua University, China), Zhang Lianyi (Tsinghua University, China), Hans Zantema (Radboud University, Nijmegen, The Netherlands), Jörg Endrullis (Amsterdam Vrije Universiteit, The Netherlands), Stéphane Le Roux (ENS Lyon, France), Léo Ducas (ENS Paris, France), Solange Coupet-Grimal (Université de Provence Aix-Marseille I, France), William Delobel (Université de Provence Aix-Marseille I, France), Sébastien Hinderer (LORIA, France), Frédéric Blanqui (INRIA, France)

Bibliography:

• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. F. Blanqui and A. Koprowski, MSCS 21(4):827-859, 2011.

• Coq formalization of the higher-order recursive path ordering, A. Koprowski, Applicable Algebra in Engineering Communication and Computing 20(5-6):379-425, 2009.

• Automated Verification of Termination Certificates, F. Blanqui and A. Koprowski, INRIA Research Report 6949, 2009.

• Automated Verification of Termination Certificates, F. Blanqui, Talk at East China Normal University, Shanghai, 3 December 2008.

• Termination of rewriting and its certification, A. Koprowski, PhD Thesis, 2008.

• Certification of Proving Termination of Term Rewriting by Matrix Interpretations, A. Koprowski and H. Zantema, SOFSEM'08.

• Arctic termination... below zero, A. Koprowski and J. Waldmann, RTA'08.

• Acyclicity and Linear Extendability: a Formal and Constructive Equivalence, S. Le Roux, TPHOL'07.

• Certification of Matrix Interpretations in Coq, A. Koprowski and H. Zantema, WST'07.

• Certification de preuves de terminaison basées sur la décomposition du graphe des paires de dépendance, L. Ducas, B. Sc. thesis, 2007.

• CoLoR, a Coq Library on Rewriting and termination, F. Blanqui, S. Coupet-Grimal, W. Delobel, S. Hinderer and A. Koprowski, WST'06. [slides]

• A Formalization of the Simply Typed Lambda Calculus in Coq, A. Koprowski, draft, 2006.

• A Constructive Axiomatization of the Recursive Path Ordering, S. Coupet-Grimal and W. Delobel, Research report 28, LIF, Universit&eacute de la Méditerranée, 2006.

• An Effective Proof of the Well-Foundedness of the Multiset Path Ordering, S. Coupet-Grimal and W. Delobel, Applicable Algebra in Engineering Communication and Computing 17(6):453-469, 2006.

• Certified Higher-Order Recursive Path Ordering, A. Koprowski, RTA'06.

• Une preuve effective de la bonne fondation de l'ordre récursif multi-ensemble sur les chemins, S. Coupet-Grimal and W. Delobel, JFLA'06.

• Well-foundedness of the Higher-Order Recursive Path Ordering in Coq, A. Koprowski, Master thesis, 2004.

• Certification des preuves de termination par interprétations polynomiales, S. Hinderer, Master thesis, 2004.

• Well-foundedness of the Recursive Path Ordering in Coq, N. de Kleijn, A. Koprowski and F. van Raamsdonk, Dutch Proof Tools Day, 2004.

• Well-foundedness of RPO in Coq, N. de Kleijn, Master thesis, 2003.