\chapter{Metaprogramming}
\label{chap:metaprogramming}

Like most proof assistants, Lean can be extended with custom functionality,
notably tactics. This kind of programming---programming the prover---is called
metaprogramming. Lean's metaprogramming framework uses mostly the same notions
and syntax as Lean's input language itself, so that we do not need to learn a
different programming language.

These notes are partly inspired by an article by Gabriel Ebner et al.\
\cite{ebner-et-al-2017} and by Chapter~8 of \emph{Programming in Lean}
\cite{programming-in-lean}. We strongly recommend that you read the chapter.

\section{Overview}

Lean's metaprogramming framework enables us to program the prover in its own
language, using a monadic language. Abstract syntax trees, presented as
inductive types in Lean, \emph{reflect} internal data structures. For example,
the type of expressions---i.e., terms---is viewed as an inductive type with
ten constructors, but internally in Lean it is a C++ data structure. The
prover's C++ internals are exposed through Lean interfaces, which we can use
for accessing the current context and goal, unifying expressions, querying and
modifying the environment, and setting attributes (e.g., \li{@[simp]}).

Most of Lean's predefined tactics are implemented as metaprograms, and not in
C++. We can find these definitions by clicking on the name of a construct in
Visual Studio Code while holding the control or command key.

Here are some example applications of metaprogramming:

\begin{itemize}
\item proof goal transformations (e.g., apply all safe introduction rules for
  connectives, put the goal in negation normal form);

\item heuristic proof search (e.g., apply unsafe introduction rules for
  connectives and hypotheses with backtracking);

\item decision procedures (e.g., for propositional logic, linear arithmetic);

\item definition generators (e.g., Haskell-style \li{derive} for inductive
  types);

\item advisor tools (e.g., lemma finders, counterexample generators);

\item exporters (e.g., documentation generators);

\item ad hoc proof automation (to avoid boilerplate or duplication).
\end{itemize}

A key benefit of Lean's metaprogramming framework is that users, who may not
even be computer scientists, do not need to learn another programming language
to write metaprograms. They can work with the same constructs and notation
used to define ordinary objects in the prover's library. Everything in that
library is available for metaprogramming purposes (e.g., \li{ℤ}, \li{list},
algebraic structures). Metaprograms can be written and debugged in the same
interactive environment, encouraging a style where formal libraries and
supporting automation are developed at the same time.
%But there is also trouble in Eden.%
%\footnote{https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/}

The framework is articulated around three main types:

\begin{itemize}
\item the \li{tactic} monad, which contains the proof state, the
  environment, and more;

\item the \li{name} type for storing structured names (e.g., \li{option.bind});

\item the \li{expr} type representing terms, types, proofs, and propositions
  as abstract syntax trees.
\end{itemize}

\section{The Tactic Monad}

The \li{tactic} monad combines the attributes of several kinds of monads. It
is a state monad providing access among others to the list of goals, the
environment (including all definitions and inductive types), notations, and
attributes (e.g., the list of \li{@[simp]} rules).

Goals are represented as metavariables, standing for the missing proofs. Each
metavariable has a type and a local context giving the constants and
hypotheses. By the Curry--Howard correspondence, constants and hypotheses are
not distinguished. Tactics have access to the elaborator, to elaborate
expressions and compute their types.

The \li{tactic} monad also behaves like an option monad. The program
\li{fail} \texttt{\itshape msg}, where \texttt{\itshape msg} is a text string,
leaves the monad in an error state.

Moreover, the \li{tactic} monad is also an alternative monad. Namely, it
provides an operator \li{<|>} for specifying alternatives. The program
\li{s <|> t} first executes \li{s}; if \li{s} is a failure, then the state is
reverted to its initial condition and \li{t} is executed instead.

Finally, \li{tactic} provides some tracing capabilities. We can use
\li{trace msg}, where \li{msg} is a text string, or we can display the current
proof state using \li{trace_}\allowbreak\li{state}.

Let us put the \li{tactic} monad to some use:

\lstinputlisting[linerange=hello_triv-q]{../lean/love07_metaprogramming_demo_master.lean}
%
This first example is very modest: It uses the monad's tracing facilities to
print the message ``Hello, Metacosmos!'' before applying the \li{triv} tactic,
which can be used to prove trivial goals such as \li{true}. The \li{do}
keyword signals entry into the \li{tactic} monad. The \li{by} keyword is
necessary to enter tactic mode.

As is usually the case in computer science, we can introduce a layer of
indirection. We can package our combination of tracing and proving as its own
tactic, and gloriously apply it to prove \li{true}:

