/autosubst2-1

Official repository of the Autosubst 2 project.

Primary LanguageHaskellOtherNOASSERTION

Autosubst 2

This is the main branch containing the development version of Autosubst 2. We recommend using the main branch in almost every case, since it exceeds the released beta versions in functionality and usability.

Formalizing syntactic theories with variable binders in a general-purpose proof assistant is hard.

With Autosubst 2, we present a tool that:

  1. offers support for unscoped and well-scoped de Bruijn in Coq.
  2. generates first-order renaming, substitutions, and the appropriate substitution lemmas.
  3. offers support for custom syntax: potentially mutually inductive and with several sorts of variables.

Requirements:

  • Haskell Stack build environment
  • active internet connection (stack setup loads and installs a private version of GHC)
  • the generated output is compatible with Coq 8.11.

Installation

stack setup
stack init
stack build
stack exec -- as2-exe <OPTIONS>

You can use stack install, to later on use as2-exe instead of stack exec --as2-exe.

Summary

With no options, Autosubst 2 operates as follows:

  1. reads a HOAS specification from stdin
  2. prints generated well-scoped Coq code to stdout

See the signatures file system for examples of the HOAS specification.

In the standard case, a user probably wants to specify input and output files via the -i and -o option. The following command generates the code for a call-by-value variant of System F and dumps it to sysf_cbv.v.

stack exec -- as2-exe -i specs/sysf_cbv.sig -o sysf_cbv.v

The generated code depends on a small number of header files which define commonly used notations and definitions. These library files are called axioms.v (needed for all output, imports e.g. functional extensionality), fintype.v (only for well-scoped syntax), unscoped.v (for unscoped syntax), and header_extensible.v (for modular syntax) and can be found in the headers directory.

To use the generated code, place the output of the tool, say syntax.v, and the respective header file in your project directory, and import them by adding the following directive to your development (the header is sourced implicitly through the generated code file):

Require Export syntax.

Options

Per default, the tool will not silently overwrite existing files but request for user confirmation. This can be explicitly disabled via the -f option. The maximal line width of the generated Coq code is 140 characters, but this can also be adjusted via the -w option.

It is furthermore possible to choose for which prover code is generated. At the moment, well-scoped Coq code (-p Coq), unscoped Coq code (-p UCoq), and output for only modular syntax (-p ECoq) are available. Not all modes are co modexp.sig mpatible with all syntactic inputs and the tool will output a corresponding error message.

The following command prints an overview of all options:

stack exec -- as2-exe --help

Bugs, Requests, etc.

Please direct any inquiries regarding this software via Github.

Publications