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

  1. 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.
  2. Download the metatheory library distribution (see the link above).
  3. Unpack the zip file.
  4. 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 of theories 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.
  5. 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.
  6. Note that the distribution includes a README.txt file, and a doc 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 than fsetdec. However, it seems to behave more predictably when used as a hint for Coq's auto and eauto 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 and solve_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.