\lstinputlisting[linerange=hello_world-q]{../lean/love07_metaprogramming_demo_master.lean}

The \li{hello_world} tactic's type is \li{tactic unit}. In general, tactics
will have the type \li{tactic σ}, where \li{σ} is the type of some value
returned by the tactic. Often our tactics will only have side effects on the
state but return no value. In such cases, we return the empty tuple, of type
\li{unit}. This is what the \li{triv} tactic returns, and hence this is what
we return.

Also notice the presence of the \li{meta} keyword in front of the function
definition. Any executable (i.e., not defined using the \li{noncomputable}
keyword) Lean definition can be used as a metaprogram. In addition, we can put
\li{meta} in front of a definition to indicate that is a
\emph{metadefinition}; these need not terminate but cannot be used in
non-\li{meta} contexts. Metaprograms (whether defined with \li{meta} or not)
can communicate with Lean through \emph{metaconstants}, which are implemented
in C++ and have no logical meaning---i.e., they are opaque names. Metaprograms
can also call other metaprograms.

Most tactics are designed to work on a proof state, but the Lean concept of a
tactic is more general, and they can be used also on the top level, without a
proof context, by using the \li{run_cmd} command:

\lstinputlisting[linerange=run_cmd_hello_world-q]{../lean/love07_metaprogramming_demo_master.lean}

Tactics usually need to adapt to the situation where they are called. This
means they must inspect the current goal. The following example prints the
local context, the goal conclusions, and the current goal or ``target'':

