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

Like most proof assistants, Lean can be extended with custom tactics and other
functionality. Programming Lean itself 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. Monads are used to provide access to the proof
assistant's state and handle tactic failures.

Abstract syntax trees, presented as inductive types, \emph{reflect}
internal data structures. In a metaprogram, Lean terms are viewed as an
inductive type with ten constructors, but internally they are stored in a C++
data structure. The proof assistant's C++ internals are exposed through Lean
interfaces, which we can use for accessing the current goal, unifying terms,
querying and modifying the global context, and setting attributes (e.g.,
\li{@[simp]}).

Here are some example applications of metaprogramming:

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

\item heuristic proof search (e.g., applying unsafe introduction rules with
  backtracking);

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

\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}
%
%But there is also trouble in Eden.%
%\footnote{https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/}
%
As mathematician and Lean user Kevin Buzzard wrote:%
\footnote{\url{https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/}}
%
\begin{quote}
%Note that
If you find yourself ``grinding'' (to use a computer game phrase),
doing the same sort of stuff over and over again because you need to do it to
make progress, then you can try to persuade a computer scientist to write a
tactic to do it for you (or even write your own tactic if you're brave enough
to write \li{meta} Lean code).
\end{quote}

This chapter is inspired by an article by Ebner et al.\ \cite{ebner-et-al-2017}
and by Chapter~8 of \emph{Programming in Lean} \cite{programming-in-lean}.

\section{Tactics and Tactic Combinators}
\label{sec:tactics-and-tactic-combinators}

When programming our own tactics, we often need to repeat some actions on
several goals, or to recover if a tactic fails. Tactic combinators help in such
case. The most important one is \li|repeat {| \ttvar{tactic} \li|}|. It invokes
the tactic specified within curly braces repeatedly on all goals, emerging
subgoals, emerging subsubgoals, and so on, until the tactic is no longer
applicable. Here is an example of \li{repeat} in action:

\lstinputlisting[linerange=repeat_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
After the first \li{repeat}, the proof state consists of four goals:
%
\begin{align*}
  & \text{\lic|\⊢ even 4|}
& & \text{\lic|\⊢ even 7|}
& & \text{\lic|\⊢ even 3|}
& & \text{\lic|\⊢ even 0|}
\end{align*}
%
There are no more conjunctions in sight. The second \li{repeat}, which applies
the lemma \li{even.add_two : ∀k, even k → even (k + 2)} over and over, leaves
us with these goals:
%
\begin{align*}
  & \text{\lic|\⊢ even 0|}
& & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 0|}
\end{align*}

The first and last goals are annoying because they correspond to the lemma
\li{even.}\allowbreak\li{zero}. We can prove them by trying to apply
\li{even.zero} whenever applying \li{even.add_two} fails. This is achieved as
follows:
%
\lstinputlisting[linerange=repeat_orelse_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The tactic combinator \li$<|>$ first executes its left-hand side. If this
fails, the right-hand side is executed instead. If the right-hand side also
fails, the entire combinator fails. With the new tactic, we have two unprovable
goals left:
%
\begin{align*}
  & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 1|}
\end{align*}

The \li{repeat} combinator is very aggressive, targeting all goals and subgoals
recursively. A less ambitious variant is \li{iterate}. It works repeatedly on
the first goal until it fails; then it stops. Consider this example:
%
\lstinputlisting[linerange=iterate_orelse_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
After three applications of \li{even.add_two} or \li{even.zero}, the first goal
cedes its place to the second goal. The \li{iterate} combinator keeps
on working on this goal, until it gets stuck:
%
\begin{align*}
  & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 3|}
& & \text{\lic|\⊢ even 0|}
\end{align*}
%
The last two goals are never considered.

