Efficient verification and metaprogramming in Lean
In this talk, we provide a short introduction to the Lean theorem
prover and its metaprogramming framework. We also describe how this
framework extends Lean’s object language with an API to many of Lean’s
internal structures and procedures, and provides ways of reflecting
object-level expressions into the metalanguage. We provide evidence to
show that our implementation is performant, and that it provides a
convenient and flexible way of writing not only small-scale
interactive tactics, but also more substantial kinds of automation.
We view this as important progress towards our overarching goal of
bridging the gap between interactive and automated reasoning. Users
who develop libraries for interactive use can now more easily develop
special-purpose automation to go with them thereby encoding
procedural heuristics and expertise alongside factual knowledge. At
the same time, users who want to use Lean as a back end to assist in
complex verification tasks now have flexible means of adapting Lean’s
libraries and automation to their specific needs. As a result, our
metaprogramming language opens up new opportunities, allowing for more
natural and intuitive forms of interactive reasoning, as well as for
more flexible and reliable forms of automation.
More information about Lean can be found at http://leanprover.github.io.
The interactive book “Theorem Proving in Lean” (https://leanprover.github.io/theorem_proving_in_lean)
is the standard reference for Lean. The book is available in PDF and
HTML formats. In the HTML version, all examples and exercises can be
executed in the reader’s web browser.