\lstinputlisting[linerange=local_context_etc-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The output is as follows:
%
\begin{itemize}
\item local context: \li{[α, a]};

\item goals: \li{[?m_1]};

\item target: \li{true}.
\end{itemize}

The goals are a list of variables of certain types that must be instantiated.
They are normally not displayed in the proof state; instead, their types are
shown. In the example, we have \li{?m_1 : true}.

The next example performs something somewhat more useful. It implements a
\li{find_}\allowbreak\li{assumption} tactic that, like the predefined
\li{assumption} tactic, looks for a hypothesis of the right type (i.e., the
right proposition) and applies it to solve the current goal:

\lstinputlisting[linerange=find_assumption-q]{../lean/love07_metaprogramming_demo_master.lean}

The main function extracts all available hypotheses forming the local context,
which are stored as expressions of type \li{expr}, and iterates through them.
For each hypothesis, we first try to apply the predefined \li{exact} tactic
(which exists also as a monadic program, like many other tactics). If this
fails, the \li{<|>} operator passes control to the right branch, in which we
continue recursively with the remaining hypotheses. If no hypotheses are left,
we invoke \li{fail}.

A simple invocation follows:

\lstinputlisting[linerange=find_assumption_example-q]{../lean/love07_metaprogramming_demo_master.lean}

The tracing information informs us that \li{p}, \li{α}, \li{a}, and \li{h}
have been tried in turn until the matching \li{h} was found.

\section{Names and Expressions}

Terms, including proof terms, are represented by an inductive type
\li{expr} of ``expressions'' in the metaprogramming framework:

% simplified by removing   (elaborated : bool := tt)
\begin{verbatim}
meta inductive expr : Type
| var      {} : nat → expr
| sort     {} : level → expr
| const    {} : name → list level → expr
| mvar        : name → name → expr → expr
| local_const : name → name → binder_info → expr → expr
| app         : expr → expr → expr
| lam         : name → binder_info → expr → expr → expr
| pi          : name → binder_info → expr → expr → expr
| elet        : name → expr → expr → expr → expr
| macro       : macro_def → list expr → expr
\end{verbatim}

Briefly:

\begin{itemize}
\item \li{var} represents a bound variable, using a notation known
  as De Bruijn indices.

\item \li{sort} is used to represent the type of types \li{Type}, \li{Type 1},
  etc.

\item \li{const} represents a constant, such as \li{list.reverse} or \li{ℕ}.

\item \li{mvar} represents a metavariable, i.e., a variable with a question
  mark (e.g., \li{?m_1}).

\item \li{local_const} represents a local constant in the proof state
  (e.g., \li{h}).

\item \li{app} represents the application of a function to an argument.

\item \li{lam} represents a $\lambda$ binder.

\item \li{pi} represents a $\Pi$ binder.
\end{itemize}

Fortunately, we can often use higher-level interfaces to manipulate
expressions. A lightweight way to construct an expression is using Lean's
quoting mechanism, based on backticks. Expressions are enclosed in parentheses
and preceded by one, two, or three backticks (\li{`}).

An expression preceded by a single backtick---%
\verb|`(|\texttt{\itshape e}\verb|)|%
---must be fully elaborated. It may not contain holes, as in the second
example below:

\lstinputlisting[linerange=one_backtick_expr-q]{../lean/love07_metaprogramming_demo_master.lean}

With two backticks---%
\verb|``(|\texttt{\itshape e}\verb|)|%
---we have \emph{pre-expressions}. These are Lean expressions
that may contain some holes to be filled in later, based on some context:

\lstinputlisting[linerange=two_backticks_expr-q]{../lean/love07_metaprogramming_demo_master.lean}

With three backticks---%
\verb|```(|\texttt{\itshape e}\verb|)|%
---we have pre-expressions without name checking. We can refer to
\li{some_silly_name} even if it does not exist at the point when the
pre-expression is parsed:

\lstinputlisting[linerange=three_backticks_expr-q]{../lean/love07_metaprogramming_demo_master.lean}

A similar quoting mechanism exists for names. The syntax consists of one or
two backticks, without parentheses:

\lstinputlisting[linerange=backtick_names-q]{../lean/love07_metaprogramming_demo_master.lean}

The single-backtick variant---%
\verb|`|\texttt{\itshape n}%
---does not check whether the name exists; the two-backtick variant---%
\verb|``|\texttt{\itshape n}%
---performs this check. Whether the check is desirable depends on the
situation.


Sometimes we would like to plug in existing expressions into a larger
expression. This can be achieved using \emph{antiquotations}. These are
announced by a prefix \verb|%%| followed by a name from the current context.
Antiquotations are available with one, two, and three backticks:

\lstinputlisting[linerange=antiquotation_examples-q]{../lean/love07_metaprogramming_demo_master.lean}

Antiquotations can also be used to perform pattern matching:

\lstinputlisting[linerange=antiquotation_patterns_example-q]{../lean/love07_metaprogramming_demo_master.lean}

In the example, the two \li{←} lines, corresponding to monadic bind
operations, succeed only if the right-hand side has the right shape (which it
has). Given that \li{target} is \li{1 + 2 = 3}, executing the first line binds
the variables \li{a}, \li{b}, \li{r} to \li{1}, \li{2}, \li{3}, respectively.
The second pattern looks at \li{1 + 2 = 3} through different lenses---namely,
without syntactic sugar, as an expression of the form \li{(@eq α l r)}, for
some \li{α}, \li{l}, \li{r}. This also succeeds.

\section{Example: A Destructive Tactic}

Next, we review two examples of metaprograms that accomplish a well-defined
task. The first example is a tactic called \li{destruct_and} that automates
the elimination of conjunctions in premises. Our aim is to automate proofs
such as the following:

\lstinputlisting[linerange=example_1_2_3-q]{../lean/love07_metaprogramming_demo_master.lean}

We would like in each case to simply write \li{destruct_and h}.

Our tactic relies on a helper function, which takes as argument the hypothesis
\li{h} to use and its type---i.e., its proposition:

\lstinputlisting[linerange=destruct_and_helper-q]{../lean/love07_metaprogramming_demo_master.lean}
%
We perform pattern matching with antiquotations to see if the hypothesis
\li{h} is of the form \li{a ∧ b}. If so, we try three things in turn. First,
we try to invoke the \li{exact} tactic. If this fails, we try the left
elimination rule, producing \li{and.elim_left h} \li{:} \li{a}, and continue
recursively with that. The \li{to_expr} call converts a pre-expression into an
expression, elaborating it. If our attempt at left elimination fails, we try
right elimination instead.

The main function has very little to do:

\lstinputlisting[linerange=destruct_and_main-q]{../lean/love07_metaprogramming_demo_master.lean}
%
It retrieves the hypothesis \li{h} with the specified name \li{nam}, extracts
its type (i.e., its proposition), and calls the helper function.

We can now turn to our motivating examples and prove them again, this time
using our new widget:

\lstinputlisting[linerange=example_4_5_6-q]{../lean/love07_metaprogramming_demo_master.lean}
%
Unfortunately, we need to quote the name of the hypothesis with a backtick. We
would need more (not particularly pleasant to write) code to provide proper
parsing for our tactic's argument.

\section{Example: A Solvability Advisor}

Our second example enriches Lean with functionality that is available in the
Isabelle/HOL proof assistant. It sometimes happens that a user states a lemma,
proves it, and later realizes that the lemma already existed in the library.
To help prevent this, we implement a \li{solve_direct} tactic, which goes
through all lemmas in the database and checks whether one of them can be used
to fully solve the current goal.

We will review the code in steps. The first step is a function \li{is_theorem}
that returns true (\li{tt}) if a declaration is a theorem or an axiom and
false (\li{ff}) otherwise:

\lstinputlisting[linerange=is_theorem-q]{../lean/love07_metaprogramming_demo_master.lean}
%
We will use this function to filter out the declarations that do not interest
us.

The next function returns the list of all theorem (and axiom) names:

\lstinputlisting[linerange=get_all_theorems-q]{../lean/love07_metaprogramming_demo_master.lean}

The \li{get_env} function (in fact, tactic) returns an object representing the
environment. We can traverse it using \li{environment.fold}, which is applied
on each declaration \li{decl} in turn and on an accumulator \li{thms}.
We extend the accumulator with each declaration's name that satisfies the
\li{is_theorem} predicate. At the end, \li{fold} returns the accumulator.

The \li{fold} function is a common idiom in functional programming. If you
are not familiar with the concept, we recommend Chapter~6 of
\emph{Learn You a Haskell for Great Good!}%
\footnote{http://learnyouahaskell.com/higher-order-functions}

Another component we need is a tactic that attempts to (fully) solve the goal
using a theorem called \li{nam}.

\lstinputlisting[linerange=solve-q]{../lean/love07_metaprogramming_demo_master.lean}

\li{mk_const nam} is used to produce an \li{expr} representing the proof from a
name \li{nam} (the theorem name).

The \li{apply} tactic applies an \li{expr} to the current goal. For
performance, we pass an optional configuration,
\verb|{ md := transparency.reducible, unify := ff }|,
which tells \li{apply} to perform less computational unfolding.

The \li{all_goals} tactic, in combination with \li{assumption}, is used to
ensure that the hypothesis from the local context are used to fill in any
remaining subgoals.

Finally, our \li{solve_direct} tactic goes through all theorems found by
\li{get_}\allowbreak \li{all_}\allowbreak \li{theorems} and succeed with the
first theorem that solves the current goal:

\lstinputlisting[linerange=solve_direct-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The \li{list.mfirst} function applies a tactic to each element of a list until
one application succeeds. We use \li{trace} to output the successful theorem
to the user, so that they can apply the theorem directly instead of relying on
\li{solve_direct}.

As a small refinement of the above, we propose a version of \li{solve_direct}
that also looks for equalities stated in symmetric form---for example, if the
goal is \li{l = r} but the theorem is \li{r = l}:

\lstinputlisting[linerange=solve_direct_symm-q]{../lean/love07_metaprogramming_demo_master.lean}
%
Our solution is quite simple: We first try \li{solve_direct}, and if that
fails, we apply symmetry of equality (the property \li{?l = ?r → ?r = ?l})
to change the goal and try \li{solve_direct} again.

\section{Summary of New Syntax}

\small

\subsection{Declaration}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|meta| & prefixes declarations of metaprograms and metaconstants \\
\end{tabularx}

\subsection{Command}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|run_cmd| & executes a tactic on the top level, without a proof context \\
\end{tabularx}

\subsection{Quotations}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\verb|`|\texttt{\itshape n} & quotes literal name, with checking \\
\verb|``|\texttt{\itshape n} & quotes literal name, without checking \\
\verb|`(|\texttt{\itshape e}\verb|)| & quotes fully elaborated expressions without holes \\
\verb|``(|\texttt{\itshape e}\verb|)| & quotes pre-expressions, with name checking \\
\verb|```(|\texttt{\itshape e}\verb|)| & quotes pre-expressions, without name checking \\
\texttt{\char`\%\char`\% \itshape x} & embeds an expression in a quotation \\
\end{tabularx}

\subsection{Tactic Monad Functions}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|all_goals| & applies the given tactic to all goals \\
\li|get_env| & gives access to the list of all declarations in the environment \\
\li|get_goals| & gives the list of all proof holes to fill in \\
\li|get_local| & finds a local constant by name \\
\li|infer_type| & computes the type of an expression \\
\li|local_context| & gives the list of all local constants \\
\li|mk\_const| & builds a constant from a name \\
\li|target| & gives the current goal to prove \\
\li|to_expr| & elaborates a pre-expression \\
\li|trace| & outputs a debug string \\
\li|trace_state| & outputs the current proof state \\
\end{tabularx}
