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

\title{Encoding the HOL Light logic in Coq}
\author{Freek Wiedijk}
\institute{\email{freek@cs.kun.nl}\\University of Nijmegen}
\maketitle

\begin{abstract}
We show how to encode the HOL Light logic in Coq.
This makes an automatic translation of HOL proofs to
Coq possible.
The translated HOL proofs refer to translated HOL data types
but those data types can be related to the standard Coq data types,
making the HOL results useful for Coq.
The translated proofs have a size linear in the time HOL takes
to process the original proofs.
However the constant of linearity is large.
The approach described in this paper is similar
%to the method of
%Ewen Denney for translating HOL98 proofs to Coq \cite{den:00} and
to the method of Pavel Naumov, Mark-Oliver Stehr and Jos\'e Mesequer
for translating HOL98 proofs to Nuprl \cite{nau:ste:mes:01}.
\end{abstract}


\section{Introduction}
\subsection{Problem}

There are many systems for proof formalization.
Currently popular systems are
HOL \cite{gor:mel:93}, Coq
\cite{bar:bou:cor:cou:cos:del:rau:fil:gim:her:hue:lau:mun:mur:par:loi:pau:sai:wer:00},
Nuprl \cite{con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86},
Isabelle \cite{pau:94}, ACL2 \cite{kau:man:moo:00} and
PVS \cite{owr:rus:sha:92}.
There are two views on this multitude of systems.
The one view is to expect the best system to take the lead over
the other ones.
The other view is to expect the systems to coexists
and to be able to exchange mathematical results between them.
Often this second view is utopian and presents a future in which
`mathematical services' will be available through the world wide web.
These services will then solve almost all mathematical problems at the click
of a mouse.
Of course for this to become a reality the various system need to
be able to understand each other's mathematics.

There are two reasons why exchanging mathematics between systems
is difficult: a theoretical and a practical reason.
The theoretical reason is that the notions of the various systems
are generally not compatible.
For instance Randy Pollack writes \cite{pol:98}:
\begin{quote}\em
An advantage {\rm [\dots]} is that proofs in the same logic can be shared
by different proof checkers for that logic if a standard syntax can be found
(or mechanical translations believed), because the official proofs don't
depend on the tactics that are particular to individual proof tools.
In current practice this idea is a can of worms, and the phrase `in the
same logic' causes experts in the field to roll on the floor with laughter.
\end{quote}
The practical reason why exchanging mathematics between systems is difficult
is that translation makes things bigger and slower.
The translated mathematics is an order of magnitude worse than
the mathematics done within the system itself (like for instance 100M instead of 1M).
Also mathematics imported from a foreign system will be less readable and
often will not follow the conventions of the system.
So people will not be inclined to use translation.

This paper looks at a specific case of the translation problem.
We investigate a method to move mathematics from the HOL system to Coq.

The incentive to look at this was that in Nijmegen we were interested in
formalizing a proof of the fundamental theorem of calculus in Coq.
The fundamental theorem of calculus is the theorem that states that
integration and differentiation are inverse to each other.
But then it turned out that this theorem had already been proved by John
Harrison in HOL, called theorem \verb|FTC1|.
So we wanted to know whether it would be possible to import this
result from HOL in Coq.

\subsection{Approach}

