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 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 . AdditionalTactics.v
      coqc -q -I . Atom.v
      coqc -q -I . ListFacts.v
      coqc -q -I . PennFSetDecide.v
      coqc -q -I . AssocList.v
      coqc -q -I . FSetWeakNotin.v
      coqc -q -I . AtomSet.v
      coqc -q -I . AtomEnv.v
      coqc -q -I . Metatheory.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 library is roughly divided into three parts: auxiliary libraries, main libraries, and a library to pull everything together.

Auxiliary libraries

AdditionalTactics: General purpose tactics that are not included with Coq. The ones for delineating cases in proofs are particularly useful.
AssocList: An implementation of association lists, i.e., lists of pairs of keys and values.
ListFacts: Assorted facts about lists.
FSetWeakNotin: A tactic for proving particular forms of non-membership facts about finite sites.
PennFSetDecide: Our version of Coq's FSetDecide library, where we have fixed a few bugs.

Main libraries

Atom: An implementation of atoms, an infinite collection of structureless objects with decidable equality. One can generate an atom fresh from a given finite list of atoms.
AtomSet: An implementation of finite sets of atoms based on Coq's FSets library. It provides tactics for reasoning about finite sets of atoms and for generating fresh atoms.
AtomEnv: Association lists where the keys are atoms. These are suitable for representing the environments that show up in programming language metatheory. This is actually a specialization of the AssocList library.

Pulling everything together

Metatheory: This is the library to Require, since it pulls together the above libraries by declaring hints and notations that make them easier to use. It also defines a tactic for working with cofinite quantification.

Contact

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