\documentclass[runningheads]{llncs}
\begin{document}

\title{Mizar Light for HOL Light}
\author{Freek Wiedijk}
\institute{\email{freek@cs.kun.nl}\\Department of Computer Science\\University of Nijmegen\\The Netherlands}
\maketitle

\begin{abstract}\noindent
There are two different approaches to formalizing proofs in a computer:
the procedural approach (which is the one of the HOL system) and the declarative
approach (which is the one of the Mizar system).
Most provers are procedural.
However declarative proofs are
much closer in style to informal mathematical reasoning than procedural ones.

There have been attempts to put declarative interfaces
on top of procedural proof assistants, like John Harrison's
Mizar mode for HOL and Markus Wenzel's Isar mode for
Isabelle.
However in those cases the declarative assistant is
a {\em layer\/} on top of the procedural basis, having
a separate syntax and a different `feel' from the
underlying system.

This paper shows that the procedural and the declarative ways
of proving are related and can be integrated seamlessly.
It presents an implementation of the Mizar proof language on top of
HOL that consists of only 41 lines of ML.
This shows how close the procedural and
declarative styles of proving really are.
\end{abstract}


\section{Introduction}

We describe a programming experiment with the HOL system.
To be able to read this paper one has to have some familiarity with both the
HOL \cite{har:00} and Mizar \cite{muz:93,wie:99:1} systems.
The software described here is not meant to be used for
serious work (and it certainly doesn't emulate the full Mizar language).
Rather it's a kind of `thought experiment' to clarify the relation between the procedural and
declarative styles of proving.

This paper uses HOL for the procedural prover.
However the way the paper integrates Mizar-style proofs with it
also applies to other procedural systems like
Coq \cite{bar:bou:cor:cou:cos:del:rau:fil:gim:her:hue:lau:mun:mur:par:loi:pau:sai:wer:00} and Isabelle \cite{pau:00}.
For each of these systems a set of `Mizar tactics' could be written as described in this paper,
giving them `Mizar style' declarative proofs without a separate syntactic layer.

The plan of this paper is as follows.
It first presents the procedural and declarative
styles of proving and the HOL and Mizar systems.
Then Section \ref{basic} presents the main idea of the paper which is
implementing Mizar steps as HOL tactics.
For each of these `Mizar tactics' this section gives an ML type in the
framework of the HOL system.
After that the paper discusses various variations on this Mizar mode for HOL.
The paper concludes with a bigger example and an outlook.
The source code of the Mizar mode is an appendix.


\section{Procedural versus declarative proving}

The idea of formalizing mathematical proofs
in such a way that a computer can check the correctness is
not new but only recently it has become practical and popular.
Most of the proofs that are currently checked are proofs
of the correctness of computer software or hardware but
some people have also been formalizing other kinds of proofs
(for instance of mathematical theorems \cite{bau:99,ced:coq:neg:98}).

There are two main styles of proof checking programs
(the so-called proof checkers or proof assistants):
the {\em procedural\/} style and the {\em declarative\/} style.

The procedural proof checkers descend from a system from the
seventies called LCF \cite{gor:mil:wad:79}.
Such a system has a {\em proof state\/} which consists
of a set of `proof obligations'.
This state is transformed by means of so-called {\em tactics\/}
which take a proof obligation and reduce it to several simpler
ones (possibly none).
The proof process starts with the statement to be proved as
the sole proof obligation;
once no proof obligations remain, the proof is complete.
Procedural proofs consisting of a sequence of tactics
cannot be understood without interactively running them on a computer
because they only contain the transitions between the proof states
and not the proof states themselves.%
\footnote{Procedural proofs are therefore sometimes presented using {\em runs\/} of proof scripts (or,
even better, proof trees) showing intermediate goals.}
Also since the initial proof obligation is the final statement to be proved,
procedural proofs tend to run {\em backwards\/}, from the conclusion back
to the assumptions.

The other two proof checkers from the seventies, Automath \cite{ned:geu:vri:94}
and Mizar \cite{muz:93,wie:99:1}, both are of the declarative kind.
(Another system that is declarative is the Ontic system by David McAllester \cite{mca:89}.)
In a declarative system, a proof doesn't consist of instructions to
transform statements but of those statements themselves.
Furthermore, the statements are present in deductive order:
the assumptions are at the start and the conclusion is at the end.%
\footnote{The relation between backward and forward reasoning as related to procedural and
declarative proofs
is more subtle than is suggested here.
Declarative proofs (and informal mathematical reasoning as well) also take backward steps.
And many procedural provers also can do forward reasoning.
However the particular tactic collections found in procedural provers
tend to be biased towards backward reasoning.}

The procedural and declarative styles differ in several ways:
\begin{itemize}
\item
Declarative proofs are closer to informal mathematical reasoning
and therefore are more readable than
procedural proofs
because in a declarative proof the statements are present themselves
and in the proper order.

\item
Most current proof assistants are procedural
(perhaps because LCF style provers
are programmable by their users, while
declarative systems can generally only be extended by its developers).

\item
Declarative proofs can be written without the proof assistant running
and then checked with a batch oriented system.
Procedural proofs can only be developed interactively
because the computer has to keep track of the proof obligations.
Indeed, some declarative provers only have a batch mode
while procedural provers always also have an interactive mode.

\item
Since a declarative proof contains a chain of statements,
it is fairly robust with respect to errors.
If one step in the proof is erroneous, a declarative system
can recover from the error and check the rest of the proof file reasonably
well.
In contrast, a procedural prover stops checking at the first
error it encounters.
So after the point in the file where an error occurs, a
procedural system can't say much about correctness.

\end{itemize}
%
It seems natural to look for a way to integrate the procedural
and declarative approaches to proving.
Two attempts to put a declarative interface on a procedural
prover are the Mizar mode for HOL by John Harrison \cite{har:96}
and the Isar mode for Isabelle by Markus Wenzel \cite{wen:99}.

