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
, andcoqc
) 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 letbindings 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.