Formalizing syntactic theories with variable binders is not easy. We present Autosubst, a library for the Coq proof assistant to automate this process. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions. Our core contribution is an automation tactic that solves equations involving terms and substitutions. This makes the usage of substitution lemmas unnecessary. The tactic is based on our current work on a decision procedure for the equational theory of an extension of the sigma-calculus by Abadi et. al. The library is completely written in Coq and uses Ltac to synthesize the substitution operation.
Read the Tutorial or the Manual to get started. You can also browse the source code.
The project is on Github. Please submit bug reports there.
| Spec Lines | Proof Lines | |
|---|---|---|
|
POPLmark 1A+2A: Preservation and Progress of System F with Subtyping | 210 | 225 |
| Same proof with Ssreflect and without well-formedness assumptions | 185 | 146 |
| Normalization for CBV System F | 99 | 54 |
| Strong Normalization for System F | 153 | 96 |
| Preservation for a predicative Calculus of Construction | 214 | 229 |
The POPLmark is a benchmark to "measur[e] progress [...] in mechanizing the metatheory of programming languages". We have implemented part A of the challange problem, the preservation and progress of System F with subtyping, to compare Autosubst to manual implementations and other libraries. The following are all Coq implementations of part 1A and 2A we know of.
The unique features of our solution are the use of parallel substitutions, which allows more general lemma statements, and our automation tactics, which simplify Coq expressions containing substitutions to a normal form.
The following chart compares the lines of sourcecode of the different solutions as determined by coqwc as distributed with Coq 8.5. We did not count parts that the authors marked as library. The specification part of LNGen does not include the definitions of terms, typing and reduction, which are written in the Ott specification language.