The Mizar mode for HOL by John Harrison is a true integration,
in the sense that the Mizar commands
behave like ordinary HOL tactics.
However this doesn't become clear from the way this
mode is presented.
For instance, the Mizar sub-language has a separate parser
from the (ML based) HOL proof language.
Also once the Mizar mode is active, the normal parser of
the HOL terms is no longer easily available.
This seems to suggest that once the Mizar mode has
been activated, the `normal' style of procedural HOL proving is not meant
to be used anymore.

The Mizar mode for HOL in this paper is a variation on
the Mizar mode of John Harrison.
Its main difference with Harrison's Mizar mode is that the
Mizar primitives {\em are\/} HOL tactics (so are not just compiled to them)
and therefore the integration is very tight.
Also the implementation of our Mizar mode takes only
41 lines of ML, which is smaller than Harrison's implementation
which consists of about 650 lines of ML.

The Isar mode for Isabelle differs from the Mizar mode for HOL
in that it has outgrown the experimental stage and has been used for
serious proofs \cite{bau:99,bau:wen:00,bau:01}.
However it really is a second layer on top of the Isabelle layer
(although it is possible to `embed' tactic scripts in Isar proofs),
so in this case there is no mixture between the two approaches.
In fact, both layers have their own proof state (called `the
static proof context' and `the dynamic goal state') which
are to be synchronized at certain checkpoints.
This is presented as a benefit because it makes it possible to
give a different order to the proof steps from the order imposed by
the underlying procedural basis but it shows that there is no tight
integration.

Two other declarative systems that integrate declarative proofs
with higher order logic
are the SPL system by Vincent Zammit \cite{zam:99}
and the Declare system by Don Syme \cite{sym:99}.
These two systems are not meant as a declarative interface to a procedural
prover.
Instead they are autonomous declarative systems.
(The SPL system is {\em implemented\/} on top of the HOL system
but it is not an interface to HOL.)

Procedural and declarative proof checkers both might or might not
satisfy what Henk Barendregt calls {\em the de Bruijn principle\/} and {\em the Poincar\'e
principle\/} \cite{bar:97}.
This paper is about the relation between procedural and
declarative proof styles.
This is unrelated to the issue of whether a system
should satisfy either of these principles or how to make it do so.


\section{Example: the drinker}

As a running example in this paper, we will use the so-called {\em drinker's
principle}.
This says that in every group of people one can
point to one person in the group such that if that person drinks
then all the people in the group drink.
This somewhat surprising
statement becomes in first order predicate logic:
$$\exists x.\big(P(x) \to \forall y.\,P(y)\big)$$
The HOL version of this is:
\begin{center}
\verb|?x:A. P x ==> !y. P y|
\end{center}
(so in HOL `\verb|?|' is the existential quantifier and `\verb|!|'
is the universal quantifier) and the Mizar version is:
\begin{center}
\verb|ex x st P x implies for y holds P y|
\end{center}
%
Here is an informal proof of the drinker's principle
(we will see below how this textual version compares both to
the proofs of this statement in the HOL and Mizar systems):

\begin{quote}\em
\label{informal}
Suppose that $P(x)$ is false for some $x$.
Then for that $x$ the implication holds because from
a false proposition one may deduce anything.
That means that in this case the proposition follows.

Now suppose that $P(x)$ is false for no $x$.
Then $P(x)$ is true for all $x$.
But that statement is
the conclusion of the implication and so the proposition again
follows.
\end{quote}
%
Almost all example proofs in this paper are proofs of this simple statement.
In Section \ref{big} we will present a bigger example.


\section{HOL}

The HOL system \cite{gor:mel:93} by Mike Gordon is a descendant from LCF
that implements Church's {\em Higher Order Logic\/}
(hence the acronym `HOL'), which is a classical higher
order logic encoded by simply typed lambda calculus with ML
style polymorphism.
The system guarantees
the correctness of its proofs by reducing everything in
LCF style to a `proof kernel', which because of its small size
(nine pages of ML code, about half of which is comment)
can be thoroughly checked for correctness by inspection.

The HOL system has had several implementations: HOL88, HOL90, HOL98,
ProofPower (a commercial version) and HOL Light.
The HOL Light system \cite{har:00} which is the HOL re-implementation by
John Harrison, is the version of the system that we have used
for this paper (but all versions are similar).
It has been written in CAML Light and consists of slightly under two
megabytes of ML source, which implement a mathematical
framework containing a formalization of the
real numbers, analysis and transcendental functions
and several decision procedures for both logical
and arithmetical problems.
It has been both used for computer science applications and
for formalizing pure mathematics (like the fundamental
theorem of algebra).

The drinker's principle can be proved in HOL in
the following way:
\begin{quote}
\begin{verbatim}
let DRINKER = prove
 (`?x:A. P x ==> !y. P y`,
  ASM_CASES_TAC `?x:A. ~P x` THEN
  RULE_ASSUM_TAC (REWRITE_RULE[NOT_EXISTS_THM]) THENL
  [POP_ASSUM CHOOSE_TAC; ALL_TAC] THEN
  EXISTS_TAC `x:A` THEN
  ASM_REWRITE_TAC[]);;
\end{verbatim}
\end{quote}
There are various ways to prove this statement, but this
tactic sequence is a fairly normal way to prove something like this in HOL.


\section{Mizar}

The Mizar system \cite{muz:93,wie:99:1} by Andrzej Trybulec and
his group in Bialystok, Poland,
is a declarative prover that goes back to the seventies.
It implements classical first order logic with ZFC-style set theory.
The current version, called PC Mizar, dates from 1989.
It consists of a suite of Pascal programs which are
distributed compiled for Intel processors (both Windows and Linux).
These programs are accompanied by a huge library of all kinds of
mathematics, in the form of a series of 686 so-called `articles'
which together are about 1.3 million lines of Mizar.

In Mizar a proof of the drinker's principle looks like:
\begin{quote}
\label{original}
\begin{verbatim}
ex x st P x implies for y holds P y
proof
  per cases;
  suppose A0: ex x st not P x;
    consider a such that A1: not P a by A0;
    take a;
    assume A2: P a;
    A3: contradiction by A1,A2;
    thus A4: for y holds P y by A3;
  suppose A5: for x holds P x;
    consider a such that A6: not contradiction;
    take a;
    thus A7: P a implies for y holds P y by A5;
end;
\end{verbatim}
\end{quote}
Note that this is readable and similar to the
informal proof in Section \ref{informal}.

The Mizar system has many interesting ideas.
For instance it has a complicated type system with polymorphic
types, overloading, subtyping and type modifiers called `adjectives',
together with powerful type inference rules.
Also it has a mathematical looking operator syntax with not only
prefix and infix operators but also `aroundfix' operators, which
behave like brackets.
However in this paper we will restrict ourselves to the proof
language of Mizar.
That means that from now on we will only have HOL types
and HOL term syntax and we will not mix those with Mizar
types and Mizar term syntax.
The same restriction to just the proof fragment of Mizar was
chosen for the Mizar mode for HOL by John Harrison.

The reasoning part of Mizar turns out to be simple.
In its basic form it is given by the following context free grammar:
\begin{quote}
\begin{flushleft}
\label{grammar}
{\em proposition\/} = [ {\em label\/} \verb|:| ] {\em formula\/}
\smallskip

{\em statement\/} = {\em proposition\/} {\em justification\/}
\smallskip

{\em justification\/} =\\
\quad {\em empty\/}\\
\strut\rlap{$|$}\quad \verb|by| {\em label\/} \{\verb|,| {\em label\/}\}\\
\strut\rlap{$|$}\quad \verb|proof| \{{\em step\/}\} [ {\em cases\/} ] \verb|end|
\smallskip

{\em step\/} =\\
\quad {\em statement\/} \verb|;|\\
\strut\rlap{$|$}\quad \verb|assume| {\em proposition\/} \verb|;|\\
\strut\rlap{$|$}\quad \verb|consider| {\em variable\/} \{\verb|,| {\em variable\/}\}\\
\hfill \verb|such| \verb|that| {\em proposition\/} \{\verb|and| {\em proposition\/}\} {\em justification\/} \verb|;|\\
\strut\rlap{$|$}\quad \verb|let| {\em variable\/} \{\verb|,| {\em variable\/}\} \verb|;|\\
\strut\rlap{$|$}\quad \verb|take| {\em term\/} \{\verb|,| {\em term\/}\} \verb|;|\\
\strut\rlap{$|$}\quad \verb|thus| {\em statement\/} \verb|;|
\smallskip

{\em cases\/} = \verb|per| \verb|cases| {\em justification\/} \verb|;|
\{\verb|suppose| {\em proposition\/} \verb|;| \{{\em step\/}\}\}
\smallskip

{\em empty\/} =
\end{flushleft}
\end{quote}
The main Mizar proof feature that is missing from this language fragment is
the use of `\verb|.=|' for equational reasoning.

Note that this grammar has only seven kinds of proof
elements: a statement without keyword, \verb|assume|,
\verb|consider|, \verb|let|, \verb|per| \verb|cases|, \verb|take|
and \verb|thus|.
(Compare this with the hundreds of different tactics, tacticals,
conversions and conversionals that appear all over the
HOL proofs.)


\section{Mizar as HOL tactics}\label{basic}

We will compare the way the Mizar and HOL systems
implement natural deduction.
That will lead to a natural ML type (in the framework of HOL)
for each of the Mizar steps.
The table that lists these types
is the essence of our Mizar implementation on top of HOL.
(The appendix will show how to implement the Mizar steps according
to these types.)

There are two kinds of Mizar steps:
\begin{itemize}
\item
{\em skeleton\/} steps: the natural deduction way of reasoning
\item
{\em forward\/} steps: statements that get added to the context after
having been justified with the `\verb|by|' justification
\end{itemize}
The natural deduction rules correspond to Mizar steps
according to following table
(rules for which a `--' appears in this table
are implemented as forward steps and don't have a Mizar
step of their own):
\begin{center}
\begin{tabular}{lc}
\hline\noalign{\smallskip}
{\em natural deduction} & {\em Mizar} \\
\noalign{\smallskip}\hline\noalign{\smallskip}
$\to$ introduction & \verb|assume| \\
$\to$ elimination & -- \\
$\land$ introduction & \verb|thus| \\
$\land$ elimination & -- \\
$\lor$ introduction & -- \\
$\lor$ elimination & \verb|per| \verb|cases| \\
$\forall$ introduction & \verb|let| \\
$\forall$ elimination & -- \\
$\exists$ introduction & \verb|take| \\
$\exists$ elimination & \verb|consider| \\
\noalign{\smallskip}\hline
\end{tabular}
\end{center}
%
The HOL language has natural deduction as well.
The main difference is that the Mizar steps make the
propositions explicit that the
HOL steps leave implicit.

Compare the two ways to do $\to$ introduction.
Suppose we want to reduce the goal:
$$A, B \vdash (C \to D) \to E$$
to:
$$A, B, \,(C \to D) \vdash E$$
(this is the {\em introduction} rule because a goal oriented
prover reasons backwards).
The Mizar step doing this is:
\begin{center}
\verb|assume A2: C implies D;|
\end{center}
(here `\verb|A2|' is the label of the assumption).
The same is accomplished in HOL by:
\begin{center}
\verb|DISCH_TAC|
\end{center}
or if we write out the proof state transformation explicitly:
\begin{quote}
\begin{flushleft}
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`A`]|\\
\verb| 1 [`B`]|\\
\medskip
\verb|`(C ==> D) ==> E`|\\
\medskip
\verb|#e DISCH_TAC;;|\\
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`A`]|\\
\verb| 1 [`B`]|\\
\verb| 2 [`C ==> D`]|\\
\medskip
\verb|`E`|
\end{flushleft}
\end{quote}
The Mizar statement gives the `redundant'
information what the discharged statement is and where it ends up in
the context.
We can imitate this in HOL by defining a tactic \verb|ASSUME_A| such that
the HOL tactic becomes:
\begin{center}
\verb|ASSUME_A(2,`C ==> D`)|
\end{center}
or explicitly:
\begin{quote}
\begin{flushleft}
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`A`]|\\
\verb| 1 [`B`]|\\
\medskip
\verb|`(C ==> D) ==> E`|\\
\medskip
\verb|#e (ASSUME_A(2,`C ==> D`));;|\\
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`A`]|\\
\verb| 1 [`B`]|\\
\verb| 2 [`C ==> D`]|\\
\medskip
\verb|`E`|
\end{flushleft}
\end{quote}
All that the \verb|ASSUME_A| tactic does is check that the number
and statement fit and then apply \verb|DISCH_TAC|.

