Adrian Dapprich: Bachelor's Thesis
Generating Infrastructural Code for Terms with Binders using MetaCoq
Advisor: Andrej Dudenhefner
Summary
When formalizing languages with binders (think lambda abstractions or logical quantifiers) one often needs to reason about substituting values for the bound variables. In contrast to paper proofs where "obvious" rules about substitutions can be informally used, when one mechanizes such a language in Coq one often needs to write some amount of theoretically uninteresting but necessary infrastructure lemmas about substitution.
The Autosubst project of Kathrin Stark is a solution to this problem by automatically generating for a given input language the inductive types for the language, definitions of the substitution operation and infrastructure lemmas about substitutions.
This bachelor thesis is then concerned with two things: First, building a reimplementation of Autosubst in the OCaml language (the implementation language of Coq) in order to reuse code from the Coq code base and second, reimplementing Autosubst again in MetaCoq, a library enabling metaprogramming inside Coq. We will then also evaluate the usability and performance of the two approaches in case studies.
A partial Autosubst implementation in OCaml already existed from the author's ACP project. The MetaCoq implementation will be implemented from scratch.
Goals
- An Autosubst implementation in OCaml (without modular syntax & dot graph printing)
A memo detailing how to construct and pretty print the necessary Coq terms can be found here
Milestones
- ✅ Basic implementation that generates all necessary lemmas (Completed during ACP 2020)
- ✅ Generation of tactics
- ⌛ Full documentation
- ⌛ Publish on opam
- An Autosubst implementation in MetaCoq (without modular syntax & dot graph printing)
Milestones
- ✅ Parsing of language specification in Gallina.
- ✅ Basic implementation that generates all necessary lemmas.
- ✅ Additional features like variadic/functor/scoped syntax.
- ⌛ Generation of tactics.
- ⌛ Full documentation.
- 🚫 Publish on opam
For extensions we first target Autosubst OCaml because it is easier to program in and the current implementation of Autosubst MetaCoq is already slow.
- A rewriting tactic that does not rely on the functional extensionality axiom.
A memo detailing different approaches how we can remove the dependency on the funext axiom can be found here
An implementation of asimpl using setoid rewriting is implemented in Autosubst OCaml, it requires generation of new lemmas and morphisms. And if the user writes inductive types containing terms as indices and wants to use asimpl to simplify these terms, they will have to write morphisms that establish the extensionality of the inductive types.
An implementation of asimpl using extensionality lemmas and heuristics is left as future work that could improve performance.
Milestones
- ✅ Proper instances to use setoid rewriting for stlc.
- ✅ Implement asimpl using setoid rewriting for stlc.
- ✅ Generate the additional lemmas for setoid rewriting and Proper instances with Autosubst.
- ✅ Adapt Stark's POPLMark case study to use our new asimpl tactic.
- 🚫 A more performant version of asimpl without the functional extensionality axiom.
- Generate other common infrastructure lemmas (for evaluating predicates on all free variables)
- ✅ Define which lemmas exactly are needed.
- ✅ Generate a few of them in Autosubst OCaml.
- 🚫 Determine what the proof terms of all lemmas look like to generate them.
- Case studies & Benchmarks that use Autosubst OCaml.
Maybe Goals
- 🚫 Autosubst hosted on a website.
- Traced Syntax
- ✅ Implement for an example language (untyped lambda calculus).
- 🚫 Generate using Autosubst.
- Fast asimpl tactic using extensionality lemma and heuristics.
- 🚫 Implement asimpl just using an extensionality lemma and heuristics instead of setoid rewriting.
- 🚫 Generate the additional rewriting lemmas with Autosubst.
- 🚫 Readability & manual extensibility of proof terms.
Resources
References
- Kathrin Stark's doctoral thesis
- Abadi, Martin, et al. "Explicit substitutions." Journal of functional programming 1.4 (1991): 375-416.
- Schäfer, Steven, Tobias Tebbi, and Gert Smolka. "Autosubst: Reasoning with de Bruijn terms and parallel substitutions." International Conference on Interactive Theorem Proving. Springer, Cham, 2015.
- Schäfer, Steven, Gert Smolka, and Tobias Tebbi. "Completeness and decidability of de Bruijn substitution algebra in Coq." Proceedings of the 2015 Conference on Certified Programs and Proofs. 2015.
Legal notice, Privacy policy
