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.

- Download

The project is on Github. Please submit bug reports there.

- Completeness and Decidability of de Bruijn Substitution Algebra in Coq
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions

- Coq Workshop 2014
- abstract, slides
- ITP 2015
- slides

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.

- Leroy
- A self-contained solution using the locally nameless representation. Some tactics and lemmas about lists and numbers are in a library file.
- Charguéraud
- A solution using the library LN for locally nameless termsand the general purpose non-constructive library TLC.
- Vouillon
- A fully self-contained solution using de Bruijn terms.
- GMeta
- GMeta is a library and tool to work with a generic term type and isomorphisms between it and custom term types. It offers a locally nameless and a de Bruijn front-end.

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.