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.
Download- The source files can be obtained by running:
svn checkout svn://scm.gforge.inria.fr/svn/tlc/branches/v3.1 tlc - TLC version 3.1 compiles with Coq v8.4 (use tlc/branches/v3 for Coq-v8.3).
- TLC can be used in conjunction with the standard library.
- All the files are distributed under the GNU-LGPL license.
Tutorials| Overview of most useful tactics | | | Tutorial: using tactics | | | Tutorial: integrated automation | | | Tutorial: classic, non-constructive logic | | | Demos: tactics | | | Demos: optimal fixed points | |
Formal libraries (stable files only)| Tactics | | | Logic | | | Relations | | | Base types | | | Fixed points | | | Containers | | | Metatheory | |
Related publicationsThe Optimal Fixed Point Combinator International Conference on Interactive Theorem Proving (ITP), July 2010 |