Metatheory Library

Our library for aiding the formalizing programming language metatheory consists primarily of the following three libraries.

• Atom: This library defines a type atom with decidable equality and infinitely many elements. It is always possible to generate an atom fresh for any finite collection of atoms.
• Environment: This library provides operations, lemmas, and tactics for working with environments, association lists whose keys are atoms.
• Metatheory: This is the main library to include (via Coq's Require command) when starting a new development, since it exports the Atom and Environment libraries. This library defines notations which simplify writing common operations, hints which aid in discharging goals about the freshness of atoms, and tactics which simplify proofs. It also provides a template for those who want to use different notations, hints, and tactics when formalizing programming language metatheory.

The metatheory library depends on the following additional libraries which are not specific to programming language metatheory.

• AdditionalTactics: This library provides additional tactics, in particular a variation on remember (from Coq's standard library) and a Case tactic which helps delineate cases in an inductive proof.
• FiniteSets: This library provides an extension of Coq's library for finite sets that includes extensional equality on sets.
• FSetDecide: This library provides a general purpose decision procedure, decideFSet, for solving goals about finite sets. A similar tactic with the same name is defined in the Atom library.
• FSetNotin: This library provides a tactic, notin_solve, for solving some goals involving non-membership in finite sets.
• ListFacts: This library provides assorted facts about lists.
• Negation: This library provides an extension of Coq's Decidable library.