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.

Download

  • The source files can be obtained by running:
    git clone https://gitlab.inria.fr/charguer/tlc.git
  • TLC compiles with Coq v8.5 (there is also a branch for Coq v8.6).
  • A complete clean-up is under progress.
  • Read the Makefile in case you need to use Coq binaries that are not in your path.
  • 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

Warning: for the most recent version of the files, please check out the git repository.

Related publications

The Optimal Fixed Point Combinator
Arthur Charguéraud
ITP: International Conference on Interactive Theorem Proving, July 2010