README.org

October 26, 2021 ยท View on GitHub

#+TITLE: Autosubst MetaCoq

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.

** Switch 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. #+BEGIN_SRC bash 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 #+END_SRC

** Setup The dependencies are coq 8.13 and the corresponding metacoq version.

#+BEGIN_SRC bash opam install coq.8.13.1 coq-metacoq.1.0~beta2+8.13 #+END_SRC

You can compile all Coq sources with #+BEGIN_SRC bash make #+END_SRC

Or, if the makefile is not present #+BEGIN_SRC bash coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq #+END_SRC

  • Run 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: #+BEGIN_SRC bash From ASUB Require Import Autosubst.

MetaCoq Run Autosubst for . MetaCoq Run AutosubstNoInd for . #+END_SRC 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.

** Signatures 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. #+begin_src 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 }} |}. #+end_src