Coq library on rewriting theory and termination
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Coccinelle
Conversion
DP
Filter
HORPO
MPO
MannaNess
MatrixInt
NonTermin
PolyInt
ProofChecker
RPO
SemLab
SubtermCrit
Term
Util
doc
.gitignore
.travis.yml
CHANGES
COPYRIGHTS
INSTALL
LICENSE
Licence_CeCILL_V2.1-en.txt
Licence_CeCILL_V2.1-fr.txt
Makefile
README
README.devel
THANKS
TODO
create_dist
create_index
description
stat_color
stat_coq
stat_time
stat_time.awk
svn_mv_coq
time_coqc

README

This is the CoLoR library version 1.5.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.