TLC: a non-constructive library for Coq
TLC is a general purpose Coq library that provides an alternative to Coq's standard library.
- TLC takes as axiom extensionality, classical logic and indefinite description (Hilbert's epsilon). These axioms allow for significantly simpler formal definitions in many cases.
- TLC takes advantage of the type class mechanism. In particular, this allows for common operators and lemma names for all container data structures and all order relations.
- TLC includes the optimal fixed point combinator, which can be used for building arbitrarily-complex recursive and co-recursive definitions.
- TLC provides a collection of tactics that enhance the default tactics provided by Coq. These tactics help constructing more concise and more robust proof scripts.
- The source files are available from GitHub:
git clone https://github.com/charguer/tlc
- For installation instruction, check the README file.
- Disclaimer: to allow improving the design of TLC, backward compatibility is in no way guaranteed.
- TLC can be used in conjonction with the standard library, although TLC redefines a number of operations in order to keep the dependencies onto the standard library to the minimum.
- All the files are distributed under the MIT X11 license.
ITP: International Conference on Interactive Theorem Proving, July 2010