Advisor: Kathrin Stark
We study syntactic theories with variable binders in the Lean Theorem Prover. In a general-purpose interactive prover such as Lean, formalizing binders and substitution is technical and highly repetitive.
Autosubst is an existing automation tool that reduces boilerplate around binders in the Coq proof assistant. It relies on the use of parallel de Bruijn substitutions and their equational theory, the Sigma-calculus. Autosubst derives the substitution operations of an extension of the Sigma-calculus for custom language specifications in second-order abstract syntax. It implements a decision procedure for equations with substitution applications.
Our goal is to adapt Autosubst to Lean to simplify normalization proofs in Lean.
We implement the key features of Autosubst in Lean: the ability to derive generalized substitution lemmas as well as automation tactics for equational reasoning. In the process, we take a closer look at Lean's metaprogramming capabilities and we study how its extensions can be used to optimize the decision procedure in terms of proof term size and efficiency. As an application of the Autosubst adaptation, we formalize proofs of weak and strong normalization of the simply typed Lambda-calculus in Lean.