Autosubst: Automation for de Bruijn syntax and substitution in Coq

Saarland University Computer Science

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.

Getting Started

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.

Publications

Talks

Coq Workshop 2014
abstract, slides
ITP 2015
slides

Case Studies

Spec LinesProof 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

POPLmark Benchmark Comparison

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.


Webmaster, Fri May 12 12:03:20 2017