Advisor: Kathrin Stark
We study syntactic theories with variable binders. Formalizing binders and substitution in a general-purpose proof assistant is technical and highly repetitive. The Coq library Autosubst automates the definition of de Bruijn substitution and derives rewriting rules for custom term languges. It implements a decision procedure for equations with substitution applications.
Our goal is to adapt Autosubst to the Lean Theorem Prover. Lean is a recently developed interactive prover with flexible metaprogramming extensions. We implement the key features of Autosubst in Lean, i.e. the ability to derive generalized substitution lemmas as well as automation tactics for equational reasoning. We hope to use Lean's extended metaprogramming capabilities to optimize the decision procedure in terms of proof term size and efficiency.