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 Coq proof assistant. See
this paper
for some presentation. More papers are provided in
this bibliography. Contributions are
welcome!
Mailing list: For announcements and discussions
about this project, create an account
on https://sympa.inria.fr/, log
in and subscribe
to color.
Download: This library is distributed under the
terms of the French free software
license CeCILL,
that is compatible with the GNU General Public License. Read
the conditions
of the license
before downloading
the library. The development version is available
on Github.
Last release: version 1.5 for Coq 8.8, 4 May 2018 (see CHANGES)
CoLoR is now available on OPAM. Installation procedure:
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 Coq 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 Coq 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)
