This is a MetaCoq reimplementation of the Autosubst 2 code generator by Kathrin Stark. It uses the MetaCoq framework to implement code generation for syntax with binders.
Like Autosubst 2, it supports well-scoped & unscoped syntax as well as variadic syntax and some functors like list and the codomain functor (the product functor is not implemented in the input syntax yet)
The MetaCoq reimplementation is unfortunately missing some features:
- generating lemmas with functional extensionality
- generating lemmas with the “pointwise_relation”
- generating the improved asimpl of Autosubst OCaml (uses the lemmas from the previous point)
- Notations
As such it is unfortunately an incomplete reimplementation. We can not automatically prove substitution equations like Autosubst 2 or Autosubst OCaml. But it still generates inductive types and rewriting lemmas that can be used to manually prove substitution equations.
First, install opam following the directions for your operating system.
It is best practice to create a new opam switch to not cause conflicts with any of your other installed packages. We will also need to add the Coq repository.
opam switch create autosubst-metacoq ocaml-base-compiler.4.09.1
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
The dependencies are coq 8.13 and the corresponding metacoq version.
opam install coq.8.13.1 coq-metacoq.1.0~beta2+8.13
You can compile all Coq sources with
make
Or, if the makefile is not present
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq
To run Autosubst MetaCoq we must first import the Autosubst module, this will also load MetaCoq and the modules for the input syntax. Then there are two commands to run Autosubst:
From ASUB Require Import Autosubst.
MetaCoq Run Autosubst <scope> for <lang>.
MetaCoq Run AutosubstNoInd <scope> for <lang>.
Both commands take a value of type scope_type (Unscoped|Wellscoped) and a language definition of type autosubstLanguage.
scope_type is defined in ./src/Flags.v
autosubstLanguage is defined in ./src/parsers/CustomEntryParser.v
The `AutosubstNoInd` version is for languages that contain functors. At the moment we are not able to generate inductive types that contain functors due to universe constraint errors when unquoting. So for these languages, a user must implement the inductive type beforehand.
Examples of this and other languages can be found in ./test/examples.v
In ./test/examples.v we also prove a substitution equation for the untyped lambda calculus. Because we’re missing both the funext and the pointwise_relation lemmas we have no automation available to solve it. But just as a proof-of-concept we use funext manually to prove rewrite lemmas that asimpl_fext would use, and then prove the goal manually.
You specify the language for which to generate code with our input syntax. The syntax is described in my thesis at https://www.ps.uni-saarland.de/~dapprich/bachelor.php The parsing rules are implemented in ./src/parsers/CustomEntryParser.v
Slight differences to the Autosubst OCaml version of the syntax:
- functors have special names ending in “F”, e.g. codF and listF. Because they are not allowed to be the same name as the actual definitions.
- functors are not contained in quotation marks
- functors don’t have to be declared
The following example is for the call-by-value System F.
Definition fcbv : autosubstLanguage := {| al_sorts := <{ ty : Type; tm : Type; vl : Type }>; al_ctors := {{ arr : ty -> ty -> ty; all : (bind ty in ty) -> ty; app : tm -> tm -> tm; tapp : tm -> ty -> tm; vt : vl -> tm; lam : ty -> (bind vl in tm) -> vl; tlam : (bind ty in tm) -> vl }} |}.
You can find the code at https://gitlab.com/uds-psl/autosubst-metacoq