The \verb|ASSUME_A| tactic has the type:
\begin{center}
\verb|int| $\times$ \verb|term| $\to$ \verb|tactic|
\end{center}
If we continue along this line of thought, it turns out that
every Mizar construction has a `natural' HOL type.
The table that gives these types is the essence of
our Mizar mode for HOL:
\begin{center}
\begin{tabular}{ll}
\hline\noalign{\smallskip}
\verb|A|         & \verb|int| $\times$ \verb|term| $\to$ \verb|tactic| $\to$ \verb|tactic| \\
\verb|ASSUME_A|  & \verb|int| $\times$ \verb|term| $\to$ \verb|tactic| \\
\verb|BY|        & \verb|int list| $\to$ \verb|thm list| $\to$ \verb|tactic| \\
\verb|CONSIDER|  & \verb|term list| $\to$ \verb|(int| $\times$ \verb|term) list| $\to$ \verb|tactic| $\to$ \verb|tactic| \\
\verb|LET|       & \verb|term list| $\to$ \verb|tactic| \\
\verb|PER_CASES|\hspace{1em} & \verb|tactic| $\to$ \verb|((int| $\times$ \verb|term)| $\times$ \verb|tactic) list| $\to$ \verb|tactic| \\
\verb|TAKE|      & \verb|term list| $\to$ \verb|tactic| \\
\verb|THUS_A|    & \verb|int| $\times$ \verb|term| $\to$ \verb|tactic| $\to$ \verb|tactic| \\
\noalign{\smallskip}\hline
\end{tabular}
\end{center}
Note that this table corresponds to the Mizar proof grammar
from Section \ref{grammar}.
Implementing these eight tactics is trivial, as shown in the appendix.
%
The first of these tactics, the \verb|A| tactic, corresponds to a Mizar step without a
keyword: a forward reasoning step.
%
The \verb|BY| tactic is used to justify steps.
It takes two lists of arguments.
The first list is a list of integers referring to the assumption
list of the current goal,
the second list is a list of \verb|thm|s.

Now we can write down the proof of the
drinker's principle as a normal HOL proof (so with \verb|prove|
and a chain of tactics put together with \verb|THEN|),
this time using the `Mizar tactics':
\begin{quote}
\begin{verbatim}
let DRINKER = prove
 (`?x:A. P x ==> !y. P y`,
  PER_CASES (BY [][])
  [(0,`?x:A. ~P x`),
   (CONSIDER [`a:A`] [(1,`~(P:A->bool) a`)] (BY [0][]) THEN
    TAKE [`a:A`] THEN
    ASSUME_A(2,`(P:A->bool) a`) THEN
    A(3,`F`) (BY [1;2][]) THEN
    THUS_A(4,`!y:A. P y`) (BY [3][]))
  ;(0,`!x:A. P x`),
   (CONSIDER [`a:A`] [] (BY [][]) THEN
    TAKE [`a:A`] THEN
    THUS_A(1,`P a ==> !y:A. P y`) (BY [0][]))]);;
