This is the CoLoR library version 1.4.0. Check http://color.inria.fr/ for more recent versions. CoLoR is a library for the Coq proof assistant/checker (http://coq.inria.fr/) providing definitions and theorems about the termination/well-foundedness of arbitrary relations and rewrite relations on various term structures. Among other things, it includes: * libraries on logic in the Util/ subdirectory: - Logic: meta-theorems, tactics, possible axioms * libraries on mathematical structures in the Util/ directory: - Set: (infinite) sets - Relation: (infinite) binary relations/graphs - Algebra: (ordered) semi-rings * libraries on data structures in the Util/ subdirectory: - Bool: booleans - Option: option type - Nat: natural numbers - Integer: integers - Pair: type of pairs - List: lists - Vector: vectors - FSet: finite sets - FMap: finite maps - Multiset: finite multisets - Polynom: integer polynomials with multiple variables - Matrix: matrices over an (ordered) semi-ring - FGraph: finite graphs * libraries on term structures in the Term/ subdirectory: - String: words - Varyadic: varyadic terms - WithArity: algebraic terms with symbols of fixed arity - SimpleType: simply typed lambda-terms with de Bruijn indices - Lambda: lambda-terms with explicit alpha-equivalence * transformation techniques: - Conversion: conversions between term structures - DP: dependency pairs transformation and graph decomposition - Filter: arguments filterings - SemLab: semantic labeling * (non-)termination criteria: - MannaNess: inclusion in some reduction ordering - PolyInt: polynomial interpretations - MatrixInt: matrix interpretations - MPO: multiset path ordering - RPO: recursive path ordering - HORPO: higher-order recursive path ordering - NonTermin: loop certification - SubtermCrit: subterm criterion (unfinished) - Term/Lambda: computability closure Contributions to this project are very welcome! LICENSE: this file describes the license governing this library. COPYRIGHTS: this file describes the copyrights holders. INSTALL: this file describes a compilation procedure. THANKS: thanks to various people for their comments or help. CHANGES: this file briefly describes the main changes between two releases. The development version is available on https://github.com/fblanqui/color . The following scripts provide some statistics: - coq_stat [<directory>] (default is .): provides the number of definitions, lemmas, etc. - color_stat: provides the number of Coq lines (including newlines and comments) for the various kinds of formalizations (mathematical structures, data structures, etc.) 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.