llelf / color Goto Github PK

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