This paper will model the HOL logic in Coq.
So for every HOL notion we will have a Coq definition.
This means that we build a {\em model\/} of HOL inside the Coq universe.
Therefore when we translate a HOL statement it will become a statement
about this model.
However we have chosen a {\em natural\/} representation for the various
HOL constructions.
This makes it possible to relate the HOL objects to their Coq counterparts.
For instance the HOL type of natural numbers is called \verb|num|.
To this corresponds a Coq type {\tt (hol\_elts hol\_'num)} in the Coq model
of HOL which is different from the Coq type of the natural numbers \verb|nat|.
However {\tt (hol\_elts hol\_'num)} turns out to be isomorphic
to \verb|nat|, so statements about the first type do apply to the second type.

Coq is a constructive system while HOL is classical.
In order to be able to do the HOL constructions we will need to add
two axioms to the Coq logic:
a version of the axiom of choice and an extensionality axiom.

The formalization of the HOL logic in Coq will allow us to translate HOL proofs
to Coq.
This will not be done on the level of the tactics but on the level of the
basic inferences.
So the HOL tactics will {\em not\/} become available to Coq, nor will the Coq
translation resemble the HOL original.

The translation scheme that we present in this paper can be automatized but
we have not implemented this.
Instead we have only translated a sample proof manually.
This showed that the translation of a realistic HOL theorem would become
big, after which we decided not to proceed with an implementation.

\subsection{Related work}

When this paper was almost finished my attention was drawn to the work
of Ewen Denney for translating HOL98 proofs to Coq \cite{den:00} and
to the work of Pavel Naumov, Mark-Oliver Stehr and Jos\'e Mesequer
for translating HOL98 proofs to Nuprl \cite{nau:ste:mes:01}.
The work in this paper is analogous to this but for HOL Light instead of
HOL98.

\subsection{Contribution}

This paper presents three results:
\begin{itemize}
\item It shows how to model the HOL Light logic in the Coq system.
\item It presents a way to translate HOL Light mathematics to Coq.
\item It shows a way to move mathematics between systems
without the translated mathematics becoming `foreign' to the importing
system.
\end{itemize}
This paper is the explanation of a Coq file \verb|holl2coq.v|
that contains the formalization of HOL Light in Coq.
It is available on the web as:
\begin{center}
\verb|http://www.cs.kun.nl/~freek/notes/holl2coq.v|
\end{center}

\subsection{Outline}

This paper has the following structure.
First we present the HOL and Coq systems.
Then we show how to model the HOL logic with Coq.
Applying this we translate a small HOL proof to Coq.
Finally we show that the translated HOL natural numbers are isomorphic
to the Coq natural numbers.


\section{HOL}

The HOL system that we use in this paper is HOL Light by John Harrison
\cite{har:00}.
This is one of the cleanest implementations of HOL \cite{har:95}.
We will now outline the logic of this system.

\subsection{The HOL logic}

The HOL system has three kinds of notions called {\em types\/},
{\em terms\/} and {\em theorems.}

The terms of HOL are the terms of simply typed lambda calculus.
A HOL term either is a variable, a constant, a function application
$$(t\,u)$$ or a lambda abstraction $$\lambda x.t$$
For instance a HOL term might look like
$(f\,\lambda a.(e\,\lambda x.((i\,x)\,a)))$
where $f$, $e$ and $i$ are constants and $a$ and $x$ are variables.
The difference between HOL terms and those of simply typed lambda calculus
is that HOL terms can be polymorphic (in the style of ML).
For instance the constant $=$ has type
$\alpha\to(\alpha\to\verb|bool|)$ where $\alpha$ is a type variable.
This means that $=$ corresponds to a collection of constants $=_A$, one for
every type $A$.

The types of HOL are the types of simply typed lambda calculus.
There are two primitive types:
\begin{center}
\verb|bool|\\
\verb|ind|
\end{center}
The first is the type of the two truth values \verb|T| and \verb|F|.
The second is the type of {\em individuals\/}
(the only thing that is given about this type is that it is infinite).
One can define new types by taking an existing type $A$
and a predicate $P$ on it.
The new type corresponds to the elements $x$ of $A$ that satisfy $P x$,
so it will behave like:
$$\{x:A \mathbin{|} P x\}$$
Apart from these scalar types (the two basic types and the defined types)
the HOL logic has function types:
$$A\to B$$ for all types $A$ and $B$.

The two basic constants of HOL are
the equality predicate and the choice operator:
$$
\begin{array}{rcl}
\mathord{=} &:& \alpha\to(\alpha\to\verb|bool|)\\
\verb|@| &:& (\alpha\to\verb|bool|)\to\alpha
\end{array}
$$
The choice operator selects an object satisfying a predicate.
So $\verb|@|x\!:\!A.\,P x$ is some $x$ of type $A$ that satisfies $P x$
(in the case that one or more such $x$ exist;
if none exist it is some arbitrary $x$ of type $A$).
For every defined type there are two constants
that map the defined type and the type it's carved out of to each other.
Every other constant in the system
(not one of the two basic constants nor one
of a pair of mappings associated to a type definition)
is defined as an abbreviation of a HOL term.

The theorems of HOL are certain sequents of the shape:
$$t_1,\,t_2,\,\ldots,\,t_n \vdash t$$
where $t_1$, \dots, $t_n$ and $t$ are terms of type \verb|bool|.
A theorem is either one of three axioms, a theorem corresponding to
a defined constant (stating its definition),
one of two theorems corresponding to a
defined type (stating that the mappings are inverse to each other)
or it is derived from other theorems by one of ten inference rules.
The three axioms are called:
\begin{center}
\verb|ETA_AX|\\
\verb|SELECT_AX|\\
\verb|INFINITY_AX|
\end{center}
These respectively are an extensionality axiom in the form of the $\eta$
conversion rule, the axiom of choice in terms of the \verb|@| operator and an
infinity axiom for the \verb|ind| type.
The ten inference rules are called \verb|ABS|, \verb|ASSUME|, \verb|BETA|,
\verb|DEDUCT_ANTISYM_RULE|, \verb|EQ_MP|, \verb|INST|, \verb|INST_TYPE|,
\verb|MK_COMB|, \verb|REFL| and \verb|TRANS|.
For the details of the axioms and the inference rules we refer to the
HOL Light documentation \cite{har:00}.

\subsection{The theorems of HOL Light}

The HOL Light system has been implemented in the functional language CAML Light
which is a dialect of ML.
When the HOL Light system starts it processes its basic library.
This takes about ten minutes.%
\footnote{On a system with a performance of about 10 SPECint95.
The fastest current computers are about 50 SPECint95.}
During this time HOL Light generates about 1.5 million objects of the
ML data type \verb|thm|.
This data type corresponds to the theorems of the HOL Light logic
as outlined in the previous subsection.
Many of these \verb|thm|s get garbage collected after a while.
So the memory used by the HOL Light system does not need to have room
for all 1.5 million \verb|thm|s.

In order to get to an advanced theorem more \verb|thm|s have to be generated.
When processing the files \verb|analysis.ml| and \verb|transc.ml|
the system generates another million \verb|thm|s.
The fundamental theorem of calculus is one of the last theorems in
the \verb|transc.ml|.
The \verb|thm| that is the theorem \verb|FTC1| is the 2535069th
\verb|thm| that is generated by HOL Light.

\section{Coq}

The Coq system
\cite{bar:bou:cor:cou:cos:del:rau:fil:gim:her:hue:lau:mun:mur:par:loi:pau:sai:wer:00}
from France is similar to HOL.
Both are implemented in ML and are tactic based proof assistants in LCF-style.
We will not discuss the Coq logic in detail.
We will only focus on the difference in the way that HOL and Coq treat proofs.

\subsection{Coq proofs}

HOL and Coq both generate {\em proof objects\/} for proved statements.
Proof objects are compound objects built from a small number of primitives.
In the case of HOL those primitives are the ten inference rules.
In the case of Coq those are eighteen term building primitives called
\verb|Rel|,
\verb|Var|,
\verb|Meta|,
\verb|Evar|,
\verb|Sort|/\verb|Prop|/\verb|Pos|,
\verb|Sort|/\verb|Prop|/\verb|Null|,
\verb|Sort|/\verb|Type|,
\verb|Cast|,
\verb|Prod|,
\verb|Lambda|,
\verb|LetIn|,
\verb|App|,
\verb|Const|,
\verb|Ind|,
\texttt{Con}\-\texttt{struct},
\verb|Case|,
\verb|Fix| and
\verb|CoFix|.

There are two differences in the way HOL and Coq treat proofs:
\begin{itemize}
\item
HOL's proofs are checkable in {\em linear time}.
This means that the time needed to check the proof is linear
in the size of the proof object.
Every primitive in the proof object only takes a small amount of
time to process.

In contrast with this Coq proof objects can be much smaller than
the time needed to check them.
That is because the system has to verify {\em convertibility\/} of terms
(to be specific: $\beta\delta\iota$-convertibility)
without there being anything in the proof object corresponding to that.
In other words, in the Coq logic `calculation needs no proof'.%
\footnote{This is what Henk Barendregt calls the `Poincar\'e principle' \cite{bar:97}
because Henri Poincar\'e wrote in \cite{poi:02} about showing
the correctness of the calculation $2+2 = 4$:
\begin{quote}
{\em `Ce n'est pas une d\'emonstration proprement dite, {\rm [\dots]}
c'est une v\'erification'.
{\rm [\dots]}
La v\'erification diff\`ere pr\'ecis\'ement de la v\'eritable
d\'emonstration, parce qu'elle est purement analytique et parce qu'elle est
st\'erile.}
\end{quote}}

This means that there is no recursive function that gives
a bound on the `checking time' of a Coq proof object as function of its size.
Some people think that this is an undesirable property for a notion of `proof'.
Other people think that it is desirable because it keeps the size of the proof
object down.

\item
In HOL the parts of a proof object are processed `on the fly' and are not stored in
memory, while in Coq proof objects are stored.
In HOL a theorem is just a statement of which it is known that it has been proved.
In Coq a theorem is a statement together with a {\em proof term}, a term that represents
the proof object.
This is essential to the Coq logic.
Checking Coq proofs without keeping those proof terms is not possible.

\end{itemize}

\subsection{The features of Coq's logic}

HOL is classical and Coq is constructive, so one might expect that
HOL's logic is more complex than Coq's.
In fact it is the other way around.
If one ignores the classical parts then HOL's logic is a subset of Coq's.
Both logics are typed lambda calculi but Coq's logic has many features that
HOL's has not.
The Coq logic contains:
\begin{itemize}
\item full polymorphism (not just ML-style polymorphism)
\item dependent types
\item the distinction between computational and non-computational propositions
\item an infinite hierarchy of type universes
\item inductive and co-inductive types built into the logic
\end{itemize}
Since Coq's logic is more complicated than HOL's
it's not surprising that in this paper we embed HOL in Coq.
The other way around would be much harder.

\subsection{Using Coq as a proof checker}

In this paper we make some claims about Coq's logic
that have only be established by experimenting with the Coq system.
So if there is a bug in Coq then there might be incorrect claims here.

\section{Encoding the HOL logic in Coq}

We will now explain how we encoded the HOL logic in Coq.
We will first present the axioms that we added to Coq
to get classical reasoning.
Then we will show how we encoded HOL's types, terms
and theorems in Coq.

\subsection{The axioms}\label{axioms}

HOL is a classical system and Coq is not.
So we need to add classical axioms to Coq to be able to translate
HOL proofs.
We expected to have to add three axioms to Coq
but it turned out that the first followed from the second.
So we only have to add two axioms.
However we will show all three statements here:

\subsubsection{Classical logic.}

The difference between constructive and classical predicate logic is
the double negation law.
This becomes in Coq:
\begin{quote}
\verb|Lemma double_negation :|\\
\verb|  (A:Prop)~(A->False)->A.|
\end{quote}
We wrote \verb|~(A->False)| instead of \verb|~~A| to make this
an analogue of the next axiom.

\subsubsection{The axiom of choice.}

The HOL logic has a {\em choice operator} \verb|@|.
To model this we want to have an operator in Coq
that selects an element from any non-empty \verb|Set|.
This operator is given by:
\begin{quote}
\verb|Axiom choice :|\\
\verb|  (A:Set)~(A->False)->A.|
\end{quote}
The type \verb|A->False| is inhabited if and only if
\verb|A| is empty so one can read
$$\verb|A->False|$$
as:
$$\mbox{\em the set {\tt A} is empty\/}$$
So this axiom is an operator that takes a proof
that a set is not empty and returns an element of that set.
Which is a choice operator.

This axiom is {\em not\/} what constructivists call the axiom
of choice.
For constructivists the axiom of choice is an operator associating
a function to a relation.
Constructivists probably see the condition of our axiom
as the double negation of the {\em real\/} way to say that
the set is non-empty which is by giving an element.

However the resemblance to a choice operator is striking
which is why we didn't call this the double negation law
for \verb|Set| but the axiom of choice.

\subsubsection{Extensionality.}

The HOL logic is extensional.
If two functions have equal values everywhere then they are equal.
In Coq this becomes:
\begin{quote}
\verb|Axiom extensionality :|\\
\verb|  (A,B:Set; f,g:A->B)((x:A)(f x)=(g x))->f=g.|
\end{quote}
The equality \verb|=| in this axiom is Coq's standard Leibniz
equality.

\subsection{Encoding the types}

A HOL type almost corresponds to a Coq \verb|Set|.
However a HOL type always has to be non-empty while a Coq \verb|Set|
can be empty.
Therefore we can't represent a HOL type by a Coq \verb|Set|.
Instead we define:
\begin{quote}
\verb|Record hol_type : Type :=|\\
\verb|  { hol_elts  :> Set;|\\
\verb|    hol_inhab :  hol_elts|\\
\verb|  }.|
\end{quote}
and let a HOL type be represented by an object of type \verb|hol_type|.
The function \verb|hol_elts| is defined to be a coercion
so it can be omitted and we can write \verb|x:A| instead of
\verb|x:(hol_elts A)|.

There are three kinds of HOL type that we need to define:
basic types, function types and defined types.

\subsubsection{Basic types.}

The two basic HOL types \verb|bool| and \verb|ind| correspond naturally
to the Coq \verb|Set|s \verb|bool| and \verb|nat|:
\begin{quote}
\verb|Definition hol_'bool : hol_type :=|\\
\verb|  (Build_hol_type bool false).|
\medskip\\
\verb|Definition hol_'ind : hol_type :=|\\
\verb|  (Build_hol_type nat O).|
\end{quote}
The HOL type \verb|bool| is for HOL what \verb|Prop| is for Coq.
Hence we need to connect these to each other.
We define:
\begin{quote}
\verb|Definition hol_thm : hol_'bool->Prop :=|\\
\verb|  [p:hol_'bool](if p then True else False).|
\end{quote}
So if \verb|A| is a translation in \verb|hol_'bool| of some HOL
formula then:
$$\verb|(hol_thm A)|$$
is the Coq way of saying that this formula holds. 

\subsubsection{Function types.}

The HOL function types are just the Coq function types:
\begin{quote}
\verb|Definition hol_'fun : hol_type->hol_type->hol_type :=|\\
\verb|  [A,B:hol_type](Build_hol_type A->B [x:A](hol_inhab B)).|
\end{quote}
Note that in this definition
\verb|A->B| really means {\tt (hol\_elts A)->(hol\_elts B)}.
So we have that:
$$\verb|(hol_elts (hol_'fun A B))| = \verb|(hol_elts A)->(hol_elts B)|$$
Although we use an abstract representation \verb|hol_type| for the
HOL types,
if we apply \verb|hol_elts| we get the \verb|Set|s that naturally
corresponds to them.

\subsubsection{Type definitions.}

Finally there are the defined HOL types,
which are carved out of an already existing type by a predicate on that type.
Modeling these in Coq turned out to be more difficult than expected.

Naively one would expect that we could represent the defined types by a $\Sigma$ type.
If \verb|A| is some HOL type and \verb|P:A->Prop|
is some HOL predicate on it then:
$$\Sigma x\!:\!A.\,P x$$
which in Coq syntax is:
$$\verb|(sig A P)|$$
seems to represent the set of elements in \verb|A| that satisfy \verb|P|.
However this approach doesn't work because
the proposition type \verb|(P x)| can have many different inhabitants.
This means that for each \verb|x:A| there will be many elements in \verb|(sig A P)|.
Which is wrong.

The way to solve this is to use the \verb|Set| variant of the
$\Sigma$ type construction (which in Coq is called \verb|sigS|).
If a proposition is true (we can decide that because we have the
classical axioms) we associate a \verb|Set| with one element with it.
That way we can define a `clone' of \verb|sig| called \verb|sig'| that
behaves classically:
\begin{quote}
\verb|Definition irrelevant : Prop->Set :=|\\
\verb|  [A:Prop]|\\
\verb|    Cases (excluded_middle A) of|\\
\verb|      (left _) => unit|\\
\verb/    | (right _) => Empty_set/\\
\verb|    end.|
\medskip\\
\verb|Definition sig' : (A:Set)(A->Prop)->Set :=|\\
\verb|  [A:Set; P:A->Prop](sigS A [x:A](irrelevant (P x))).|
\end{quote}
Using this we can now give the Coq version of the HOL type definitions:
\begin{quote}
\verb|Definition hol_typedef :=|\\
\verb|  [A:hol_type; P:(hol_'fun A hol_'bool);|\\
\verb|      i:A; H:(hol_thm (P i))]|\\
\verb|    (Build_hol_type (sig' A (Hol_thm' P)) (exist' ?? i H)).|
\end{quote}
Here \verb|Hol_thm'| maps HOL predicates of type
{\tt (hol\_'fun A hol\_'bool)} to Coq predicates of type
\verb|A->Prop|.
It is defined such that {\tt (Hol\_thm' P x)} is the same as
{\tt (hol\_thm (P x))}.
The element \verb|i:A| is needed to show that the defined type is non-empty.
It is needed in the HOL version of a HOL type definition as well.

\subsection{Encoding the terms}

HOL terms straightforwardly translate to Coq terms.
For an example, the HOL term corresponding to:
$$(f\,\lambda a.(e\,\lambda x.((i\,x)\,a)))$$
which in HOL syntax is:
$$\verb|f \a. e \x. i x a|$$
becomes:
$$\verb|(hol'f (Hol_Abs [a:A](hol'e (Hol_Abs [x:A](hol'i x a)))))|$$
Here \verb|A| is the \verb|hol_type| of the variables \verb|a| and \verb|x|.
We prefix the HOL names with `\verb|hol'|' to indicate that they are
translations of HOL constants.

There are two elements in this translation that needs to be explained:
how abstraction is handled and how constants are modeled.

\subsubsection{Abstraction.}

As will be clear from the example,
function application in HOL translates to function application in Coq.
However for abstraction we have a typing problem.
The HOL functions have to have type \verb|(hol_'fun A B)|
but Coq abstraction has type \verb|A->B|.
To solve this we have the \verb|Hol_Abs| function:
\begin{quote}
\verb|Definition hol_Abs :|\\
\verb|  (A,B:hol_type)(A->B)->(hol_'fun A B) :=|\\
\verb|    [A,B:hol_type; f:A->B]f.|
\medskip\\
\verb|Syntactic Definition Hol_Abs := (hol_Abs ??).|
\end{quote}
This \verb|Hol_Abs| doesn't do anything
apart from changing the type from:
$$\verb|A->B|$$
to the equivalent: 
$$\verb|(hol_elts (hol_'fun A B))|$$
Although these are $\beta\delta\iota$-convertible,
Coq isn't smart enough to figure this type conversion out by itself.
If we remove the \verb|Hol_Abs| functions we get typing errors.

\subsubsection{Equality.}

The first basic HOL constant is equality.
We model it by making it correspond to the usual equality in Coq
which is the Leibniz equality \verb|=|.

However the Coq equality is in \verb|Prop|
while HOL predicates need to be in \verb|hol_'bool|.
Therefore we need to map \verb|Prop| to \verb|hol_'bool|
(an inverse to the \verb|hol_thm| function):
\begin{quote}
\verb|Definition hol_value : Prop->hol_'bool :=|\\
\verb|  [A:Prop]|\\
\verb|    Cases (excluded_middle A) of|\\
\verb|      (left _) => true|\\
\verb/    | (right _) => false/\\
\verb|    end.|
\end{quote}
Using this the definition of the HOL equality \verb|hol''eq| becomes
straightforward:
\begin{quote}
\verb|Definition hol''eq :|\\
\verb|  (A:hol_type)(hol_'fun A (hol_'fun A hol_'bool)) :=|\\
\verb|    [A:hol_type](Hol_Abs [x:A](Hol_Abs [y:A]|\\
\verb|      (hol_value x=y))).|
\medskip\\
\verb|Syntactic Definition Hol''eq := (hol''eq ?).|
\end{quote}
The HOL type of the HOL constant \verb|(=)| is the polymorphic:
$$\verb|A->(A->bool)|$$
As can be seen from the definition this corresponds in Coq to:
$$\verb|(A:hol_type)(hol_'fun A (hol_'fun A hol_'bool))|$$

\subsubsection{The choice operator.}

The other basic HOL constant is the choice operator.
Its definition is straightforward too:
\begin{quote}
\verb|Definition hol''select :|\\
\verb|  (A:hol_type)(hol_'fun (hol_'fun A hol_'bool) A) :=|\\
\verb|    [A:hol_type](Hol_Abs [P:(hol_'fun A hol_'bool)]|\\
\verb/      Cases (inhabited {x:A | (hol_thm (P x))}) of/\\
\verb|        (inl x) => (proj1_sig ?? x)|\\
\verb/      | (inr _) => (hol_inhab A)/\\
\verb|      end).|
\medskip\\
\verb|Syntactic Definition Hol''select := (hol''select ?).|
\end{quote}
The \verb|inhabited| function is defined using the \verb|choice| axiom
and decides whether a \verb|Set| is inhabited or not.
It is the \verb|Set| equivalent of the law of the excluded middle.

\subsubsection{Mapping defined types.}

Every HOL type definition produces two constants that map the
defined type (the {\em abstract\/} type) to the type it is carved
out of (the {\em representing\/} type) and back.
The Coq equivalents of these constants are given by functions:
\begin{quote}
\verb|hol_typedef_abs :|\\
\verb|  (A:hol_type; P:(hol_'fun A hol_'bool);|\\
\verb|    i:A; H:(hol_thm (P i)))|\\
\verb|      A->(hol_typedef A P i H)|
\end{quote}
and
\begin{quote}
\verb|hol_typedef_rep :|\\
\verb|  (A:hol_type; P:(hol_'fun A hol_'bool);|\\
\verb|    i:A; H:(hol_thm (P i)))|\\
\verb|      (hol_typedef A P i H)->A|
\end{quote}
Their definition is straightforward.
The only subtlety is that \verb|hol_typedef_abs| returns the constant \verb|i|
in the case that the element doesn't satisfy \verb|P|.

\subsubsection{Defined constants.}

All other HOL constants are just abbreviations of HOL terms.
These straightforwardly translate to Coq \verb|Definition|s.
The only subtlety is that type variables need to be given explicitly
as arguments.

As an example consider the HOL universal quantifier \verb|(!)|.
It is defined by:
$$\verb|(!) = \P:A->bool. P = \x. T|$$
This becomes in Coq:
\begin{quote}
\verb|Definition hol''forall :|\\
\verb|  (A:hol_type)|\\
\verb|    (hol_'fun (hol_'fun A hol_'bool) hol_'bool) :=|\\
\verb|      [A:hol_type](Hol_Abs [P:(hol_'fun A hol_'bool)]|\\
\verb|        (Hol''eq P (Hol_Abs [x:A]hol'T))).|
\medskip\\
\verb|Syntactic Definition Hol''forall := (hol''forall ?).|
\end{quote}
In this kind of translated definitions
we use the \verb|Syntactic| \verb|Definition|s to establish the
type variables.
So we write \verb|(Hol''eq |\dots\verb|)| instead of
\verb|(hol''eq A |\dots\verb|)|.
This is similar to doing ML style type inference.
Sometimes it does not work.
In that case the type variable arguments need to be given explicitly.

\subsection{Encoding the theorems}

To conclude our description of the Coq implementation of the HOL logic
we show how HOL theorems are modeled in Coq.
A HOL theorem:
$$t_1,\,t_2,\,\ldots,\,t_n \vdash t$$
becomes a Coq \verb|Prop|:
$${\cal Q}\,\verb|(hol_thm |t_1\verb|)->(hol_thm |t_2\verb|)->|\ldots\verb|(hol_thm |t_n\verb|)->(hol_thm |t\verb|)|$$
where ${\cal Q}$ quantifies over the type variables and term variables
in the theorem.

For instance the HOL theorem:
$$\verb/x = y |- y = x/$$
(where \verb|x| and \verb|y| have type \verb|A|) becomes the Coq \verb|Prop|:
$$\begin{array}{l}
\verb|(A:hol_type; x,y:A)|\\
\verb|  (hol_thm (Hol''eq x y))->(hol_thm (Hol''eq y x))|
\end{array}$$

\subsubsection{Inference rules.}

We now show how the ten HOL basic inference rules are implemented.
Those rules operate on HOL theorems with a list of assumptions
before the $\vdash$.
But the Coq representation of theorems is {\em implicit\/}
in the sense that there
is not a Coq data type representing the HOL theorems.
Therefore the assumptions are not present in the Coq representations
of the HOL inference rules and have to be manipulated outside those rules.

For instance the \verb|DEDUCT_ANTISYM_RULE| rule is:
$${\Gamma\vdash p \quad \Delta\vdash q \over
\left(\Gamma-\{q\}\right)\cup\left(\Delta-\{p\}\right)\vdash p=q}
\;\mbox{\footnotesize{\tt DEDUCT\_ANTISYM\_RULE}}
$$
The Coq implementation ignores the $\left(\Gamma-\{q\}\right)\cup\left(\Delta-\{p\}\right)$
assumptions.
It is:
\begin{quote}
\verb|hol_DEDUCT_ANTISYM_RULE : (p,q:hol_'bool)|\\
\verb|  ((hol_thm q)->(hol_thm p))->|\\
\verb|  ((hol_thm p)->(hol_thm q))->|\\
\verb|    (hol_thm (Hol''eq p q))|
\end{quote}
This says that logical equivalence implies equality of the truth values.

The \verb|ASSUME| rule which deals with assumptions and
the \verb|INST| and \verb|INST_TYPE| rules which are about substitution
don't have a Coq counterpart.
The other rules become:
\begin{quote}
\verb|hol_REFL : (A:hol_type; x:A)(hol_thm (Hol''eq x x))|
\medskip\\
\verb|hol_TRANS : (A:hol_type; x,y,z:A)|\\
\verb|  (hol_thm (Hol''eq x y))->|\\
\verb|  (hol_thm (Hol''eq y z))->|\\
\verb|    (hol_thm (Hol''eq x z))|
\medskip\\
\verb|hol_MK_COMB : (A,B:hol_type; f,g:(hol_'fun A B); x,y:A)|\\
\verb|  (hol_thm (Hol''eq f g))->(hol_thm (Hol''eq x y))->|\\
\verb|    (hol_thm (Hol''eq (f x) (g y)))|
\medskip\\
\verb|hol_ABS : (A,B:hol_type; f,g:A->B)|\\
\verb|  ((x:A)(hol_thm (Hol''eq (f x) (g x))))->|\\
\verb|    (hol_thm (Hol''eq (Hol_Abs f) (Hol_Abs g)))|
\medskip\\
\verb|hol_BETA : (A,B:hol_type; f:A->B; x:A)|\\
\verb|  (hol_thm (Hol''eq (Hol_Abs f x) (f x)))|
\medskip\\
\verb|hol_EQ_MP : (p,q:hol_'bool)|\\
\verb|  (hol_thm (Hol''eq p q))->(hol_thm p)->(hol_thm q)|
\end{quote}
(The \verb|hol_BETA| rule is almost the same as the \verb|hol_REFL| rule
because Coq does the $\beta$-reduction.)

Note that all these rules are about HOL equality.

\subsubsection{The axioms and the theorems for type and constant definitions.}
The theorems that are not derived using one of the inference rules
all translate in a straightforward way to Coq and can be proved easily.
The Coq functions are for the axioms:
\begin{quote}
\verb|hol_ETA_AX : (A,B:hol_type)(hol_thm|\\
\verb|  (Hol''forall (Hol_Abs [t:(hol_'fun A B)]|\\
\verb|    (Hol''eq (Hol_Abs [x:A](t x)) t))))|
\medskip\\
\verb|hol_SELECT_AX : (A:hol_type)(hol_thm|\\
\verb|  (Hol''forall (Hol_Abs [P:(hol_'fun A hol_'bool)]|\\
\verb|    (Hol''forall (Hol_Abs [x:A]|\\
\verb|      (hol''imp (P x) (P (Hol''select P))))))))|
\medskip\\
\verb|hol_INFINITY_AX : (hol_thm|\\
\verb|  (Hol''exists (Hol_Abs [f:(hol_'fun hol_'ind hol_'ind)]|\\
\verb|    (hol''and (Hol'ONE_ONE f) (hol''not (Hol'ONTO f))))))|
\end{quote}
and for the theorems about the mappings from and to defined types:
\begin{quote}
\verb|hol_typedef_absrep :|\\
\verb|  (A:hol_type; P:(hol_'fun A hol_'bool);|\\
\verb|    i:A; H:(hol_thm (P i)); a:(hol_typedef A P i H))|\\
\verb|      (hol_thm (Hol''eq (Hol_typedef_abs|\\
\verb|                          (Hol_typedef_rep a)) a))|
\medskip\\
\verb|hol_typedef_repabs :|\\
\verb|  (A:hol_type; P:(hol_'fun A hol_'bool);|\\
\verb|    i:A; H:(hol_thm (P i)); r:A)|\\
\verb|      (hol_thm (Hol''eq|\\
\verb|        (P r)|\\
\verb|        (Hol''eq (Hol_typedef_rep|\\
\verb|                   (hol_typedef_abs A P i H r)) r)))|
\end{quote}
The theorem for the constant definitions is \verb|hol_REFL| applying
the $\delta$-reduction of Coq.

\section{Translating a HOL proof to Coq}\label{translation}

We manually translated a small HOL proof to Coq to see whether the formalization
of the HOL logic in Coq was adequate.
For this we looked in the basic HOL Light library for a proof that was shorter
than 40 basic
inference steps and that contained all inference step types.
We could not find such a proof but we found a proof of 32 steps that contained
all step types but \verb|ASSUME|.

This is that proof:
\begin{quote}
\verb|let EXISTS_REFL = PROVE|\\
\verb| (`!a:A. ?x. x = a`,|\\
\verb|  GEN_TAC THEN EXISTS_TAC `a:A` THEN REFL_TAC);;|
\end{quote}
It is the HOL equivalent of the Coq proof:
\begin{quote}
\verb|Lemma EXISTS_REFL : (A:Set; a:A)(Ex [x:A]x=a).|\\
\verb|Proof.|\\
\verb|Intros. Exists a. Reflexivity.|\\
\verb|Qed.|
\end{quote}
So it is a proof of:
$$\forall a.\,\exists x.\,x = a$$
The 4 \verb|thm|s that are referred to from this proof are:
\begin{center}
\footnotesize
\setlength\tabcolsep{3pt}
\begin{tabular}{rlrl}
17 & \verb/|- t = t = T/ &&\\
171 & \verb/p ==> q, p |- q/ &&\\
248 & \verb/|- (P = (\x. T)) ==> (!) P/ &&\\
313 & \verb/|- P x ==> (?) P/ &&
\end{tabular}
\end{center}
In this we numbered the \verb|thm|s that HOL Light generates.
The HOL Light kernel doesn't have names for \verb|thm|s.
Only outside the HOL Light kernel ML names are given to \verb|thm|s.

The proof of \verb|EXISTS_REFL| consists of \verb|thm|s numbered 18749 until 18780:
\begin{center}
\footnotesize
\setlength\tabcolsep{3pt}
\begin{tabular}{rlrl}
18749 & \verb/|- a = a/ & \verb|REFL| & \\
18750 & \verb/|- (\x. x = a) x = x = a/ & \verb|BETA| & \\ 
18751 & \verb/|- (\x. x = a) a = a = a/ & \verb|INST| & 18750\\ 
18752 & \verb/|- P x ==> (?) P/ & \verb|INST_TYPE| & 313\\
18753 & \verb/|- (\x. x = a) a ==> (?x. x = a)/ & \verb|INST| & 18752\\
18754 & \verb/|- (\x. x = a) a = (\x. x = a) a/ & \verb|REFL| & \\ 
18755 & \verb/|- (=) = (=)/ & \verb|REFL| & \\ 
18756 & \verb/|- (=) ((\x. x = a) a) = (=) (a = a)/ & \verb|MK_COMB| & 18755 18751\\ 
18757 & \verb/|- ((\x. x = a) a = (\x. x = a) a) =/ & \verb|MK_COMB| & 18756 18754\\
& \verb/     (a = a) = (\x. x = a) a/ &&\\
18758 & \verb/|- (a = a) = (\x. x = a) a/ & \verb|EQ_MP| & 18757 18754\\
18759 & \verb/|- (\x. x = a) a/ & \verb|EQ_MP| & 18758 18749\\
18760 & \verb/(\x. x = a) a ==> (?x. x = a),/ & \verb|INST| & 171\\
& \verb/(\x. x = a) a/ &&\\
& \verb/|- ?x. x = a/ &&\\
18761 & \verb/(\x. x = a) a/ & \verb|DEDUCT|$\,$\ldots & 18753 18760\\
& \verb/|- (\x. x = a) a ==> (?x. x = a) =/ &&\\
& \verb/     (?x. x = a)/ &&\\
18762 & \verb/(\x. x = a) a/ & \verb|EQ_MP| & 18761 18753\\
& \verb/|- ?x. x = a/ &&\\
18763 & \verb/|- (\x. x = a) a = (?x. x = a)/ & \verb|DEDUCT|$\,$\ldots & 18759 18762\\ 
18764 & \verb/|- ?x. x = a/ & \verb|EQ_MP| & 18763 18759\\
18765 & \verb/|- (?x. x = a) = (?x. x = a) = T/ & \verb|INST| & 17\\
18766 & \verb/|- (?x. x = a) = T/ & \verb|EQ_MP| & 18765 18764\\
18767 & \verb/|- (\a. ?x. x = a) = (\a. T)/ & \verb|ABS| & 18766\\
18768 & \verb/|- (P = (\x. T)) ==> (!) P/ & \verb|INST_TYPE| & 248\\
18769 & \verb/|- ((\a. ?x. x = a) = (\x. T)) ==>/ & \verb|INST| & 18768\\
& \verb/     (!a. ?x. x = a)/ &&\\
18770 & \verb/((\a. ?x. x = a) = (\x. T)) ==>/ & \verb|INST| & 171\\
& \verb/  (!a. ?x. x = a),/ &&\\
& \verb/(\a. ?x. x = a) = (\x. T)/ &&\\
& \verb/|- !a. ?x. x = a/ &&\\
18771 & \verb/(\a. ?x. x = a) = (\x. T)/ & \verb|DEDUCT|$\,$\ldots & 18769 18770\\
& \verb/|- ((\a. ?x. x = a) = (\x. T)) ==>/ &&\\
& \verb/     (!a. ?x. x = a) = (!a. ?x. x = a)/ &&
\end{tabular}
\end{center}
\vfill\break
\begin{center}
\footnotesize
\setlength\tabcolsep{3pt}
\begin{tabular}{rlrl}
18772 & \verb/(\a. ?x. x = a) = (\x. T)/ & \verb|EQ_MP| & 18771 18769\\
& \verb/|- !a. ?x. x = a/ &&\\
18773 & \verb/|- ((\a. ?x. x = a) = (\a. T)) =/ & \verb|DEDUCT|$\,$\ldots & 18767 18772\\
& \verb/     (!a. ?x. x = a)/ &&\\
18774 & \verb/|- !a. ?x. x = a/ & \verb|EQ_MP| & 18773 18767\\
18775 & \verb/|- (\a. ?x. x = a) = (\a. ?x. x = a)/ & \verb|REFL| & \\
18776 & \verb/|- (\a. ?x. x = a) = (\a. ?x. x = a)/ & \verb|REFL| & \\
18777 & \verb/|- (\a. ?x. x = a) = (\a. ?x. x = a)/ & \verb|TRANS| & 18776 18775\\
18778 & \verb/|- (!) = (!)/ & \verb|REFL| & \\
18779 & \verb/|- (!a. ?x. x = a) = (!a. ?x. x = a)/ & \verb|MK_COMB| & 18778 18777\\
18780 & \verb/|- !a. ?x. x = a/ & \verb|EQ_MP| & 18779 18774
\end{tabular}
\end{center}
This derivation is not optimal.
For instance it contains the final \verb|thm| already as \verb|thm| number 18774.
Also \verb|thm|s 18775 until 18777 are all the same.

The Coq translation of these steps is simple.
It is for each step an application of the appropriate function:
\begin{quote}\footnotesize
\verb|Definition hol__18749 := [A:hol_type; a:A]|\\
\verb|  (Hol_REFL a).|
\medskip\\
\verb|Definition hol__18750 := [A:hol_type; x,a:A]|\\
\verb|  (Hol_BETA [x:A](Hol''eq x a) x).|
\medskip\\
\verb|Definition hol__18751 := [A:hol_type; a:A]|\\
\verb|  (hol__18750 ? a a).|
\medskip\\
\verb|Definition hol__18752 :=|\\
\verb|    [A:hol_type; x:A; P:(hol_'fun A hol_'bool)]|\\
\verb|  (hol__313 ? x P).|
\medskip\\
\verb|Definition hol__18753 := [A:hol_type; a:A]|\\
\verb|  (hol__18752 ? a (Hol_Abs [x:A](Hol''eq x a))).|
\medskip\\
\verb|Definition hol__18754 := [A:hol_type; a:A]|\\
\verb|  (Hol_REFL (Hol_Abs [x:A](Hol''eq x a) a)).|
\medskip\\
\verb|Definition hol__18755 := [A:hol_type]|\\
\verb|  (Hol_REFL (hol''eq A)).|
\medskip\\
\verb|Definition hol__18756 := [A:hol_type; a:A]|\\
\verb|  (Hol_MK_COMB (hol__18755 ?) (hol__18751 ? a)).|
\medskip\\
\verb|Definition hol__18757 := [A:hol_type; a:A]|\\
\verb|  (Hol_MK_COMB (hol__18756 ? a) (hol__18754 ? a)).|
\medskip\\
\verb|Definition hol__18758 := [A:hol_type; a:A]|\\
\verb|  (Hol_EQ_MP (hol__18757 ? a) (hol__18754 ? a)).|
\medskip\\
\verb|Definition hol__18759 := [A:hol_type; a:A]|\\
\verb|  (Hol_EQ_MP (hol__18758 ? a) (hol__18749 ? a)).|
\medskip\\
\verb|Definition hol__18760 := [A:hol_type; a:A]|\\
\verb|  (hol__171 (Hol_Abs [x:A](Hol''eq x a) a)|\\
\verb|    (Hol''exists (Hol_Abs [x:A](Hol''eq x a)))).|
\medskip\\
\verb|Definition hol__18761 := [A:hol_type; a:A; H0:?]|\\
\verb|  (Hol_DEDUCT_ANTISYM_RULE [H:?](hol__18753 ? a)|\\
\verb|    [H:?](hol__18760 ? a H0 H)).|
\medskip\\
\verb|Definition hol__18762 := [A:hol_type; a:A; H0:?]|\\
\verb|  (Hol_EQ_MP (hol__18761 ? a H0) (hol__18753 ? a)).|
\medskip\\
\verb|Definition hol__18763 := [A:hol_type; a:A]|\\
\verb|  (Hol_DEDUCT_ANTISYM_RULE [H:?](hol__18759 ? a)|\\
\verb|    [H:?](hol__18762 ? a H)).|
\medskip\\
\verb|Definition hol__18764 := [A:hol_type; a:A]|\\
\verb|  (Hol_EQ_MP (hol__18763 ? a) (hol__18759 ? a)).|
\medskip\\
\verb|Definition hol__18765 := [A:hol_type; a:A]|\\
\verb|  (hol__17 (Hol''exists (Hol_Abs [x:A](Hol''eq x a)))).|
\medskip\\
\verb|Definition hol__18766 := [A:hol_type; a:A]|\\
\verb|  (Hol_EQ_MP (hol__18765 ? a) (hol__18764 ? a)).|
\medskip\\
\verb|Definition hol__18767 := [A:hol_type]|\\
\verb|  (Hol_ABS [x:A](hol__18766 ? x)).|
\medskip\\
\verb|Definition hol__18768 := [A:hol_type; P:(hol_'fun A hol_'bool)]|\\
\verb|  (hol__248 ? P).|
\medskip\\
\verb|Definition hol__18769 := [A:hol_type]|\\
\verb|  (hol__18768 ? (Hol_Abs [a:A](Hol''exists (Hol_Abs [x:A]|\\
\verb|    (Hol''eq x a))))).|
\medskip\\
\verb|Definition hol__18770 := [A:hol_type]|\\
\verb|  (hol__171 (Hol''eq (Hol_Abs [a:A](Hol''exists (Hol_Abs [x:A]|\\
\verb|      (Hol''eq x a)))) (Hol_Abs [x:A]hol'T))|\\
\verb|    (Hol''forall (Hol_Abs [a:A](Hol''exists (Hol_Abs [x:A]|\\
\verb|      (Hol''eq x a)))))).|
\medskip\\
\verb|Definition hol__18771 := [A:hol_type; H0:?]|\\
\verb|  (Hol_DEDUCT_ANTISYM_RULE [H:?](hol__18769 A)|\\
\verb|    [H:?](hol__18770 ? H0 H)).|
\medskip\\
\verb|Definition hol__18772 := [A:hol_type; H0:?]|\\
\verb|  (Hol_EQ_MP (hol__18771 ? H0) (hol__18769 A)).|
\medskip\\
\verb|Definition hol__18773 := [A:hol_type]|\\
\verb|  (Hol_DEDUCT_ANTISYM_RULE [H:?](hol__18767 A)|\\
\verb|    [H:?](hol__18772 ? H)).|
\medskip\\
\verb|Definition hol__18774 := [A:hol_type]|\\
\verb|  (Hol_EQ_MP (hol__18773 A) (hol__18767 ?)).|
\medskip\\
\verb|Definition hol__18775 := [A:hol_type]|\\
\verb|  (Hol_REFL (Hol_Abs [a:A](Hol''exists (Hol_Abs [x:A]|\\
\verb|    (Hol''eq x a))))).|
\medskip\\
\verb|Definition hol__18776 := [A:hol_type]|\\
\verb|  (Hol_REFL (Hol_Abs [a:A](Hol''exists (Hol_Abs [x:A]|\\
\verb|    (Hol''eq x a))))).|
\medskip\\
\verb|Definition hol__18777 := [A:hol_type]|\\
\verb|  (Hol_TRANS (hol__18776 A) (hol__18775 ?)).|
\medskip\\
\verb|Definition hol__18778 := [A:hol_type]|\\
\verb|  (Hol_REFL (hol''forall A)).|
\medskip\\
\verb|Definition hol__18779 := [A:hol_type]|\\
\verb|  (Hol_MK_COMB (hol__18778 A) (hol__18777 ?)).|
\medskip\\
\verb|Definition hol__18780 := [A:hol_type]|\\
\verb|  (Hol_EQ_MP (hol__18779 A) (hol__18774 ?)).|
\end{quote}
These Coq statements take approximately 100 bytes Coq source code per HOL step.
So to represent the 1.5 million steps from the basic HOL Light library
in this way would take a Coq file of about 150M.

If we check the type of \verb|hol__18780| it indeed is the \verb|Prop| that corresponds
to \verb|EXISTS_REFL|:
\begin{quote}\footnotesize
\verb|Coq < Check hol__18780.|\\*
\verb|hol__18780|\\*
\verb|     : (A:hol_type)|\\*
\verb|        (hol_thm|\\
\verb|          (hol''forall A|\\
\verb|            (hol_Abs A hol_'bool|\\
\verb|              [a:(A)]|\\
\verb|               (hol''exists A|\\
\verb|                 (hol_Abs A hol_'bool [x:(A)](hol''eq A x a))))))|
\end{quote}

\section{Encoded HOL data types versus Coq data types}

We can translate HOL theorems about the HOL type \verb|num| to Coq.
These translations will be about the Coq type {\tt (hol\_elts (hol\_'num))}.
However the Coq type for the natural numbers is the
Coq type \verb|nat|.
We will now show that how to define an isomorphism between
{\tt (hol\_elts (hol\_'num))} and \verb|nat|.

It is straightforward to define a function \verb|num_of_nat|:
\begin{quote}
\verb|Fixpoint num_of_nat [n:nat] : hol_'num :=|\\
\verb|  Cases n of|\\
\verb|    O => hol'_0|\\
\verb/  | (S m) => (hol'SUC (num_of_nat m))/\\
\verb|  end.|
\end{quote}
We show that this function is a surjection by proving:
\begin{quote}
\verb|nat_of_num_exists :|\\
\verb|  (n:hol_'num)(Ex [m:nat](num_of_nat m)=n)|
\end{quote}
with induction on the Coq version of \verb|num| using the translation of the HOL induction
principle \verb|num_INDUCTION|:
\begin{quote}
\verb^|- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)^
\end{quote}
We use \verb|nat_num_exists| to define
an inverse
\begin{quote}\
\verb|nat_of_num : hol_'num->nat|
\end{quote}
satisfying:
\begin{quote}
\verb|num_of_nat_of_num :|\\
\verb|  (n:hol_'num)(num_of_nat (nat_of_num n))=n|
\end{quote}
Then using the translations of HOL's theorems \verb|NOT_SUC| and \verb|SUC_INJ|:
\begin{quote}
\verb/|- !n. ~(SUC n = 0)/\\
\verb/|- !m n. (SUC m = SUC n) = (m = n)/
\end{quote}
it follows that this function is injective:
\begin{quote}
\verb|num_of_nat_injective :|\\
\verb|  (m,n:nat)(num_of_nat m)=(num_of_nat n)->m=n|
\end{quote}
From that we derive that \verb|nat_of_num| is the inverse to \verb|num_of_nat|.

These bijections commute with the corresponding versions of the
various functions on the natural numbers.
For instance it commutes with the addition functions
\verb|hol''add| and \verb|plus|.
We prove:
\begin{quote}
\verb|plus_add : (m,n:nat)|\\
\verb|  (num_of_nat (plus m n))=|\\
\verb|    (hol''add (num_of_nat m) (num_of_nat n))|
\medskip\\
\verb|add_plus : (m,n:hol_'num)|\\
\verb|  (nat_of_num (hol''add m n))=|\\
\verb|    (plus (nat_of_num m) (nat_of_num n))|
\end{quote}

\section{Conclusion}
\subsection{Discussion}

This paper shows:
\begin{itemize}
\item
It is straightforward to formalize the HOL Light semantics in Coq.
This can be used as the basis of a proof converter
that has the property that the converted HOL data types are isomorphic
to their natural Coq counterparts.

\item
The conversion of the basic HOL Light library will take about 150M of
Coq source code.
This means that the approach from this paper will not give an efficient
way to move mathematics from HOL to Coq.

\end{itemize}
The first is surprisingly nice but the second is discouraging.

\subsection{Future work}

There are several things that can be done to continue the
work in this paper:
\begin{itemize}
\item
The classical axioms from section \ref{axioms}:
\medskip
\begin{quote}
\verb|Axiom choice : (A:Set)~(A->False)->A.|
\medskip\\
\verb|Axiom extensionality :|\\
\verb|  (A,B:Set; f,g:A->B)((x:A)(f x)=(g x))->f=g.|
\end{quote}
\medskip
are not consistent
with the Coq logic (the `Calculus of Inductive Constructions').
It might be interesting to see whether the Coq people can be convinced
to make their logic consistent with these axioms by removing the
impredicativity of \verb|Set|.

\item
We didn't automate the translation from HOL to Coq as outlined in
section \ref{translation}.
It might be interesting to do this and
investigate the performance difference between checking the basic
HOL Light library in HOL Light
and checking its translation in Coq.

\item
It might be interesting to restrict the translation to just translating the
statements and omitting the proofs.
That would be analogous to the approach of \cite{how:96}.
In such a way importing HOL Light mathematics in Coq might become realistic.

\item
We related the natural numbers of the two systems.
It might be interesting to relate the counterparts of other data types.

\item
It might be interesting to work out a systematic way to prove the Coq analogue
of a HOL Light statement from its direct translation.
For instance the direct translation of HOL's theorem \verb|ADD_SYM|:
\medskip
\begin{quote}
\verb/|- !m n. m + n = n + m/
\end{quote}
\medskip
is:
\medskip
\begin{quote}
\verb|(hol_thm (Hol''forall (Hol_Abs [m:hol_'num]|\\
\verb|    (Hol''forall (Hol_Abs [n:hol_'num]|\\
\verb|      (Hol''eq (hol''add m n) (hol''add n m)))))))|
\end{quote}
\medskip
However this is not meaningful to a Coq user.
A Coq user wants to see:
\medskip
\begin{quote}
\verb|(m,n:nat)(plus m n)=(plus n m)|
\end{quote}
\medskip
This paper shows that it is possible to derive this from the previous statement.
But it does not give a systematic description
of what the structure of this kind of transformation is.

\end{itemize}

\subsection{Acknowledgments}

Thanks to Herman Geuvers and John Harrison for helpful discussions.
Thanks to John Harrison for drawing my attention to \cite{den:00}
and \cite{nau:ste:mes:01}.

%\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, Samuel Boutin, Cristina Cornes, Judica{\"e}l Courant, Yann
  Coscoy, David Delahaye, Daniel de~Rauglaudre, Jean-Christophe Filli\^atre,
  Eduardo Gi\-m\'enez, Hugo Herbelin, G\'erard Huet, Henri Laulh\`ere, C\'esar
  Mu{\~n}oz, Chetan Murthy, Catherine Parent-Virouroux, Patrick Loiseleur,
  Christine Paulin-Mohring, Amokrane Sa{\"\i}bi, and Benjamin Werner.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2000.
\newblock \hfill\break URL: \verb|<ftp://ftp.inria.fr/|
  \hfill\break\hbox{}\hfill
  \verb|INRIA/coq/V6.3.1/doc/Reference-Manual-all.ps.gz>|.

\bibitem{con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86}
Robert~L. Constable, Stuart~F. Allen, H.M. Bromley, W.R. Cleaveland, J.F.
  Cremer, R.W. Harper, Douglas~J. Howe, T.B. Knoblock, N.P. Mendler,
  P.~Panangaden, James~T. Sasaki, and Scott~F. Smith.
\newblock {\em Implementing Mathematics with the {N}uprl Development System}.
\newblock Prentice-Hall, NJ, 1986.

\bibitem{den:00}
Ewen Denney.
\newblock {A Prototype Proof Translator from HOl to Coq}.
\newblock In Mark Aagaard and John Harrison, editors, {\em Theorem Proving in
  Higher Order Logics, TPHOLs 2000, Portland}, pages 108--125, Berlin, 2000.
  Springer-Verlag.

\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{har:95}
John Harrison.
\newblock {HOL Done Right}.
\newblock \hfill\break URL:
  \verb|<http://www.cl.cam.ac.uk/users/jrh/papers/holright.ps.gz>|, 1995.

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

\bibitem{how:96}
D.~Howe.
\newblock {Importing mathematics from HOL into Nuprl}.
\newblock In J.~von Wright, J.~Grundy, and J.~Harrison, editors, {\em Theorem
  Proving in Higher Order Logics}, volume 1125 of {\em LNCS}, pages 267--282,
  Berlin, 1996. Springer-Verlag.

\bibitem{kau:man:moo:00}
Matt Kaufmann, Panagiotis Manolios, and J.~Strother Moore.
\newblock {\em Computer-Aided Reasoning: An Approach}.
\newblock Kluwer Academic Publishers, Boston, 2000.

\bibitem{nau:ste:mes:01}
Pavel Naumov, Mark-Oliver Stehr, and Jos\'e Mesequer.
\newblock {A Proof-Theoretic Approach to the HOL-Nuprl Connection with
  Applications to Proof Translation}.
\newblock \hfill\break URL:
  \verb|<http://www.csl.sri.com/users/stehr/holnuprl-ext.ps.gz>|, 2001.

\bibitem{owr:rus:sha:92}
S.~Owre, J.~Rushby, and N.~Shankar.
\newblock {PVS: A prototype verification system}.
\newblock In D.~Kapur, editor, {\em 11th International Conference on Automated
  Deduction (CADE)}, volume 607 of {\em LNAI}, pages 748--752, Berlin,
  Heidelberg, New York, 1992. Springer-Verlag.

\bibitem{pau:94}
Lawrence~C. Paulson.
\newblock {\em Isabelle: a generic theorem prover}, volume 828 of {\em LNCS}.
\newblock Springer-Verlag, New York, 1994.

\bibitem{poi:02}
Henri Poincar\'e.
\newblock {\em La Science et l'Hypoth\`ese}.
\newblock Flammarion, Paris, 1902.

\bibitem{pol:98}
Robert Pollack.
\newblock {How to Believe a Machine-Checked Proof}.
\newblock In G.~Sambin and J.~Smith, editors, {\em Twenty-Five Years of
  Constructive Type Theory}. Oxford University Press, Oxford, 1998.

\end{thebibliography}

\end{document}