Autosubst

Autosubst is a library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders. 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.

Meta

• Author(s):
  • Steven Schäfer (initial)
  • Tobias Tebbi (initial)
• Rocq-community maintainer(s):
  • Ralf Jung (@RalfJung)
  • Dan Frumin (@co-dan)
• License: MIT License
• Compatible Rocq/Coq versions: 9.0 or later
• Additional dependencies: none
• Rocq/Coq namespace: Autosubst
• Related publication(s):
  • Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions doi:10.1007/978-3-319-22102-1_24

Building and installation instructions

The easiest way to install the latest released version of Autosubst is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-autosubst

To instead build and install manually, do:

git clone https://github.com/coq-community/autosubst.git
cd autosubst
make   # or make -j <number-of-cores-on-your-machine> 
make install

To build the examples that do not need ssreflect, type

make examples-plain

The examples that depend on ssreflect are built with

make examples-ssr

To build the documentation (including all examples), type

make doc

You can use the file doc/toc.html to browse the documentation.

Bug Reports

Please submit bugs reports on https://github.com/coq-community/autosubst/issues