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