Tealeaves is a Coq framework for proving theorems about syntax abstractly, i.e. independently of a concrete grammar. This independence makes syntactical theory reusable between developments, and is achieved by separating a choice of grammar from a choice of variable representation. Our central abstraction is a "structured" kind of monad that we call decorated traversable, which is an abstraction of abstract syntax trees. Tealeaves "core" is a Coq implementation of the equational theory of such monads, as well as higher-level principles built on top of this theory.
System requirements:
make(see GNU Make)- An installation of Coq >= 8.13 (see the Coq downloads page).
Compilation instructions:
- Run
makein the top-level directory - Run
make cleanto remove all build artifacts (including compiled files) and start over
We have tested with Coq 8.13, but other versions may work too. We observe a compilation time of approximately 4-5 minutes on a typical desktop computer. On multicore systems you may want to use the -j flag to use several build threads. We have sometimes observed that -j leads to cryptic build errors. The solution to these is simply to re-run the build command again.
Tealeaves is built with the coq_makefile, which is distributed with Coq itself. This utility generates a customized Makefile to build a Coq project. For simplicity, we provide a top-level Makefile which will call coq_makefile for you, and then recursively call make on the generated Makefile, so that you should not have to do anything except call make once in the top-level directory.
Pretty-printed HTML documentation is generated by default in the html/ directory.
Classes of "structured" functors (like monads, decorated monads, traversable functors, etc.) are found in under Tealeaves/Classes. The internal implementation of Tealeaves uses an algebraic rather than Kleisli-style implementation of our typeclasses, so that operations like bind are derived rather than taken as primitive. For example, decorated monads are defined here as monads equipped with a "decoration" operation. Their equivalent Kleisli presentation is derived here in the same file. A characterization of decorated functors as comodules of the reader/writer bimonad is found here.
Our locally nameless backend library is formalized under the LN/ directory. The operations (opening, closing, local closure, etc) are defined here. Various lemmas about these operations, proved polymorphically over a decorated traversable monad T, are proved here.
Our formalization of STLC is under the STLC/ directory. A formalization of STLC's syntax as a DTM is found here. Basic metatheory such as a progress theorem are proved here.
Our multisorted classes live under Multisorted/. Our extension of the locally nameless backend lives under LN/Multisorted/. SystemF lives under SystemF.
| Tealeaves Typeclasses | Functor | Monad |
|---|---|---|
| Plain | Classes/Functor.v | Algebraic / Kleisli |
| Decorated | Algebraic / Kleisli | Algebraic / Kleisli |
| Traversable | Algebraic / Kleisli | Algebraic / Kleisli |
| Decorated+Traversable | Algebraic / Kleisli | Algebraic / Kleisli |
Tealeaves currently uses two axioms commonly used in Coq formalizations, which have been proven (on paper) to be equi-consistent with Coq itself. They are the following.
- Propositional extensionality, which says that equivalent propositions (
P <-> Q) are propositionally equal (P = Q) - Functional extensionality, which is the statement
forall x, f x = g x -> f = g.
There axioms are assumed here. They are a convenience to use Coq's rewriting features. In principle one can eliminate these at the cost of ``setoid hell'' (see this question on StackOverflow).