Metatheory library - Documentation

The Penn PLClub has developed, and continues to work on, a collection of Coq libraries for mechanizing programming language metatheory in the Coq proof assistant. The original design and implementation of the library includes work by Arthur Charguéraud and was distributed with Engineering Formal Metatheory. The library has evolved since then, but its purpose has remained the same.

Installation

To compile this library, run 'make coq' in the directory containing all of the .v files. If you don't have make, run the following commands. (You may need to replace coqc with the full path to the executable.)

      coqc -q  -I . CoqFSetDecide.v
      coqc -q  -I . CoqUniquenessTac.v
      coqc -q  -I . CoqListFacts.v
      coqc -q  -I . LibTactics.v
      coqc -q  -I . AssocList.v
      coqc -q  -I . CoqEqDec.v
      coqc -q  -I . CoqFSetInterface.v
      coqc -q  -I . CoqUniquenessTacEx.v
      coqc -q  -I . FSetExtra.v
      coqc -q  -I . FSetWeakNotin.v
      coqc -q  -I . LibDefaultSimp.v
      coqc -q  -I . MetatheoryAtom.v
      coqc -q  -I . Metatheory.v
      coqc -q  -I . LibLNgen.v
      coqc -q  -I . AssumeList.v
      coqc -q  -I . MetatheoryAlt.v
      coqc -q  -I . Fsub_LetSum_Definitions.v
      coqc -q  -I . Fsub_LetSum_Infrastructure.v
      coqc -q  -I . Fsub_LetSum_Lemmas.v
      coqc -q  -I . Fsub_LetSum_Soundness.v
      coqc -q  -I . CoqIntro.v
      coqc -q  -I . STLCsol.v

To use the library in your development, do one of the following:

Put your development in the same directory as the library.
Use Add LoadPath directives in your files to specify the location of the library.
Use the -I flags to the Coq executables (coqtop, coqide, and coqc) to specify the location of the library.

Documentation

The metatheory library consists of quite a few files. From a user's perspective, the main files are the ones below. Documentation for the others can be reached by following links or by looking in the doc/html/ directory of the distribution.

Metatheory: This is the library to Require, since it exports all the useful libraries that come with the metatheory library. It adds to those libraries a collection of hints and notations that makes them easier to use. It also defines a tactic for working with cofinite quantification.
MetatheoryAtom: An implementation of atoms, an infinite collection of structureless objects with decidable equality, and finite sets of atoms. One can generate an atom fresh from a given finite set of atoms. The implementation of finite sets of atoms is based on Coq's FSets library and includes several tactics for reasoning about finite sets.
AssocList: A library for association lists. The implementation is a functor parameterized over the type of keys. Association lists are suitable for representing the environments that show up in programming language metatheory. The Metatheory library instantiates this library so that the keys are atoms.

Tutorials and examples

The library comes with two tutorials and one extended example. The first tutorial, CoqIntro.v, is a general introduction to Coq. Solutions to exercises are at the end of the file. The second tutorial, STLC.v, is an introduction to locally nameless representations and the metatheory library using the simply typed lambda calculus as a running example. Solutions to exercises are in STLCsol.v. The extended example, in the files Fsub_*.v, is System F with subtyping, extended with let-bindings and sum types. We prove preservation and progress for this language.

Unstable code

MetatheoryAlt is an alternate version of the Metatheory library that uses "assumption lists", as implemented in AssumeList. This implementation lags behind the "main" one and is subject to change radically in future releases.

Contact

If you have any questions about the library, feel free to contact Brian Aydemir.