Next, \li{all_goals} invokes a tactic exactly once on each
goal. The combinator succeeds only if the inner tactic succeeds on \emph{all}
goals. It fails in the example below, because \hbox{\li{even.add_two}} cannot be
applied to the goal \li{⊢ even 0}:
%
\lstinputlisting[linerange=all_goals_example-q]{../lean/love07_metaprogramming_demo_master.lean}
\joinlistings
\lstinputlisting[linerange=all_goals_example_wrong-q]{../lean/love07_metaprogramming_demo_master.lean}
%
To ignore failures of the inner tactic, we can wrap it in the \li{try}
combinator:
%
\lstinputlisting[linerange=all_goals_try_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The resulting state is
%
\begin{align*}
  & \text{\lic|\⊢ even 2|}
& & \text{\lic|\⊢ even 5|}
& & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 0|}
\end{align*}
%
The construct \li|try { |\ttvar{tactic}\li| }| is equivalent to
\ttvar{tactic}\li$ <|> skip$, where \li{skip} is a tactic that succeeds without
doing anything. A related tactic is \li{done}; it succeeds if there are no goals
left and fails otherwise.

Another variant is the \li{any_goals} combinator. Like \hbox{\li{all_goals},} it
invokes a tactic once one each goal. But unlike \li{all_goals}, it succeeds if
the inner tactic succeeds on \emph{any} goal. The example
%
\lstinputlisting[linerange=any_goals_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
results in the state
%
\begin{align*}
  & \text{\lic|\⊢ even 2|}
& & \text{\lic|\⊢ even 5|}
& & \text{\lic|\⊢ even 1|}
& & \text{\lic|\⊢ even 0|}
\end{align*}
%
This is the same state as in the previous example. The difference is that
\li{any_goals} can fail whereas \li$all_goals { try { … } }$ always succeeds.

Sometimes we want to leave a goal alone unless we can fully prove it. The
\li{solve1} combinator takes an arbitrary tactic as argument and transforms it
into an all-or-nothing tactic (also called a terminal or end-game tactic).
If the inner tactic does not prove the goal, the combinator fails. In the
example
%
\lstinputlisting[linerange=any_goals_solve1_repeat_orelse_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
the first and fourth goals are proved, and we are left with the two unprovable
goals, exactly as they stand in the lemma statement:
%
\begin{align*}
  & \text{\lic|\⊢ even 7|}
& & \text{\lic|\⊢ even 3|}
\end{align*}

The combinators \li{repeat}, \li{iterate}, \li{all_goals}, and \li{any_goals}
can lead to infinite looping. Consider this example:
%
\lstinputlisting[linerange=repeat_not_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The \li{not.intro} rule is \li{(?a → false) → ¬ ?a}, so it applies once to
transform the goal into \li{⊢ even 1 → false}. Because \li{¬ ?a} is defined as
\li{?a → false}, the rule applies again, yielding the same goal again. The
tactic loops.

So far we have not left the comfort of Lean's interactive interface level. It
is time to start with the actual metaprogramming, by coding a custom
tactic. The tactic embodies the behavior we hardcoded in the \li{solve1}
example above:
%
\lstinputlisting[linerange=intro_and_even-q]{../lean/love07_metaprogramming_demo_master.lean}
%
Let us analyze this code step by step:
%
\begin{itemize}
\item The first line starts with \li{meta def}, indicating the declaration of a
  metafunction. These are much like regular functions declared without
  the \li{meta} keyword, but they do not need to pass the termination check.

\item The first line declares a metafunction called \li{intro_and_even} of type
  \hbox{\li{tactic}} \hbox{\li{unit},} where \li{tactic α} is the type of
  metaprograms returning a value of type \li{α}. (The terms ``tactic'' and
  ``metaprogram'' are often used interchangeably in Lean.) Often, metaprograms
  only have side effects on the state but return no value. In such cases, they
  can return the empty tuple \li{()}, of type \li{unit}.

\item The second line, \li{do}, marks the entry into a monad:\ the
  metaprogramming monad (\li{tactic}).

\item The third line is the low-level, metaprogram equivalent of the familiar
  tactic invocation \li$repeat {$ \li$apply and.intro$ \hbox{\li$}$.} The \li{tactic.repeat}
  metafunction corresponds to \hbox{\li{repeat}.} The \li{tactic.applyc} metafunction
  is one of several that correspond to \li{apply}. It applies a lemma specified
  by its name, of type \li{name}. The name here is \li$``and.intro$. The two
  backticks resolve the name of a Lean constant and create a value of type
  \li{name}.

\item The rest of the metaprogram follows the same principles. Notice
  how the monad operator \li$<|>$ is used to provide the same effect as the
  tactic combinator \li$<|>$. In fact, the metaprogramming monad is an
  alternative monad. Without \li{pure} \li{()} at the end, the metaprogram would
  have \li{all_goal}'s result type as its type, but we want \li{tactic unit}.
\end{itemize}

Tactics and tactic combinators often have the same name at the user interface
level and at the metaprogramming level, except for the \li{tactic.} prefix. A
notable exception is \li{sorry}, which is called \li{tactic.admit}.

Once we have defined a custom tactic, we can invoke it as usual:
%
\lstinputlisting[linerange=any_goals_solve1_repeat_orelse_example₂-q]{../lean/love07_metaprogramming_demo_master.lean}
%
This yields the subgoals
%
\begin{align*}
  & \text{\lic|\⊢ even 7|}
& & \text{\lic|\⊢ even 3|}
\end{align*}

A key benefit of Lean's metaprogramming framework is that we do not need to
learn another programming language to write metaprograms. We can work with the
same constructs and notation used to define ordinary objects in Lean's library.
Everything in that library is available for metaprogramming purposes (e.g.,
\li{ℤ}, \li{list}). 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. All we need is some basic
understanding of monads and some familiarity with Lean's metaprogramming
interfaces.

We conclude this section by introducing a further tactic combinator that can be
useful for metaprogramming. The ``and then'' operator \li{;} can be used to
join two tactics. The left-hand side is executed on the first goal. The
right-hand side is executed on every emerging subgoal (but not on the original
second goal, third goal, etc.). Like \li$<|>$, the \li{;} operator has the same
syntax at the interactive interface level and at the metaprogramming level.
Thus, we can write
%
\begin{lstlisting}
by induction n; simp [*]
\end{lstlisting}
%
instead of
%
\begin{lstlisting}
begin
  induction n,
  { simp },
  { simp [n_ih] }
end
\end{lstlisting}

\section{The Metaprogramming Monad}
\label{sec:the-metaprogramming-monad}

The metaprogramming monad, \li{tactic}, combines the attributes of several
kinds of monads:
%
\begin{itemize}
\item \li{tactic} is a state monad providing access among others to the list of goals,
  the global context (including all definitions and inductive types),
  notations, and attributes (e.g., the list of \li{@[simp]} lemmas).

\item \li{tactic} behaves like an option monad. The program
  \li{tactic.}\allowbreak\li{fail} \ttvar{string}, where \ttvar{string} is an
  error message, leaves the monad in an error state.

\item \li{tactic} is an alternative monad. Namely, it provides an operator
  \li{<|>} for specifying alternatives.

\item \li{tactic} supports tracing. We can use \li{tactic.trace}
  \ttvar{string}, or display the current proof state using
  \li{tactic.}\allowbreak\hbox{\li{trace_state}.}
\end{itemize}

In addition, metaprograms have access to the current goals. Each goal is
represented as a metavariable \li{?m} standing for a missing proof term. Each
metavariable has a type and a local context specifying the variables and
hypotheses that can be used to instantiate \li{?m}. By the PAT principle,
variables and hypotheses are not distinguished. Metaprograms have access to
Lean's functions for inferring implicit arguments and types.

Let us put the metaprogramming monad to some use:

\lstinputlisting[linerange=even_14-q]{../lean/love07_metaprogramming_demo_master.lean}
%
This first example is very modest: It uses the monad's tracing facilities to
print the message ``Proving evenness \ldots''\ before invoking the
\li{intro_and_even} tactic we developed above. The \li{do} keyword signals
entry into the monad. The \li{by} keyword preceding it is necessary to enter
tactic mode, as usual.

As usual in computer science, we can introduce a layer of indirection. We can
package our combination of tracing and proving as its own tactic, and invoking it
to prove that 16 is even:

\lstinputlisting[linerange=hello_then_intro_and_even-q]{../lean/love07_metaprogramming_demo_master.lean}
%
Notice, again, the presence of the \li{meta} keyword in front of the function
definition. Any executable 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
metadefinition. These need not terminate but cannot be used in non-\li{meta}
contexts, because they might be logically inconsistent. Metaprograms can also
call other metaprograms, some of which are implemented in C++.

Most metaprograms are designed to work on a proof state, as a tactic, but some
can also be used on the top level, without a proof context, by invoking the
\li{run_cmd} command:

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

To adapt to the situation in which they are invoked, tactics must be able to
inspect the current goal. The following example outputs the local context, the
target, and all goals (both the metavariables and their types):

\lstinputlisting[linerange=local_context_etc-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The output, which is visible by hovering over the \li{do} keyword, is as follows:
%
\begin{lstlisting}[language=]
local context:
[α, a]
target:
even 18
all missing proofs:
[?m_1, ?m_1]
[even 18, even 20]
\end{lstlisting}
%
The goals are a list of metavariables that must be instantiated. They are
normally not displayed in the proof state; instead, only their types are shown.
In the example, the goals are \li{?m_1 :} \hbox{\li{even 18}} and
\li{?m_1 : even 20}. Confusingly, Lean reuses the same metavariable names for
different goals.

The metafunctions in the above programs have the following types:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|tactic.trace| & \lic| : α → tactic unit| \\
\lic|tactic.local_context| & \lic| : tactic (list expr)| \\
\lic|tactic.target| & \lic| : tactic expr| \\
\lic|tactic.get_goals| & \lic| : tactic (list expr)| \\
\lic|tactic.infer_type| & \lic| : expr → tactic expr| \\
\end{tabular}
\end{center}
%
where \li{expr} stores a term and \li{α} is restricted by a type class (not
shown) to be printable. In addition, \li{list.mmap}
(Section~\ref{sec:a-generic-algorithm-iteration-over-a-list}) is typed as
follows:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|list.mmap {α β : Type}| & \lic| : (α → m β) → list α → m (list β)| \\
\end{tabular}
\end{center}

In practice, instead of the ad hoc \li{trace_goals} tactic, we would normally
use the following predefined tactic:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|tactic.trace_state| & \lic| : tactic unit| \\
\end{tabular}
\end{center}

The next example is more realistic. It implements a \hbox{\li{hypothesis}} tactic
that, like the predefined \li{assumption}, looks for a hypothesis of the
right type (i.e., the right proposition) and applies it to prove the goal:

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

The main metafunction extracts all available hypotheses in the local context,
which are stored as expressions of type \hbox{\li{expr},} and iterates through them.
For each hypothesis, we first try to invoke the predefined \li{exact} tactic. 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{tactic.fail}.

A simple invocation follows:

\lstinputlisting[linerange=hypothesis_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The tracing informs us that \li{α}, \li{p}, \li{a}, and \li{h} were tried in
turn before the matching \li{h} was found and successfully applied.

The example featured the metafunction
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|tactic.fail {α β : Type}| & \lic| : α → tactic β| \\
\end{tabular}
\end{center}
%
where \li{α} must support printing.

\section{Names, Expressions, Declarations, and Environments}
\label{sec:names-expressions-declarations-and-environments}

The metaprogramming framework revolves around five main types:
%
\begin{itemize}
\item \li{tactic} manages the proof state, the global context, and more;

\item \li{name} represents a structured name (e.g., \li{x}, \li{even.add_two});

\item \li{expr} represents an expression---i.e., a term, type, proof, or
  proposition---as an abstract syntax tree;

\item \li{declaration} represents a constant declaration, a definition, an
  axiom, or a lemma;

\item \li{environment} stores all the declarations and notations that make up
  the global context.
\end{itemize}

The type \li{expr} is presented as follows to metaprograms:

% simplified by removing (elaborated : bool := tt)
\begin{lstlisting}
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{lstlisting}
%
In turn:

\begin{sloppypar}
\begin{itemize}
\item \li{expr.var} represents a bound variable, using a notation known
  as De Bruijn indices. For example, \li{expr.var 0} refers to the variable
  bound by the closest \li{λ}- or \li{∀}-binder, \li{expr.var 1} refers to the
  variable bound by the second closest binder, and so on.

\item \li{expr.sort} is used to represent the types of types. For example,
  \hbox{\li{expr.sort}} \hbox{\li{level.zero}} represents \li{Prop}, and
  \li{expr.sort (level.succ level.zero)} represents \li{Type}.

\item \li{expr.const} represents a constant, such as \li{list.reverse} or \li{ℕ}.
  The second argument represents universe levels, a concept that will be
  explained in Chapter~\ref{chap:logical-foundations-of-mathematics}.

\item \li{expr.mvar} represents a metavariable, i.e., a variable \li{?m} with a
  question mark. The first \li{name} argument is a unique name for the
  metavariable, the second \li{name} is a ``pretty'' name, and the \li{expr}
  either stores the metavariable's type or is a dummy value.

\item \li{expr.local_const} represents a variable in the local context (e.g., \li{x},
  \li{h}). The first \li{name} argument is a unique name for the variable; the
  second \li{name} is a ``pretty'' name; the \li{binder_info} stores whether
  the variable is an explicit \li{( )}, implicit \li${ }$, or type class
  \li{[ ]} argument; and the \li{expr} either stores the variable's type or is a
  dummy value.

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

\item \li{expr.lam} represents a $\lambda$-expression. The \li{name} is the
  bound variable's name, the \li{binder_info} is as for \li{expr.local_const},
  the first \li{expr} is the bound variable's type, and the second \li{expr} is
  the $\lambda$-expression's body.

\item \li{expr.pi} represents a $\forall$-quantifier, including the degenerate
  case where the bound variable does not occur in the body (\li{→}). The
  arguments are as for \li{expr.lam}.

\item \li{expr.elet} represents a \li{let} expression. The \li{name} is
  the name of the definition variable, the first \li{expr} is its type, the
  second \li{expr} is the right-hand side of the definition, and the third
  \li{expr} is the \li{let} expression's body.

\item \li{expr.macro} is a low-level mechanism used to implement \li{sorry},
  nameless placeholders (\li{_}), and recursive metaprograms.
\end{itemize}
\end{sloppypar}

To each constructor corresponds a discriminator of type \hbox{\li{expr →}}
\hbox{\li{bool}.} For example, \li{expr.is_pi e} returns \li{tt} if \li{e} is
of the form \li{expr.pi …}\,; otherwise, it returns \li{ff}. The names are easy
to guess, except for \li{expr.is_constant},
\li{expr.}\allowbreak\hbox{\li{is_local_constant},}
\hbox{\li{expr.}}\allowbreak\hbox{\li{is_lambda},} and \li{expr.is_let}.

A lightweight way to construct an expression uses Lean's quoting mechanism,
based on backticks. Expressions are enclosed in parentheses \li{( )} and
preceded by one, two, or three backticks (\li{`}).

An expression preceded by a single backtick---%
\verb|`(|\ttvar{expr}\verb|)|%
---must be fully elaborated. In other words, it may not contain placeholders,
as in the second example:

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

With two backticks---%
\verb|``(|\ttvar{expr}\verb|)|%
---we have \emph{pre-expressions}. These are Lean expressions
that may contain some placeholders to be filled in later:

\lstinputlisting[linerange=two_backticks_expr-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The type \li{pexpr} is a variant of \li{expr}. A \li{pexpr} can be elaborated
into an expression using \lic|tactic.to_expr|, which has type
\li{pexpr → tactic expr}.

With three backticks---%
\verb|```(|\ttvar{expr}\verb|)|%
---we have pre-expressions without any name checking. We can refer to
\li{seattle.washington} even if it does not exist 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}
\joinlistings
\lstinputlisting[linerange=backtick_names_wrong-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The single-backtick variant---%
\verb|`|\ttvar{name}%
---does not check whether the name exists. The two-backtick variant---%
\verb|``|\ttvar{name}%
---fully elaborates the name of a constant and returns an error if no constant
of that name exists in the current global context.
Whether the check and elaboration is desirable depends on the situation. In the
demonstration file associated with this chapter, \li$`intro_and_even$ returns
the name \li{intro_and_even} (of the metafunction we defined in
Section~\ref{sec:tactics-and-tactic-combinators}), whereas
\hbox{\li$``intro_and_even$} expands to the fully elaborated name
\hbox{\li{LoVe.intro_and_even},} including the namespace \li{LoVe}. Tactics such
as \li{tactic.applyc} expect a fully elaborated name. This is why we
wrote \li$tactic.applyc ``and.intro$ earlier. A name can be turned into a
string using the polymorphic \li{to_string} operation.

Sometimes we would like to embed an existing expression in a larger expression.
This can be achieved using \emph{antiquotations}. These are announced by the
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}
%
The three commands print \li{2 + 1}, \hbox{\li$list.map (as_is$ \li$(id.{1} nat))$,}
and \hbox{\li$a 6._.13$} \hbox{\li$(as_is (id.{1} nat))$}---cryptic but precise.

Antiquotations can also be used to perform pattern matching:

\lstinputlisting[linerange=antiquotation_patterns_example-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The two \li{←} lines, corresponding to 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{c} to \li{1}, \li{2}, \li{3}, respectively. The second pattern looks at
\hbox{\li{1 +}} \hbox{\li{2 = 3}} through different lenses---namely, without syntactic sugar,
as an expression of the form \li{@eq α l r}. This also succeeds, binding \li{α},
\li{l}, \li{r} to \li{ℕ}, \li{1 + 2}, and \li{3}, respectively.

Declarations are presented as an inductive type to metaprogrammers:

\begin{lstlisting}
meta inductive declaration
| defn : name → list name → expr → expr →
  reducibility_hints → bool → declaration
| thm  : name → list name → expr → task expr → declaration
| cnst : name → list name → expr → bool → declaration
| ax   : name → list name → expr → declaration
\end{lstlisting}
%
For example, in a declaration of the form \li{declaration.defn nam _ τ rhs _ _},
\li{nam} is the name of the defined constant, \li{τ} is its type, and \li{rhs}
is the definition's body. Given a declaration,
\li{declaration.}\allowbreak\li{to_name} extracts its first component, of type
\li{name}.

The environment is presented as an abstract type, equipped with some
operations to query and modify it. The most useful metafunction is
%
\begin{center}
\begin{tabular}{@{}l@{}}
\lic|environment.fold {α : Type} :| \\
\quad \lic|environment → α → (declaration → α → α) → α| \\
\end{tabular}
\end{center}
%
A call to \li{environment.fold env x f} applies the given function \li{f} on
each declaration in the global context in turn. In addition, an accumulator
value is threaded through. Its initial value is \li{x} and the final value is
returned at the end. For example, the following command outputs the number of
global declarations:

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

Fold functions are a common idiom in functional programming. If you
are not familiar with them, we recommend the chapter ``Higher Order
Functions'' of \emph{Learn You a Haskell for Great Good!} \cite{lipovaca-2011}.
You can start from the heading ``Only folds and horses.''

\section{First Example: A Conjunction-Destructing Tactic}
\label{sec:first-example-a-conjunction-destructing-tactic}

In this and the next section, we review two metaprograms that accomplish
well-defined tasks. The first program 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}
%
In each case, we would like to simply write \li{destruct_and h}.

Our tactic relies on a helper metafunction, which takes as argument the
hypothesis \li{h} to use as an expression rather than as a name:

\lstinputlisting[linerange=destruct_and_helper-q]{../lean/love07_metaprogramming_demo_master.lean}
%
We first extract \li{h}'s type (i.e., its proposition). We perform pattern
matching with antiquotations to see if the type is of the form \hbox{\li{a ∧ b}.}
If so, we try three things in turn. First, we invoke \hbox{\li{exact h}.} If
this fails, we apply the left elimination rule on \li{h}, producing the proof
term \li{and.elim_left h} \li{:} \li{a}, and continue recursively with that
proof term. The \li{tactic.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 metafunction has very little to do:

\lstinputlisting[linerange=destruct_and_main-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The metafunction retrieves the hypothesis \li{h} with the specified name
\li{nam} using \li{tactic.get_local}, which has type \li{name →}
\hbox{\li{tactic}} \hbox{\li{expr},} and calls the helper metafunction.

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, unpleasant-to-write code to provide proper parsing for our
tactic's argument.

\section{Second Example: A Provability Advisor}
\label{sec:second-example-a-provability-advisor}

Sometimes we state a lemma, prove it, and later realize that the lemma already
existed. This can be prevented using \hbox{\li{prove_direct},} a tool that
traverses all available lemmas and checks whether one of them can prove the
current goal.

We will review the code of \li{prove_direct} in steps. The first step is a
metafunction \li{is_theorem} that returns \li{tt} if a declaration is a lemma
or an axiom and \li{ff} otherwise:

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

The next metafunction returns the list of all theorem names:

\lstinputlisting[linerange=get_all_theorems-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The \li{tactic.get_env} metafunction yields an \li{environment} object
giving the global context. We can traverse it using
\li{environment.}\allowbreak\li{fold}, which is applied on each declaration
\li{decl} in turn and on an accumulator \li{nams}. We extend the accumulator
with each declaration's name that satisfies \li{is_theorem}. At the end,
\li{environment.}\allowbreak\li{fold} returns the accumulator.

Another component we need is a tactic that attempts to prove the goal using a
theorem specified by its name:

\lstinputlisting[linerange=prove_with_name-q]{../lean/love07_metaprogramming_demo_master.lean}
%
The \li{tactic.applyc} applies the theorem named \li{nam} to the current goal.
For performance, we pass an optional configuration,
\hbox{\li|{ md := transparency.reducible,|} \hbox{\li|unify := ff }|,}
which instructs \li{tactic.}\allowbreak\li{applyc} to perform less computational
expansion. This is important since this tactic will be invoked thousands of
times.
%
The \li{tactic.all_goals} combinator, in conjunction with
\hbox{\li{tactic.}}\allowbreak\hbox{\li{assumption},} is used to
apply the hypotheses from the local context to all remaining subgoals.

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

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

As a small refinement of the above, we propose a version of \li{prove_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=prove_direct_symm-q]{../lean/love07_metaprogramming_demo_master.lean}
%
Our solution is simple: We first try \li{prove_direct}, and if that fails, we
apply symmetry of equality (the property \li{?l = ?r → ?r = ?l}) to change the
goal and try \li{prove_direct} again.

This concludes our review of \li{prove_direct}. A similar, more sophisticated
tactic is available as \li{library_search} in \li{mathlib}.

\section{A Look at Two Predefined Tactics}
\label{sec:a-look-at-some-predefined-tactics}

Quite a few of Lean's predefined tactics are implemented as metaprograms and
not in C++. We can find these definitions by clicking the name of a construct
in Visual Studio Code while holding the control or command key. To familiarize
ourselves further with the metaprogramming framework, we conclude this chapter
by looking at the implementation of two basic tactics that were introduced
in Chapter~\ref{chap:backward-proofs}:\ \li{intro} and \li{assumption}.

We can find \li{intro}'s code by entering \li{#check tactic.intro} and by
clicking \li{tactic.intro} while holding control or command:

\begin{lstlisting}
meta def intro (n : name) : tactic expr :=
do
  t ← target,
  if expr.is_pi t ∨ expr.is_let t then
    intro_core n
  else
    whnf_target >> intro_core n
\end{lstlisting}
%
The definition is located inside the \li{tactic} namespace, explaining
why \li{tactic.}\allowbreak\li{intro} and \li{tactic.target} are simply called
\li{intro} and \li{target}. If the goal's target is a \li{∀}-quantifier or a \li{let}
expression, \li{tactic.intro_core} is invoked. Otherwise, a tactic named
\li{tactic.whnf_target} is invoked before \li{tactic.intro_core}, in the hope
that a \li{∀} or \li{let} will emerge. The \li{>>} operator performs sequential
composition in a monad; \li{ma >> mb} is syntactic sugar for \li{do ma, mb}.

If we follow the definition of \li{tactic.intro_core}, we reach a dead end:
%
\begin{lstlisting}
meta constant intro_core : name → tactic expr
\end{lstlisting}
%
The metafunction is simply declared as a constant, without a definition. This
indicates that the implementation is in C++. The core of the \li{whnf_target}
tactic, which normalizes the goal by expanding definitions,
\li{β}-reducing, and more, is also implemented in C++, for efficiency reasons.

In Section~\ref{sec:the-metaprogramming-monad}, we implemented a
\li{hypothesis} tactic that mimicked \li{assumption}. Let us now have a
look at the real thing:
%
\begin{lstlisting}
meta def assumption : tactic unit :=
do {
  ctx ← local_context,
  t ← target,
  H ← find_same_type t ctx,
  exact H }
<|> fail "assumption tactic failed"
\end{lstlisting}
%
Again, the definition is in the \li{tactic} namespace. The
\hbox{\li{assumption}} tactic attempts to find a hypothesis \li{H} (of type \hbox{\li{expr})}
among the variables declared in the local context \li{ctx} that has a type
unifiable with that of the target \li{t} (i.e., a hypothesis whose statement is
unifiable with \li{t}). Then \li{H} is applied to the target using
\li{tactic.}\allowbreak\li{exact}. If anything goes wrong, the \li{assumption}
tactic catches the error and reports ``assumption tactic failed.''

The auxiliary metafunction \li{find_same_type} is defined as follows:
%
\begin{lstlisting}
meta def find_same_type : expr → list expr → tactic expr
| e []        := failed
| e (H :: Hs) :=
  do
    t ← infer_type H,
    (unify e t >> return H)
    <|> find_same_type e Hs
\end{lstlisting}
%
The metafunction takes an expression \li{e} representing a type (i.e., a
proposition) and a context and returns an expression. If the context is empty,
an anonymous error is raised. Otherwise, we check if the local context's
first hypothesis \li{H}'s type \li{t} is unifiable with \li{e}. If so, \li{H}
is returned; otherwise, we continue with the remaining hypotheses \li{Hs}. The
\li{return} operation is an alias for \hbox{\li{pure}.}

The \li{find_same_type} metafunction relies on two general\hyp{}purpose
metafunctions we had not encountered before:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|tactic.failed {α : Type}| & \lic| : tactic α| \\
\lic|tactic.unify| & \lic| : expr → expr → tactic unit| \\
\end{tabular}
\end{center}

\section{Miscellaneous Tactics}
\label{sec:miscellaneous-tactics-metaprogramming}

\subsection*{skip}

The \li{skip} tactic succeeds without doing anything. It is sometimes useful
when writing custom tactics.

\subsection*{done}

The \li{done} tactic raises a failure if there are some goals left; otherwise,
it succeeds without doing anything. It is sometimes useful as a building block
when writing custom tactics.

\subsection*{library\_search}

The \li{library_search} tactic searches the loaded libraries for a lemma that
exactly proves the goal. On success, it suggests a tactic invocation of the form
\li{exact …}\,, which can be inserted in the formalization.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Command}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|run_cmd| & executes a metaprogram on the top level, without a \hbox{proof context} \\
\end{xltabular}

\subsection*{Declaration}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|meta| & prefixes declarations of metaprograms \\
\end{xltabular}

\subsection*{Quotations}

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

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|done| & fails if there are some goals left \\
\lic|library_search| & searches the libraries for a lemma that proves the \hbox{current goal} \\
\lic|skip| & does nothing \\
\end{xltabular}

\subsection*{Tactic Combinators}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|;| & invokes the second tactic to all subgoals from the \hbox{first tactic} \\
\lic$<|>$ & tries the left-hand side first; tries the right-hand side on~failure \\
\lic|all_goals| & invokes a tactic once on each goal, expecting \hbox{only successes} \\
\lic|any_goals| & invokes a tactic once on each goal, expecting at least one~success \\
\lic|iterate| & repeatedly invokes a tactic on the first goal \hbox{until~failure} \\
\lic|repeat| & repeatedly invokes a tactic on all goals and subgoals \hbox{until~failure} \\
\lic|solve1| & transforms a tactic into an all-or-nothing tactic \\
\lic|try| & tries to invoke a tactic; does nothing on failure \\
\end{xltabular}

\endgroup
