\section{The \Ivor{} Library}
%Given the basic operations defined in section \ref{holeops}, we can
%create a library of tactics.
The \Ivor{} library allows the incremental, type directed development
of $\source$ terms. In this section, I will introduce the basic
tactics available to the library user, along with the Haskell
interface for constructing and manipulating $\source$ terms. This
section includes only the most basic operations; the API is however
fully documented on the
web\footnote{\url{http://www.cs.st-andrews.ac.uk/~eb/Ivor/doc/}}.
\subsection{Definitions and Context}
The central data type is \hdecl{Context} (representing $\Gamma$ in the
typing rules), which is an abstract type holding information about
inductive types and function definitions as well as the current proof
state. All operations are defined with respect to the context. An
empty context is contructed with \hdecl{emptyContext :: Context}.
Terms may be represented several ways; either as concrete syntax (a
\texttt{String}), an abstract internal representation (\texttt{Term})
or as a Haskell data structure (\texttt{ViewTerm}). A typeclass
\hdecl{IsTerm} is defined, which allows each of these to be converted
into the internal representation. This typeclass has one method:
\begin{verbatim}
class IsTerm a where
check :: Monad m => Context -> a -> m Term
\end{verbatim}
The \texttt{check} method parses and typechecks the given term, as
appropriate, and if successful returns the internal representation.
Constructing a term in this way may fail (e.g. due to a syntax or
type error) so \texttt{check} is generalised over a monad
\hdecl{m} --- it may help to read \hdecl{m} as \hdecl{Maybe}.
In this paper, for the sake of readability we will use the syntax
described in section \ref{corett}, and assume an instance of
\hdecl{IsTerm} for this syntax.
Similarly, there is a typeclass for inductive families,
which may be represented either as concrete syntax or a Haskell data
structure.
\begin{verbatim}
class IsData a where
addData :: Monad m => Context -> a -> m Context
\end{verbatim}
The \hdecl{addData} method adds the constructors and elimination
rules for the data type to the context. Again, we assume an instance
for the syntax presented in section \ref{indfamilies}.
The simplest way to add new function definitions to the context is
with the \hdecl{addDef} function. Such definitions may not be recursive,
other than via the automatically generated elimination rules, ensuring
termination:
\begin{verbatim}
addDef :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
\end{verbatim}
However, \Ivor{} is primarily a library for constructing proofs; the
Curry-Howard correspondence~\cite{curry-feys,howard} identifies
programs and proofs, and therefore such definitions can be viewed as
proofs; to prove a theorem is to add a well-typed definition to the
context. We would like to be able to construct more complex proofs
(and indeed programs) interactively --- and so at the heart of \Ivor{}
is a theorem proving engine.
\subsection{Theorems}
In the \hdecl{emptyContext}, there is no proof in progress, so no
proof state --- the \hdecl{theorem} function creates a proof state in
a context. This will fail if there is already a proof in progress, or
the goal is not well typed.
\begin{verbatim}
theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
\end{verbatim}
A proof state can be thought of as an incomplete term, i.e. a
term in the development calculus.
For example, calling \hdecl{theorem}
with the name $\FN{plus}$ and type $\Nat\to\Nat\to\Nat$, an initial
proof state would be:
\DM{
\FN{plus}\:=\:\hole{\VV{plus}}{\Nat\to\Nat\to\Nat}
}
This theorem is, in fact, a specification (albeit imprecise) of a
program for adding two unary natural numbers, exploiting the
Curry-Howard isomorphism. Proving a theorem (i.e. also writing a
program interactively) proceeds by applying tactics to each unsolved
hole in the proof state. The system keeps track of which subgoals are
still to be solved, and a default subgoal, which is the next subgoal
to be solved. I will write proof states in the following form:
\DM{
\Rule{
\AR{
\mbox{\textit{bindings in the context of the subgoal $\vx_0$}} \\
\ldots\\
}
}
{
\AR{
\hole{\vx_0}{\mbox{\textit{default subgoal type}}} \\
\ldots \\
\hole{\vx_i}{\mbox{\textit{other subgoal types}}} \\
\ldots
}
}
}
Functions are available for querying the bindings in the context of
any subgoal. A tactic typically works on the bindings in scope and the
type of the subgoal it is solving.
When there are no remaining subgoals, a proof can be lifted into the
context, to be used as a complete definition, with the \texttt{qed}
function:
\begin{verbatim}
qed :: Monad m => Context -> m Context
\end{verbatim}
This function typechecks the entire proof. In practice, this check
should never fail --- the development calculus itself ensures that
partial constructions as well as complete terms are well-typed, so it
is impossible to build ill-typed partial constructions. However, doing
a final typecheck of a complete term means that the soundness of the
system relies only on the soundness of the typechecker for the core
language, e.g.~\cite{coq-in-coq}. We are free to implement tactics in
any way we like, knowing that any ill-typed constructions will be
caught by the typechecker.
%% but if the tactics are correctly implemented this check will always succeed.
\subsection{Basic Tactics}
A tactic is an operation on a goal in the current system state; we
define a type synonym \hdecl{Tactic} for functions which operate as
tactics. Tactics modify system state and may fail, hence a tactic
function returns a monad:
%
\begin{verbatim}
type Tactic = forall m . Monad m => Goal -> Context -> m Context
\end{verbatim}
%
A tactic operates on a hole binding, specified by the \texttt{Goal}
argument. This can be a named binding, \texttt{goal :: Name -> Goal},
or the default goal \texttt{defaultGoal :: Goal}. The default goal is
the first goal generated by the most recent tactic application.
\subsubsection{Hole Manipulations}
There are three basic operations on holes, \demph{claim}, \demph{fill},
and \demph{abandon}; these are given the following types:
%
\begin{verbatim}
claim :: IsTerm a => Name -> a -> Tactic
fill :: IsTerm a => a -> Tactic
abandon :: Tactic
\end{verbatim}
%
The \hdecl{claim} function takes a name and a type and creates a new
hole. The \hdecl{fill} function takes a guess to attach to the current
goal. In addition, \hdecl{fill} attempts to solve other goals by
unification. Attaching a guess does not necessarily solve the goal
completely; if the guess contains further hole bindings, it cannot yet
have any computational force.
%% The \hdecl{solve} tactic is provided to
%% check whether a guess is \demph{pure} (i.e. does not contain any hole
%% bindings or guesses itself) and converts it to a $\RW{let}$ binding if
%% so.
A guess can be removed from a goal with the \hdecl{abandon}
tactic.
%% It can be inconvenient to have to \texttt{solve} every goal after a
%% \texttt{fill} (although sometimes this level of control is
%% useful). For this reason, \texttt{fill} and other tactics will
%% automatically solve all goals with hole-free guesses attached. More
%% fine-grained tactics are available, but are beyond the scope of this paper.
\subsubsection{Introductions}
A basic operation on terms is to introduce $\lambda$ bindings into the
context. The \texttt{intro} and \texttt{introName} tactics operate on
a goal of the form $\fbind{\vx}{\vS}{\vT}$, introducing
$\lam{\vx}{\vS}$ into the context and updating the goal to
$\vT$. That is, a goal of this form is solved by a $\lambda$-binding.
\texttt{introName} allows a user specified name choice,
otherwise \Ivor{} chooses the name.
%
\begin{verbatim}
intro :: Tactic
introName :: Name -> Tactic
\end{verbatim}
%
For example, to define our addition function, we might begin with
\DM{
\Axiom{
\hole{\VV{plus}}{\Nat\to\Nat\to\Nat}
}
}
Applying \texttt{introName} twice with the names $\vx$ and $\vy$ gives
the following proof state, with $\vx$ and $\vy$ introduced into the
local context:
\DM{
\Rule{
\AR{
\lam{\vx}{\Nat}\\
\lam{\vy}{\Nat}
}
}
{\hole{\VV{plus\_H}}{\Nat}}
}
\subsubsection{Refinement}
The \texttt{refine} tactic solves a goal by an application of a
function to arguments. Refining attempts to solve a goal of type
$\vT$, when given a term of the form $\vt\Hab\fbind{\tx}{\tS}{\vT}$. The tactic
creates a subgoal for each argument $\vx_i$, attempting to solve it by
unification.
%
\begin{verbatim}
refine :: IsTerm a => a -> Tactic
\end{verbatim}
%
For example, given a goal
\DM{
\Axiom{
\hole{\vv}{\Vect\:\Nat\:(\suc\:\vn)}}
}
\noindent
Refining by $\Vcons$ creates subgoals for each argument, attaching
a guess to $\vv$:
\DM{
\Axiom{
\AR{
\hole{\vA}{\Type}\\
\hole{\vk}{\Nat}\\
\hole{\vx}{\vA}\\
\hole{\vxs}{\Vect\:\vA\:\vk}\\
\guess{\vv}{\Vect\:\Nat\:(\suc\:\vn)}{\Vcons\:\vA\:\vk\:\vx\:\vxs}
}
}
}
\noindent
However, for $\Vcons\:\vA\:\vk\:\vx\:\vxs$ to have type
$\Vect\:\Nat\:(\suc\:\vn)$ requires that $\vA=\Nat$ and $\vk=\vn$.
Refinement unifies these, leaving the
following goals:
\DM{
\Axiom{
\AR{
\hole{\vx}{\Nat}\\
\hole{\vxs}{\Vect\:\Nat\:\vn}\\
\guess{\vv}{\Vect\:\Nat\:(\suc\:\vn)}{\Vcons\:\Nat\:\vn\:\vx\:\vxs}
}
}
}
\subsubsection{Elimination}
Refinement solves goals by constructing new values; we may also solve
goals by deconstructing values in the context, using an elimination
operator as described in section \ref{elimops}. The \texttt{induction}
and \texttt{cases} tactics apply the $\delim$ and $\dcase$ operators
respectively to the given target:
%
\begin{verbatim}
induction, cases :: IsTerm a => a -> Tactic
\end{verbatim}
%
These tactics proceed by refinement by the appropriate elimination
operator. The motive for the elimination is calculated automatically
from the goal to be solved. Each tactic generates subgoals for each
method of the appropriate elimination rule.
%% A more general elimination tactic is \texttt{by}, which takes an
%% application of an elimination operator to a target.
%% \begin{verbatim}
%% by :: IsTerm a => a -> Tactic
%% \end{verbatim}
%% The type of the term given to \texttt{by} must be a function expecting
%% a motive and methods.
An example of \texttt{induction} is in continuing the definition of
our addition function. This can be defined by induction over the first
argument. We have the proof state
\DM{
\Rule{
\AR{
\lam{\vx}{\Nat}\\
\lam{\vy}{\Nat}
}
}
{\hole{\VV{plus\_H}}{\Nat}}
}
Applying \texttt{induction} to $\vx$ leaves two subgoals, one for the
case where $\vx$ is zero, and one for the inductive
case\footnote{c.f. the Haskell function \texttt{natElim
:: Nat -> a -> (Nat -> a -> a) -> a)}}:
\DM{
\Rule{
\AR{
\lam{\vx}{\Nat}\\
\lam{\vy}{\Nat}
}
}
{
\AR{
\hole{\VV{plus\_O}}{\Nat}\\
\hole{\VV{plus\_S}}{\fbind{\vk}{\Nat}{\fbind{\VV{k\_H}}{\Nat}{\Nat}}}
}
}
}
By default, the next goal to solve is $\VV{plus\_O}$. However, the
\hdecl{focus} tactic can be used to change the default goal.
The $\VV{k\_H}$ argument to the $\VV{plus\_S}$ goal is the result of a
recursive call on $\vk$.
\subsubsection{Rewriting}
It is often desirable to rewrite a goal given an equality proof, to
perform equational reasoning. The \texttt{replace} tactic replaces
occurrences of the left hand side of an equality with the right hand
side. To do this, it requires:
\begin{enumerate}
\item The equality type; for example
$\TC{Eq}\Hab\fbind{\vA}{\Type}{\vA\to\vA\to\Type}$.
\item A replacement lemma, which explains how to substitute one term
for another; for example\\
$\FN{repl}\Hab\fbind{\vA}{\Type}{
\fbind{\va,\vb}{\vA}{
\TC{Eq}\:\_\:\va\:\vb\to\fbind{\vP}{\vA\to\Type}{
\vP\:\va\to\vP\:\vb}}}$
\item A symmetry lemma, proving that equality is symmetric; for
example\\
$\FN{sym}\Hab\fbind{\vA}{\Type}{
\fbind{\va,\vb}{\vA}{\TC{Eq}\:\_\:\va\:\vb\to\TC{Eq}\:\_\:\vb\:\va}}$
\item An equality proof.
\end{enumerate}
The \Ivor{} distribution contains a library of $\source$ code with the
appropriate definitions and lemmas. Requiring the lemmas to be
supplied as arguments makes the library more flexible --- for example,
heterogeneous equality~\cite{mcbride-thesis} may be preferred. The
tactic will fail if terms of inappropriate types are given; recall
from sec. \ref{sec:devcalc} that the development calculus requires
that incomplete terms are also well-typed, so that all tactic
applications can be typechecked. The type is:
\begin{verbatim}
replace :: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) =>
a -> b -> c -> d -> Bool -> Tactic
\end{verbatim}
The \texttt{Bool} argument determines whether to apply the symmetry
lemma to the equality proof first, which allows rewriting from right
to left.
This \hdecl{replace} tactic is
similar to \Lego{}'s \texttt{Qrepl} tactic \cite{lego-manual}.
For example, consider the following fragment of proof state:
\DM{
\Rule{
\AR{
\ldots\\
\lam{\vx}{\Vect\:\vA\:(\FN{plus}\:\vx\:\vy)}
}
}
{
\hole{\VV{vect\_H}}{\Vect\:\vA\:(\FN{plus}\:\vy\:\vx)}
}
}
Since $\FN{plus}$ is commutative, $\vx$ ought to be a vector of the
correct length. However, the type of $\vx$ is not convertible to the
type of $\VV{vect\_H}$. Given a lemma $\FN{plus\_commutes}\Hab
\fbind{\vn,\vm}{\Nat}{\TC{Eq}\:\_\:(\FN{plus}\:\vn\:\vm)\:(\FN{plus}\:\vm\:\vn)}$,
we can use the \texttt{replace} tactic to rewrite the goal to the
correct form. Applying \texttt{replace} to $\TC{Eq}$, $\FN{repl}$,
$\FN{sym}$ and $\FN{plus\_commutes}\:\vy\:\vx$ yields the following
proof state, which is easy to solve using the \texttt{fill} tactic
with $\vx$.
\DM{
\Rule{
\AR{
\ldots\\
\lam{\vx}{\Vect\:\vA\:(\FN{plus}\:\vx\:\vy)}
}
}
{
\hole{\VV{vect\_H}}{\Vect\:\vA\:(\FN{plus}\:\vx\:\vy)}
}
}
\subsection{Tactic Combinators}
\label{combinators}
\Ivor{} provides an embedded domain specific language for
building tactics, in the form of a number of
combinators for building more complex tactics from the basic tactics
previously described. By providing an API for basic tactics and a
collection of combinators, it becomes easy to extend the library with
more complex domain specific tactics. We will see examples in
sections \ref{example1} and \ref{example2}.
\subsubsection{Sequencing Tactics}
There are three basic operators for combining two tactics to create a
new tactic:
\begin{verbatim}
(>->), (>+>), (>=>) :: Tactic -> Tactic -> Tactic
\end{verbatim}
\begin{enumerate}
\item The \hdecl{>->} operator constructs a new tactic by sequencing two
tactic applications to the \remph{same} goal.
\item The \hdecl{>+>} operator constructs a new tactic by applying the
first, then applying the second to the next \remph{default} goal.
\item The \hdecl{>=>} operator constructs a new tactic by applying the first
tactic, then applying the second to every subgoal generated by the first.
\end{enumerate}
\noindent
Finally, \hdecl{tacs} takes a list of tactics and applies
them in turn to the default goal:
\begin{verbatim}
tacs :: Monad m => [Goal -> Context -> m Context] ->
Goal -> Context -> m Context
\end{verbatim}
Note that the type of this is better understood as \hdecl{[Tactic] ->
Tactic}, but the Haskell typechecker requires that the same monad be
abstracted over all of the combined tactics.
\subsubsection{Handling Failure}
Tactics may fail (for example a refinement may be ill-typed).
Recovering gracefully from a failure may be needed, for
example to try a number of possible ways of rewriting a term.
The \hdecl{try} combinator is an exception handling combinator.
The identity tactic, \hdecl{idTac}, is often appropriate on success.
% which
%tries a tactic, and chooses a second tactic to apply to the same goal
%if the first tactic succeeds, or an alternative tactic if the first
%tactic fails.
\begin{verbatim}
try :: Tactic -> -- apply this tactic
Tactic -> -- apply if the tactic succeeds
Tactic -> -- apply if the tactic fails
Tactic
\end{verbatim}
%% \subsection{The Shell}
%% The \texttt{Ivor.Shell} module provides a command driven interface to
%% the library, which can be used for experimental purposes or for
%% developing a library of core lemmas for a domain specific task. It is
%% written entirely with the \texttt{Ivor.TT} interface but provides a
%% textual interface to the tactics. This gives, among other things, a
%% convenient method for loading proof scripts or libraries, or allowing
%% user directed proofs in the style of other proof assistants such as
%% \Coq{}.
%% A small driver program is provided (\texttt{jones}), which gives a
%% simple interface to the \Ivor{} shell.