\end{verbatim}
\end{quote}
Note that this is similar to the Mizar version of this
proof from Section \ref{original}.
The main difference is that type annotations
are needed (\verb|`(P:A->bool)|{\tt{ }}\verb|a`| instead of \verb|`P a`|).
This problem of having to put type annotations in
terms is standard in HOL.
A possible approach to this problem will be presented in Section \ref{context}.


\section{Enhancements}\label{enhance}

The Mizar tactics that we presented in the previous section are very basic.
They can be enhanced in various ways.
Because we lack the space we don't give all the details.
Curious readers are referred to the HOL Light source file \verb|miz.ml|
at the URL \verb|<http://www.cs.kun.nl/~freek/mizar/miz.ml>|.


\subsection{The {\tt BECAUSE} tactic}

The common way to justify a Mizar step in our Mizar mode
is with a justification that looks like:
\begin{center}
\verb|(BY [|{\em local statement list\/}\verb|][|{\em global statement list\/}\verb|])|
\end{center}
This has the prover `hardwired in' (in the implementation
from the
appendix, this prover first tries \verb|REWRITE_TAC|
and if that fails tries \verb|MESON_TAC|).
However the \verb|BY| tactic is built on top of a tactic called `\verb|BECAUSE|'
which has the type:
\begin{center}
\verb|(thm list| $\to$ \verb|tactic)| $\to$ \verb|int list| $\to$ \verb|thm list| $\to$ \verb|tactic|
\end{center}
This means that one can use it with any tactic that has the type
\verb|thm list| $\to$ \verb|tactic|
like \verb|REWRITE_TAC|, \verb|SIMP_TAC|, \verb|MESON_TAC| and so on.
(One also could use it with tactics like \verb|ASM_REWRITE_TAC| but that
would be silly, because the assumptions already are accessible through the `local
statements' argument.)
For instance one could justify a step by:
\begin{center}
\verb|(BECAUSE ONCE_SIMP_TAC[|{\em local statement list\/}\verb|][|{\em global statement list\/}\verb|])|
\end{center}
This would prove the statement being justified using the \verb|ONCE_SIMP_TAC| tactic with the relevant \verb|thm|s.

The \verb|BECAUSE| tactic gives control over the exact
behavior of the prover if that is needed, making a refined version of
\verb|BY| unnecessary.


\subsection{A more powerful {\tt ASSUME\_A} tactic}

The \verb|ASSUME_A| tactic is the declarative version of the procedural \verb|DISCH_TAC| tactic.
The implementation from the appendix mirrors \verb|DISCH_TAC| exactly.
However since the \verb|ASSUME_A| tactic contains the statement that is discharged, it can be more general.
It becomes more powerful if we implement it as:
\begin{quote}
\begin{verbatim}
let ASSUME_A (n,tm) =
  DISJ_CASES_THEN2
    (fun th -> REWRITE_TAC[th] THEN N_ASSUME_TAC n th)
    (fun th -> REWRITE_TAC[REWRITE_RULE[] th] THEN
      MIZ_ERROR_TAC "ASSUME_A" [n])
    (SPEC tm EXCLUDED_MIDDLE);;
\end{verbatim}
\end{quote}
For instance in that case one can use it to reason by contradiction:
\begin{quote}
\begin{flushleft}
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb|`A`|\\
\medskip
\verb|#e (ASSUME_A(0,`~A`));;|\\
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`~A`]|\\
\medskip
\verb|`F`|
\end{flushleft}
\end{quote}
This is also how the \verb|assume| step of the real Mizar system behaves.


\subsection{An interactive version of the {\tt PER\_CASES} tactic}

The \verb|PER_CASES| tactic has the type:
\begin{center}
\begin{tabular}{rcl}
\verb|PER_CASES| &$\;:\;$& \verb|tactic| $\to$ \verb|((int| $\times$ \verb|term)| $\times$ \verb|tactic) list| $\to$ \verb|tactic|
\end{tabular}
\end{center}
In order to debug a proof interactively a version that has type:
\begin{center}
\begin{tabular}{rcl}
\verb|PER_CASES| &$\;:\;$& \verb|tactic| $\to$ \verb|(int| $\times$ \verb|term) list| $\to$ \verb|tactic|
\end{tabular}
\end{center}
and that leaves the cases as subgoals is more practical.
Using this variant makes the proof look less like Mizar because the list of
the statements of the cases has been separated from the list of proofs of the cases.

A hybrid is also possible that has the type of the original \verb|PER_CASES| but doesn't require all the cases to be
completely proved after the tactic finishes.


\subsection{Tactics versus proofs}

Some of the \verb|tactic| arguments of the Mizar tactics
not only have to {\em reduce\/} the proof obligations
but they have to prove the goal altogether.
So those arguments are more `proofs' than `tactics'.
One might try to reflect this in the typing of the Mizar
tactics by at certain places changing
\verb|tactic|
(which is defined as \verb|goal| $\to$ \verb|goalstate|)
to
\verb|goal| $\to$ \verb|thm|.
The second type is in a way a special case (`subtype') of the first.
Then functions:
\begin{center}
\begin{tabular}{rcl}
\verb|PROOF| &$\;:\;$& \verb|tactic| $\to$ \verb|goal| $\to$ \verb|thm|\\
\verb|PER|   &$\;:\;$& \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|tactic|
\end{tabular}
\end{center}
map these two types to each other and:
\begin{center}
\verb|prove'| $\;:\;$ \verb|term| $\times$ \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|thm|
\end{center}
runs a proof.
Using this approach, the Mizar mode tactics will get the following type assignments:
\begin{center}
\begin{tabular}{ll}
\hline\noalign{\smallskip}
\verb|A|         & \verb|int| $\times$ \verb|term| $\to$ \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|tactic| \\
\verb|ASSUME_A|  & \verb|int| $\times$ \verb|term| $\to$ \verb|tactic| \\
\verb|BY|        & \verb|int list| $\to$ \verb|thm list| $\to$ \verb|goal| $\to$ \verb|thm| \\
\verb|CASES|     & \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|((int| $\times$ \verb|term)| $\times$ \verb|(goal| $\to$ \verb|thm)) list| \\
                 & $\quad\to$ \verb|goal| $\to$ \verb|thm| \\
\verb|CONSIDER|\hspace{1em} & \verb|term list| $\to$ \verb|(int| $\times$ \verb|term) list| $\to$ \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|tactic| \\
\verb|LET|       & \verb|term list| $\to$ \verb|tactic| \\
\verb|TAKE|      & \verb|term list| $\to$ \verb|tactic| \\
\verb|THUS_A|    & \verb|int| $\times$ \verb|term| $\to$ \verb|(goal| $\to$ \verb|thm)| $\to$ \verb|tactic| \\
\noalign{\smallskip}\hline
\end{tabular}
\end{center}
(Note that we have separated the \verb|PER_CASES| tactic into a
combination of \verb|PER| and \verb|CASES|.)
The example proof becomes, using these tactics:
\begin{quote}
\begin{verbatim}
let DRINKER = prove'
 (`?x:A. P x ==> !y. P y`,
  PROOF
  (PER (CASES (BY [][])
    [(0,`?x:A. ~P x`),
     PROOF
     (CONSIDER [`a:A`] [(1,`~(P:A->bool) a`)] (BY [0][]) THEN
      TAKE [`a:A`] THEN
      ASSUME_A(2,`(P:A->bool) a`) THEN
      A(3,`F`) (BY [1;2][]) THEN
      THUS_A(4,`!y:A. P y`) (BY [3][]))
    ;(0,`!x:A. P x`),
     PROOF
     (CONSIDER [`a:A`] [] (BY [][]) THEN
      TAKE [`a:A`] THEN
      THUS_A(1,`P a ==> !y:A. P y`) (BY [0][]))])));;
\end{verbatim}
\end{quote}


\subsection{Terms in context}\label{context}

The HOL system parses a \verb|term| in
an empty context because the HOL implementation is functional.
So if we write an expression of type \verb|term| it doesn't have
access to the goal state.
This means that \verb|`n`| will always be read as a polymorphic variable,
whatever is in the current goal.
If a goal talks about a natural number \verb|`n`| of type \verb|`:num`|,
then to instantiate an existential quantifier with this \verb|`n`|
one has to write
\verb|EXISTS_TAC `n:num`|
instead of
\verb|EXISTS_TAC `n`|.
Generally this doesn't get too bad but it is irritating.

In our Mizar mode this problem is worse because there are
more statements in the tactics.
So we might try to modify things for this.
The idea is to change the type
\verb|term|
to
\verb|goal| $\to$ \verb|term|
everywhere.
This means that the `term parsing function' \verb|X| will have to get the type
\verb|string| $\to$ \verb|goal| $\to$ \verb|term|.
Again a variant function \verb|prove''| of type
\verb|(goal| $\to$ \verb|term)| $\times$ \verb|tactic| $\to$ \verb|thm|
is needed.

If we follow this approach then most type annotations will be gone, except in the
statement of the theorem to be proved and in the arguments
of \verb|LET| and \verb|CONSIDER| (where they also are
required in the `real' Mizar).

Because in that case the terms are parsed in the context of
a goal, we can give a special meaning to the variables \verb|`antecedent`|
and \verb|`thesis`|.
See Section \ref{big} for an example of this.

The main disadvantage of this modification to our Mizar mode
is that the original HOL proof scripts will not
work anymore because the \verb|X| function has been changed.
That is a big disadvantage if one wants true integration between
the `pure' HOL and the Mizar mode.


\subsection{Out of sequence labels and negative labels}

Another thing that can be changed is to be less restrictive which numbers are allowed for the labels.
Until now they had to be the exact position that the statement would end up
in the assumption list of the goal.
However there is no reason not to allow any number and put
the statement at that position, padding the assumption list with \verb|`T`| \verb|thm|s
if necessary.
That way we can make the labels in the example match the labels
in the original Mizar version.
If we do this in the example proof, then the second \verb|CONSIDER| will see a goal like:
\begin{quote}
\begin{flushleft}
\verb|it : goalstack = 1 subgoal (1 total)|\\
\medskip
\verb| 0 [`T`]|\\
\verb| 1 [`T`]|\\
\verb| 2 [`T`]|\\
\verb| 3 [`T`]|\\
\verb| 4 [`T`]|\\
\verb| 5 [`!x. P x`]|\\
\medskip
\verb|`?x. P x ==> (!y. P y)`|
\end{flushleft}
\end{quote}
%
Related to this is an enhancement that implements Mizar's \verb|then|.
In Mizar a step can refer to the step
directly before it with the \verb|then| prefix.
%
A way to imitate this in our Mizar
mode is to allow negative numbers in the labels, counting
back from the top of the assumption stack.
The label \verb|-1|
will then refer to the top of the stack (which contains the statement from the previous step).
Therefore use of \verb|-1| will behave like \verb|then|.


\subsection{Symbolic labels}

Instead of numeric labels we also can have symbolic labels.
HOL Light supports symbolic labels already.
It is straight-forward to change the set of Mizar tactics to work with these symbolic labels
instead of with the numeric positions in the list of assumptions.

In the rest of this paper we have presented our Mizar mode with numeric labels.
We had two reasons for this:
\begin{itemize}
\item In HOL the symbolic labels are almost never used, so proof states that contain them
are un-HOL-like.
\item In Mizar the `symbolic' labels generally just are \verb|A1|, \verb|A2|, \verb|A3|, \dots
That means that the Mizar labels really are used as numbers, most of the time.
Therefore we didn't consider numeric labels un-Mizar-like.
\end{itemize}


\subsection{Error recovery}

A declarative proof contains explicit statements for all reasoning steps.
Because of this a declarative system like Mizar
can recover from errors and continue checking proofs after the first error.%
\footnote{The Mizar mode by John Harrison does not have this feature.
Isar satisfies the principle that sub-proofs can be checked
independently, but the present implementation simply
stops at the first error it encounters.}
This behavior can be added to our Mizar mode for HOL by catching the exception
if there is an error,
and then continue with the appropriate statement added to the context as an axiom.
This was implemented by using a justification function that just throws an exception.

Having this enhancement of course only gives error recovery for `reasoning errors' and will not
help with other errors like syntax errors or ML type errors.

One of the referees of this paper liked the idea of error recovery for
the Mizar tactics, and suggested a stack on which
the goalstates of the erroneous steps could be stored for later proof debugging.
We implemented this idea, but we think that the standard
HOL practice of running a proof one tactic at a time is more convenient
(for which the `Mizar tactics with error recovery' are unusable).


\section{Bigger example}\label{big}

In this section we show a larger example of our Mizar
mode (it uses the variant
from Section \ref{context}, so terms are parsed
in the context of the proof):
\begin{quote}\footnotesize
\begin{verbatim}
let FIXPOINT = prove''
 (`!f. (!x:A y. x <= y /\ y <= x ==> (x = y)) /\
       (!x y z. x <= y /\ y <= z ==> x <= z) /\
       (!x y. x <= y ==> f x <= f y) /\
       (!X. ?s. (!x. x IN X ==> s <= x) /\
                (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s))
       ==> ?x. f x = x`,
  LET [`f:A->A`] THEN
  ASSUME_A(0,`antecedent`) THEN
  A(1,`!x y. x <= y /\ y <= x ==> (x = y)`) (BY [0][]) THEN
  A(2,`!x y z. x <= y /\ y <= z ==> x <= z`) (BY [0][]) THEN
  A(3,`!x y. x <= y ==> f x <= f y`)(BY [0][]) THEN
  A(4,`!X. ?s. (!x. x IN X ==> s <= x) /\
               (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s)`)
    (BY [0][]) THEN
  CONSIDER [`Y:A->bool`] [(5,`Y = {b | f b <= b}`)] (BY [][]) THEN
  A(6,`!b. b IN Y = f b <= b`) (BY [5][IN_ELIM_THM;BETA_THM]) THEN
  CONSIDER [`a:A`] [(7,`!x. x IN Y ==> a <= x`);
    (8,`!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a`)] (BY [4][]) THEN
  TAKE [`a`] THEN
  A(9,`!b. b IN Y ==> f a <= b`)
   (LET [`b:A`] THEN
    ASSUME_A(9,`b IN Y`) THEN
    A(10,`f b <= b`) (BY [6;9][]) THEN
    A(11,`a <= b`) (BY [7;9][]) THEN
    A(12,`f a <= f b`) (BY [3;11][]) THEN
    THUS_A(13,`f a <= b`) (BY [2;10;12][])) THEN
  A(10,`f(a) <= a`) (BY [8;9][]) THEN
  A(11,`f(f(a)) <= f(a)`) (BY [3;10][]) THEN
  A(12,`f(a) IN Y`) (BY [6;11][]) THEN
  A(13,`a <= f(a)`) (BY [7;12][]) THEN
  THUS_A(14,`thesis`) (BY [1;10;13][]));;
\end{verbatim}
\end{quote}
This is a translation to our framework of an example proof from John Harrison's Mizar mode
which proves the Knaster-Tarski fixpoint theorem.


\section{Conclusion}

The tactics that are presented here might
be the basis of a realistic system that offers the best of
both the procedural and declarative provers.
One hopes this to be possible: to build a prover
that has the readable proofs of the declarative
provers and the programmability of the procedural ones.
The Mizar mode for HOL by John Harrison and the Isar mode for Isabelle might
claim to be just that,
but in those systems it feels
like one has to learn {\em two\/} provers if one wants to
be able to use both styles of proving.

The Mizar mode of this paper makes clear that that both kinds of prover are very similar.
Although the proofs using our Mizar tactics look awkward and fragile compared
with their Mizar counterparts,
we have shown that it is possible to bridge the gap between the procedural
and declarative proof styles
in a more intimate way than had been accomplished thus far.


\paragraph{Acknowledgements.}
Thanks to Dan Synek, Jan Zwanenburg and the anonymous referees for valuable comments.
Due to space limits we have not been able to incorporate all of them.


%\bibliographystyle{plain}
%\bibliography{frk}

\begin{thebibliography}{10}

\bibitem{bar:97}
Henk Barendregt.
\newblock {The impact of the lambda calculus}.
\newblock {\em Bulletin of Symbolic Logic}, 3(2), 1997.

\bibitem{bar:bou:cor:cou:cos:del:rau:fil:gim:her:hue:lau:mun:mur:par:loi:pau:s%
ai:wer:00}
Bruno Barras, e.a.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2000.
\newblock \hfill\break \verb|<ftp://ftp.inria.fr/INRIA/coq/V6.3.1/doc/Reference-Manual-all.ps.gz>|.

\bibitem{bau:99}
Gertrud Bauer.
\newblock Lesbare formale {B}eweise in {I}sabelle/{I}sar --- der {S}atz von
  {H}ahn-{B}anach.
\newblock Master's thesis, TU M\"unchen, November 1999.
\newblock \hfill\break
  \verb|<http://www.in.tum.de/~bauerg/HahnBanach-DA.pdf>|.

\bibitem{bau:01}
Gertrud Bauer.
\newblock The {H}ahn-{B}anach {T}heorem for real vector spaces.
\newblock Part of the Isabelle99-2 distribution,
  \verb|<http://isabelle.in.tum.de/| \hfill\break\hbox{}\hfill
  \verb|library/HOL/HOL-Real/HahnBanach/document.pdf>|, February 2001.

\bibitem{bau:wen:00}
Gertrud Bauer and Markus Wenzel.
\newblock Computer-assisted mathematics at work --- the {H}ahn-{B}anach theorem
  in {I}sabelle/{I}sar.
\newblock In Thierry Coquand, Peter Dybjer, Bengt Nordstr\"om, and Jan Smith,
  editors, {\em Types for Proofs and Programs: TYPES'99}, volume 1956 of {\em
  LNCS}, 2000.

\bibitem{ced:coq:neg:98}
Jan Cederquist, Thierry Coquand, and Sara Negri.
\newblock {The Hahn-Banach Theorem in Type Theory}.
\newblock In G.~Sambin and J.~Smith, editors, {\em Twenty-Five years of
  Constructive Type Theory}, Oxford, 1998. Oxford University Press.

\bibitem{gor:mel:93}
M.J.C. Gordon and T.F. Melham, editors.
\newblock {\em Introduction to HOL}.
\newblock Cambridge University Press, Cambridge, 1993.

\bibitem{gor:mil:wad:79}
M.J.C. Gordon, R.~Milner, and C.P. Wadsworth.
\newblock {\em Edinburgh LCF: A Mechanised Logic of Computation}, volume~78 of
  {\em LNCS}.
\newblock Springer Verlag, Berlin, Heidelberg, New York, 1979.

\bibitem{har:96}
John Harrison.
\newblock {A Mizar Mode for HOL}.
\newblock In {\em Proceedings of the 9th International Conference on Theorem
  Proving in Higher Order Logics, TPHOLs '96}, volume 1125 of {\em LNCS}, pages
  203--220. Springer, 1996.

\bibitem{har:00}
John Harrison.
\newblock {\em The HOL Light manual (1.1)}, 2000.
\newblock \hfill\break
  \verb|<http://www.cl.cam.ac.uk/users/jrh/hol-light/manual-1.1.ps.gz>|.

\bibitem{mca:89}
David~A. McAllester.
\newblock {\em Ontic: A Knowledge Representation System for Mathematics}.
\newblock The MIT Press Series in Artificial Intelligence. MIT Press, 1989.

\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fondation Philippe le Hodey, Brussels, 1993.
\newblock
  \verb|<http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz>|.

\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C.~de Vrijer.
\newblock {\em Selected Papers on Automath}, volume 133 of {\em Studies in
  Logic and the Foundations of Mathematics}.
\newblock Elsevier Science, Amsterdam, 1994.

\bibitem{pau:00}
L.C. Paulson.
\newblock {\em The Isabelle Reference Manual}, 2000.
\newblock \verb|<http://www.cl.cam.ac.uk/|
  \hfill\break\hbox{}\hfill
  \verb|Research/HVG/Isabelle/dist/Isabelle99-1/doc/ref.pdf>|.

\bibitem{sym:99}
Don Syme.
\newblock {Three Tactic Theorem Proving}.
\newblock In {\em Theorem Proving in Higher Order Logics, TPHOLs '99},
volume 1690 of {\em LNCS}, pages 203--220. Springer, 1999.

\bibitem{wen:99}
M.~Wenzel.
\newblock {\em The Isabelle/Isar Reference Manual}.
\newblock TU M{\"u}nchen, M{\"u}nchen, 1999.
\newblock \hfill\break
  \verb|<http://isabelle.in.tum.de/doc/isar-ref.pdf>|.

\bibitem{wie:99:1}
F.~Wiedijk.
\newblock Mizar: An impression.
\newblock \hfill\break
  \verb|<http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz>|, 1999.

\bibitem{zam:99}
Vincent Zammit.
\newblock {On the Implementation of an Extensible Declarative Proof Language}.
\newblock In {\em Theorem Proving in Higher Order Logics, TPHOLs '99},
volume 1690 of {\em LNCS}, pages 185--202. Springer, 1999.

\end{thebibliography}


\appendix
\section{Implementation}

Here is the full listing of the Mizar implementation as described
in Section \ref{basic}.

\newcounter{lineno}
\newcommand{\lineno}{\addtocounter{lineno}{1}%
  \makebox[0pt][l]{%
    \makebox[0pt][r]{\tiny\bf\thelineno
    \quad
    }}%
  }

\begin{flushleft}\footnotesize
\lineno\verb|let miz_error msg nl =|\\
\lineno\verb|  failwith (rev_itlist (fun s t -> t^" "^s) (map string_of_int nl) msg);;|\\
\medskip
\lineno\verb|let MIZ_ERROR_TAC msg nl = fun g -> miz_error msg nl;;|\\
\medskip
\lineno\verb|let N_ASSUME_TAC n th (asl,_ as g) =|\\
\lineno\hbox to\hsize{\verb|  if length asl = n then ASSUME_TAC th g else miz_error "N_ASSUME_TAC" [n];;|\hss}\\
\medskip
\lineno\verb|let A (n,tm) tac =|\\
\lineno\verb|  SUBGOAL_THEN tm (N_ASSUME_TAC n) THENL|\\
\lineno\verb|  [tac THEN MIZ_ERROR_TAC "A" [n]; ALL_TAC];;|\\
\medskip
\lineno\verb|let ASSUME_A (n,tm) =|\\
\lineno\verb|  DISCH_THEN (fun th -> if concl th = tm then N_ASSUME_TAC n th|\\
\lineno\verb|    else miz_error "ASSUME_A" [n]);;|\\
\medskip
\lineno\verb|let (BECAUSE:(thm list -> tactic) -> int list -> thm list -> tactic) =|\\
\lineno\verb|  fun tac nl thl (asl,_ as g) ->|\\
\lineno\hbox to\hsize{\verb|    try tac ((map (fun n -> snd (el (length asl - n - 1) asl)) nl) @ thl) g|\hss}\\
\lineno\verb|    with _ -> ALL_TAC g;;|\\
\medskip
\lineno\verb|let BY = BECAUSE (fun thl -> REWRITE_TAC thl THEN MESON_TAC thl);;|\\
\medskip
\lineno\verb|let CONSIDER =|\\
\lineno\verb|  let T = `T` in|\\
\lineno\verb|  fun vl ntml tac ->|\\
\lineno\verb|    let ex = itlist (curry mk_exists) vl|\\
\lineno\verb|      (itlist (curry mk_conj) (map snd ntml) T) in|\\
\lineno\verb|    SUBGOAL_THEN ex|\\
\lineno\verb|      ((EVERY_TCL (map X_CHOOSE_THEN vl) THEN_TCL EVERY_TCL (map|\\
\lineno\verb|         (fun (n,_) tcl cj ->|\\
\lineno\verb|           let th,cj' = CONJ_PAIR cj in N_ASSUME_TAC n th THEN tcl cj')|\\
\lineno\verb|       ntml)) (K ALL_TAC)) THENL|\\
\lineno\verb|    [tac THEN MIZ_ERROR_TAC "CONSIDER" (map fst ntml); ALL_TAC];;|\\
\medskip
\lineno\verb|let LET = MAP_EVERY X_GEN_TAC;;|\\
\medskip
\lineno\verb|let PER_CASES =|\\
\lineno\verb|  let F = `F` in|\\
\lineno\verb|  fun tac cases ->|\\
\lineno\verb|    let dj = itlist (curry mk_disj) (map (snd o fst) cases) F in|\\
\lineno\verb|    SUBGOAL_THEN dj|\\
\lineno\verb|      (EVERY_TCL (map (fun case -> let n,_ = fst case in|\\
\lineno\verb|        (DISJ_CASES_THEN2 (N_ASSUME_TAC n))) cases) CONTR_TAC) THENL|\\
\lineno\verb|    ([tac] @ map snd cases) THEN MIZ_ERROR_TAC "PER_CASES" [];;|\\
\medskip
\lineno\verb|let TAKE = MAP_EVERY EXISTS_TAC;;|\\
\medskip
\lineno\verb|let THUS_A (n,tm) tac =|\\
\lineno\verb|  SUBGOAL_THEN tm ASSUME_TAC THENL|\\
\lineno\verb|  [tac THEN MIZ_ERROR_TAC "THUS_A" [n]|\\
\lineno\hbox to\hsize{\verb|  ;POP_ASSUM (fun th -> N_ASSUME_TAC n th THEN REWRITE_TAC[EQT_INTRO th])];;|\hss}
\end{flushleft}


\end{document}
