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 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 publications

Arthur Charguéraud
ITP: International Conference on Interactive Theorem Proving, July 2010