TLC: a non-constructive library for CoqTLC 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.
TLC is used in particular in CFML and FormalMetaCoq. Download- The source files are available from TLC's GitHub repository.
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.
Related publicationsArthur Charguéraud ITP: International Conference on Interactive Theorem Proving, July 2010 |