Metatheory library
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.
Installation instructions
- Install an appropriate version of Coq according to the instructions distributed with it. It should not matter whether you install a binary package or compile it from source. In addition to the resources available through Coq's homepage, the POPLmark wiki also contains some tips on installing Coq.
- Download the metatheory library distribution (see the link above).
- Unpack the zip file.
- To install the library globally:
- Unpack the zip file and copy the resulting directory to some
location within Coq's
theories
directory, e.g.,theories/metatheory
. The exact location oftheories
will depend on how you installed Coq. - Run
make
within the directory. - You should now be able to import the library,
e.g.,
Require Import Metatheory
, without any other commands or options to Coq.
- Unpack the zip file and copy the resulting directory to some
location within Coq's
- The library can also be used locally by unpacking the zip file
and copying all the
.v
files to the same directory as the Coq development with which you wish to use the library. Compile the library using the same means as you would to compile your development. - Note that the distribution includes a
README.txt
file, and adoc
directory that contains a copy of this web page and the HTML documentation linked to below.
Documentation
The library is roughly divided into three parts: auxiliary libraries, main libraries, and a library to pull everything together.
Auxiliary libraries
Generic additions to Coq's standard library:
- AdditionalTactics: This library contains general purpose tactics that are not included with Coq. The tactics for delineating cases in proofs are particularly useful since programing language metatheory typically contains inductive proofs with many cases.
- ListFacts: This library contains assorted facts about lists. It is not specifically geared towards programming language metatheory, but the facts may be useful anywhere one uses lists in a development.
Libraries that extend Coq's FSets library:
- FSetWeakDecide: This
library provides a decision procedure (as the
tactic
fsetdec
) for solving goals about finite sets, as implemented by Coq's FSets library. Some form of this library and tactic are likely to be included with Coq 8.2. - FSetWeakNotin: This
library provides a tactic
solve_notin
that solves particular forms of non-membership goals about finite sites. This tactic is strictly less powerful thanfsetdec
. However, it seems to behave more predictably when used as a hint for Coq'sauto
andeauto
tactics:fsetdec
's use of rewriting can interact poorly with existential variables in goals. The tactic is intended to discharge the many freshness goals that appear in programming language metatheory.
Main libraries
Support for names:
- Atom: This library provides an implementation of atoms, structureless objects with a decidable equality relation. It is also possible to generate an atom fresh for a finite collection of atoms.
- AtomSet: This library provides
an implementation of finite sets of atoms using Coq's FSets library.
It also instantiates the finite set tactics provided by
FSetWeakDecide
and FSetWeakNotin. Note that
the tactics are named here as
atomsetdec
andsolve_atomset_notin
. This library also defines a "pick fresh
" tactic for generating an atom fresh for given finite set.
Support for environments:
- AssocList: This library provides a functor which implements association lists, i.e., lists of pairs of keys and values, over a given type of keys. It provides basic functions and predicates on association lists, as well as properties of those functions and predicates. Association lists can be used to represent, for example, the environments that appear in programming language definitions.
- AtomEnv: This library provides a
signature for the functor
in AssocList where the keys have
been specialized to atoms. Such association lists can be used to
represent environments (a.k.a. contexts). To reflect this fact,
tactics whose names ended in "
alist
" now end in "env
". (Coq's module system does not require that tactics be defined identically in a module signature and its implementation.) Note: This library is automatically generated from AssocList. As a result, some of the documentation may not quite fit.
Pulling everything together
- Metatheory: By design, the
libraries above do not declare many hints or define many notations.
The intent is for users to glue the libraries together in some
fashion that suits their particular needs and preferences.
The Metatheory library provides a
reasonable default combination of the libraries above. In addition
to declaring an assortment of hints and notations, it also defines a
tactic for working with cofinite quantification. Users of the
metatheory library (as a whole) can simply
Require Import Metatheory
to get started on their developments.
Additional reading
The metatheory library was originally developed to support the paper
Engineering
Formal Metatheory. (The link is to the ACM Digital Library.
The paper is also available from the authors' homepages.) The
"pick fresh and apply
" tactic, defined
in Metatheory, supports working
with the cofinite quantification technique discussed in that paper.
Aside from this, the library is potentially useful wherever one
needs to work with atoms, finite sets, and association lists.
Contact
If you have any questions about the library, feel free to contact Brian Aydemir.