\documentclass[jsco,square]{academic}
\newcommand{\cA}{{\cal A}}
\begin{document}
\title{A Constructive Algebraic Hierarchy in Coq}
\shorttitle{A Constructive Algebraic Hierarchy in Coq}
\author{Herman Geuvers}
\author{Randy Pollack}
\author{Freek Wiedijk}
\author{Jan Zwanenburg}
\shortauthor{H. Geuvers et al.}
\address{Department of Computer Science, Nijmegen University, the
Netherlands}
\maketitle
\begin{abstract}
We describe a framework of algebraic structures in the proof
assistant Coq. We have developed this framework as part of the FTA
project in Nijmegen, in which a constructive proof of the Fundamental
Theorem of Algebra has been formalized in Coq.
The algebraic hierarchy that is described here is both abstract and
structured. Structures like groups and rings are part of it in
an abstract way, defining e.g.\ a ring as a tuple consisting of a
group, a binary operation and a constant that together satisfy the
properties of a ring. In this way, a ring automatically inherits the
group properties of the additive subgroup. The algebraic hierarchy is
formalized in Coq by applying a combination of labeled record types
and coercions. In the labeled record types of Coq, one can use {\em
dependent types}: the type of one label may depend on another
label. This allows to give a type to a dependent-typed tuple like
$\langle A, f ,a\rangle$, where $A$ is a set, $f$ an operation on $A$
and $a$ an element of $A$. Coercions are functions that are used
implicitly (they are inferred by the type checker) and allow, for
example, to use the structure $\cA := \langle A, f ,a \rangle$ as
synonym for the carrier set $A$, as is often done in mathematical
practice. Apart from the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations.
\end{abstract}
\section{Introduction}
\subsection{Background}
When we started working on the FTA (Fundamental Theorem of Algebra)
project in the proof tool Coq \cite{coq:WWW} (see Sect.\ \ref{fta} for
an overview of this project) we needed an algebraic framework for it.
The requirements for such a framework included the following.
\begin{itemize}
\item We wanted to formalize a {\em constructive\/} proof of the
fundamental theorem of algebra, so we needed support for constructive
algebra.
\item We wanted to reason about {\em real numbers} and polynomials
over the reals.
\item We wanted to use an \emph{abstract\/} presentation of the real
numbers that could be instantiated with various constructions in the
future. In intensional type theory, such as Coq, this requires the
use of \emph{setoids}, which are a type and an equivalence relation
packaged together. This allows to deal with the set-theoretic notion
of a quotient, which any actual construction of the reals is a typical
example of.
\end{itemize}
No algebraic developments in Coq at that time could be a base for our
work, so we decided to develop our own \emph{algebraic hierarchy} for
Coq. This would be a constructive theory of the real numbers and
beyond, built on a pervasive notion of constructive setoid.
\subsection{Approach}
We did not want our mathematics to be dependent on specific
representations of the various algebraic structures, so we decided to
use an {\em axiomatic\/} approach. Instead of defining the real
numbers as, e.g.\ Cauchy sequences or Dedekind cuts, we have defined a
notion of {\em real number structure\/} of which both these
constructions would be an instance. For any `implementation' of this
notion all of our theory would immediately be available.
Constructive mathematics is supposed to have computational content,
but a proof of FTA based on an abstract real number structure,
although using only constructive principles, cannot compute the number
that the theorem claims exists, because the real number structure is
like an abstract data-type specification without an implementation.
However, after instantiating the abstract proof with a concrete
construction of the real number structure, the proof has full
computational content. Indeed, the proof of FTA that we have
formalized contains a root-finding algorithm. (As a matter of fact,
the proof can be seen as a correctness proof of this algorithm.) It
should be pointed out that, in order to do feasible computations with
this algorithm the actual representation of the real numbers is
crucial. The straightforward representation of reals as Cauchy
sequences over ${\mathbb Q}$ the rationals, as used in
\cite{geu:niq:01}, does not yield feasible computations.
\subsection{Related work}
Other algebraic hierarchies are similar to ours. However, they often
have not been {\em used\/} in a large proof development. Our
framework has been written and optimized for real-life use (to prove
the fundamental theorem of algebra).
Paul Jackson, in his Ph.D.\ thesis \cite{jac:95}, presents a
constructive development of algebra in Nuprl and uses it to prove some
results in abstract algebra. Nuprl, like Coq, is based on type theory,
but it uses an extensional equality. This makes several constructions
easier (e.g.\ quotienting), but renders type checking undecidable. As
Nuprl does not have coercive sub-typing, there is in general no
inheritance between structures.
A constructive algebraic hierarchy for Lego appears in the Ph.D.\
thesis of Anthony Bailey \cite{bai:99}.
Lo\"\i c Pottier has implemented a classical algebraic hierarchy for
Coq \cite{pot:01}. This hierarchy is more elaborate than ours and
mimics the hierarchy of the Axiom computer algebra system
\cite{jen:sut:92}.
In the FOC project, Sylvain Boulm\'e, Th\'er\`ese Hardin, Val\'erie
M\'enissier-Mo\-rain, Virgile Pr\'evosto and Renaud Rioboo are
building an environment to develop certified programs for symbolic
computation \cite{bou:har:hir:men:rio:99}. This environment will
contain a classical algebraic hierarchy. It is built from a certain
kind of records with dependent labeled fields, on which several
operations (refinement, extension, redefinition) have been defined
\cite{bou:00}. A Coq formalization of the FOC algebraic hierarchy is
planned. Currently only the framework of the FOC records has been
formalized.
Many provers have a formalization of the real numbers. Often such a
formalization is `flat' -- the type of the real numbers is not an
instance of a notion of `field' -- but some are part of an algebraic
hierarchy.
A flat development of the real numbers has been added to the Coq
library by Micaela Mayero \cite{del:may:01}. This development gives
classical axioms for the real numbers but does not implement a
specific model of it.
The Mizar system \cite{muz:93,wie:99:1} has both flat real numbers as
well as an algebraic hierarchy. Interestingly, it is the flat real
numbers that is used in most proofs that need the real numbers. The
Mizar algebraic hierarchy
has not been designed by one person. The various types, like
\verb|Group|, \verb|Ring| and \verb|Field| are defined in various
articles by various authors.
\subsection{Contribution}
We have built a library for doing algebra and analysis in Coq. It is
completely self-contained and completely constructive. That is, it
uses the Coq logic (the calculus of inductive constructions) and
contains no axioms. The algebraic hierarchy that we describe in this
paper is part of this library. It ranges from {\em constructive
setoids\/} to {\em real number structures}. (In \cite{geu:niq:01} it
is shown that the notion real number structure is categoric: any two
real number structures are isomorphic.) The library also contains a
construction of the complex numbers (out of a real number structure)
and of the polynomials over an arbitrary ring. The complex numbers are
shown to be an instance of a field and the polynomials are shown to be
a ring, which allows the inheritance of properties and notation from
fields, respectively rings. Finally, the library contains a
construction of the real numbers as Cauchy sequences, so despite the
fact that our theory is axiomatic in spirit we also give a specific
construction of the field of the real numbers (see \cite{geu:niq:01}).
Subjects treated in our framework are:
\begin{itemize}
\item groups, rings and fields
\item finite sums
\item polynomials
\item finite dimensional vector spaces
\item the real and complex numbers
\item real valued functions and continuity
\item the intermediate value theorem
\item real and complex roots
\end{itemize}
%
All together our Coq code consists of approximately
35000 lines or 860 kilobytes.
The theory that we have developed contains many `calculation lemmas'.
These are lemmas that give a calculation rule used to manipulate
algebraic expressions. We have created an automatic way to keep track
of these lemmas in the form of a {\LaTeX} document, in the spirit of
`literate programming'. Also we have developed specific reasoning
tools to make it easier to reason inside our framework without having
to know the names of the lemmas \cite{geu:wie:zwa:00}.
\subsection{Outline of this paper}
In Sect.\ \ref{fta} an overview of the FTA project is presented.
Sect.\ \ref{setoid} gives the notion of constructive setoid. Building
on this, Sect.\ \ref{hier} presents the algebraic hierarchy. Sect.\
\ref{add} develops our approach to representing the inheritance of
common notions in the hierarchy. Sect.\ \ref{partial} describes the
way our framework models partial functions such as division. For this
we introduce the notion of {\em sub-setoid}. Finally Sect.\
\ref{syntax} discusses the syntax of expressions and the complexity of
the underlying Coq terms.
In order to understand this paper one must have some basic familiarity
with the Coq system \cite{coq:WWW}.
\section{The Fundamental Theorem of Algebra project}\label{fta}
In 1999 and 2000 in the group of Henk Barendregt at the University of
Nijmegen, a proof of the fundamental theorem of algebra was formalized
in the Coq proof assistant \cite{coq:WWW}. This work was done in the
spirit of the QED Manifesto \cite{qed:94}. See \cite{FTA, FTApub,
geu:wie:zwa:01} for further details of this formalization project.
The proof of the FTA project is constructive. Before the FTA project
had been finished, a classical proof of the fundamental theorem of
algebra had already been formalized by Robert Milewski in Mizar
\cite{mil:00} and by John Harrison in HOL \cite{har:01}.
The four authors of the present paper designed the algebraic hierarchy
that is part of the FTA project.
The fundamental theorem of algebra states that every non-constant
polynomial over the complex numbers has a zero. In other words it
says that the field of the complex numbers is algebraically closed.
The proof that was formalized in Coq was a constructive proof by
Hellmuth and Martin Kneser \cite{kne:81,geu:wie:zwa:01}. We have kept
the formalization free of axioms. All that we needed was already
present in the Coq logic, the calculus of inductive constructions.
The final statement that we proved in the formalization was:
\begin{quote}
\begin{verbatim}
Lemma fta :
(f:(cpoly_cring CC))(nonConst ? f)->(EX z | f!z[=]Zero).
\end{verbatim}
\end{quote}
This says that for every non constant polynomial $f$
over the complex numbers there exists some complex number $z$
such that $f(z) = 0$.
\section{Setoids, constructive setoids and setoid functions}\label{setoid}
Coq is an intensional type theory. A notion called \emph{Leibniz
equality} is definable; it is the smallest reflexive relation. In a
context with no assumptions about Leibniz equality, it is equivalent
to the meta theoretic (intensional) \emph{definitional equality}. On
concrete constructions, such as natural numbers, where equality and
identity coincide, Leibniz equality coincides with the definable
structural identity. However, in abstract mathematics, this is not a
very useful relation. For instance consider the representation of
real numbers as Cauchy sequences. Two different Cauchy sequences
(i.e.\ intensionally distinguished by Leibniz equality) can represent
the same (extensionally) real number. If we were to assume axioms
restricting Leibniz equality to behave as intended for an abstract
real number structure, it would be impossible to implement that
structure with a construction.
We want to make a {\em quotient type\/} by dividing out the
equivalence relation `represent the same real'. The solution is to
work with {\em setoids} instead of raw types. A setoid is a type
together with an equivalence relation on it. (This equivalence,
called {\em setoid equality\/}, or \emph{book equality}, is written
\verb|x[=]y| in our use of Coq notation.) Quotienting a setoid is
achieved by changing its equivalence relation.
In constructive mathematics there is a little more to say, as the
notion of {\em apartness\/} (written $x\mathbin{\#}y$) is more
fundamental than the notion of equality. No amount of information can
show that concretely presented real numbers are equal. For example,
consider real numbers, $x$ and $y$, presented as Cauchy sequences: no
matter how many terms of $x$ and $y$ we may have examined and found to
be equal, we can not be sure that some later terms will not
distinguish $x$ from $y$. However, after some number of terms we may
see that $x$ and $y$ are so far apart that, being Cauchy sequences,
they cannot represent the same real. Two objects are \emph{apart} if
we `positively' know (have evidence) that they are different. For
instance a real number $x$ is apart from $0$ only if we can give some
natural number $n$ such that we know that $|x|>1/n$.
Packaging a carrier set with an equivalence relation and an apartness
relation, we get the notion of {\em constructive setoid\/}, called
\verb|CSetoid| in our framework. Apartness in such a \verb|CSetoid|
is written $\verb|x[#]y|$. In Coq we define constructive setoid as
a record type, as is shown on the top of the following page.
A {\em record type\/} in Coq consists of {\em labeled tuples}, where
the type of a field may be dependent on other fields. A term of type
\verb|CSetoid| is a tuple $\langle \verb|A|, \verb|R1|, \verb|R2|,
\verb|p|\rangle$, with \verb|A:Set|, \verb|R1:(relation A)|,
\verb|R2:(relation A)| and \verb|p:(is_CSetoid A R1 R2)|. (\verb|p|
is a proof that \verb|A|, \verb|R1|, \verb|R2| have property
\verb|is_CSetoid|.) The labels allow projection of a specific field
of the tuple: if \verb|S:CSetoid|, then \verb|(cs_crr S):Set| and
\verb|(cs_eq S):(relation (cs_crr S))|.
\begin{quote}
\begin{verbatim}
Record CSetoid : Type :=
{ cs_crr :> Set;
cs_eq : (relation cs_crr);
cs_ap : (relation cs_crr);
cs_proof : (is_CSetoid cs_crr cs_eq cs_ap)
}.
\end{verbatim}
\end{quote}
As a matter of fact, the
projection \verb|cs_crr| does not have to be written, because
\verb|cs_crr| is declared (by the annotation \verb|:>|) to be a {\em
coercion function}. This means that the type checker will insert this
function when necessary, driven by type-checking. For example \verb|S|
is not a type, and cannot have inhabitants, but if we declare a
variable \verb|x:S|, the type checker implicitly forms the correct
declaration \verb|x:(cs_crr S)|. This captures the common
mathematical usage of confusing a structure with its carrier.
In the above definition, \verb|is_CSetoid| is a predicate, the
conjunction of the defining properties of a constructive setoid. It
is itself defined as a record:
\begin{quote}
\begin{verbatim}
Record is_CSetoid [A:Set; eq,ap:(relation A)] : Prop :=
{ ax_ap_irreflexive : (irreflexive A ap);
ax_ap_symmetric : (symmetric A ap);
ax_ap_cotransitive : (cotransitive A ap);
ax_ap_tight : (tight_apart A eq ap)
}.
\end{verbatim}
\end{quote}
This says that a constructive setoid is a tuple
$\langle A,\mathord{\approx},\mathord{\#}\rangle$
that satisfies, for all $x$, $y$ and $z$ in $A$:
\begin{itemize}
\item apartness is irreflexive:\quad $\neg(x\mathbin{\#}x)$
\item apartness is symmetric:\quad $x\mathbin{\#}y \to y\mathbin{\#}x$
\item apartness is cotransitive:\quad $x\mathbin{\#}y \to x\mathbin{\#}z \lor z\mathbin{\#}y$
\item apartness is tight:\quad $\neg(x\mathbin{\#}y) \leftrightarrow x\approx y$
\end{itemize}
Because of the property of tightness we could have defined equality in
terms of apartness, rather than carrying it in our setoid structure.
However, equality is a very central notion in algebra (algebraic
properties are equational) and we wanted the notion of constructive
setoid to be a refinement of the notion of setoid. (Also to make the
work readily accessible for classical mathematicians.) Therefore we
didn't do this.
The field \verb|cs_eq| of a \verb|CSetoid| record is the function
that represents the equality.
Hence the Coq expression:
$$\verb|(cs_eq S x y)|$$ represents $x\approx y$ in \verb!S!. Since Coq can
determine the argument \verb|S| from the types of \verb|x| and
\verb|y|, we can define an operator \verb|[=]| such that $\verb|x[=]y|$
is a shorthand for \verb|(cs_eq S x y)|. Similarly we can define
\verb|x[#]y| as an abbreviation of {\tt (cs\_ap S x y)}.
The notion of \emph{setoid} allows an intensional formalization of {\em
quotient}. A function $f$ only induces a corresponding function on a
quotient of its domain when it {\em respects\/} the equivalence
$\approx$ that is being divided out:
$$x\approx y \to f(x)\approx f(y)$$
This is called {\em weak extensionality\/} or
{\em well-definedness\/} of the function.
It is defined in the Coq formalization as:
\begin{quote}
\begin{verbatim}
Definition fun_well_def [f:S1->S2] : Prop :=
(x,y:S1)(x[=]y)->((f x)[=](f y)).
\end{verbatim}
\end{quote}
Constructively, as apartness is more fundamental than equality, so the
property of {\em strong extensionality\/}
\begin{quote}
\begin{verbatim}
Definition fun_strong_ext [f:S1->S2] : Prop :=
(x,y:S1)((f x)[#](f y))->(x[#]y).
\end{verbatim}
\end{quote}
is more fundamental than well-definedness. It is easily shown that
strong extensionality implies well-definedness. The properties of
well-definedness and strong extensionality are also defined for
relations.
We have a record type of {\em constructive setoid functions},
consisting of pairs $\langle \verb|f|, \verb|p|\rangle$, with
\verb|f:S1->S2| and {\tt p:(fun\_strong\_ext f)}. (\verb|p| is a proof
that \verb|f| is strongly extensional.)
\begin{quote}
\begin{verbatim}
Record CSetoid_fun [S1,S2:CSetoid] : Set :=
{ csf_fun :> S1 -> S2;
csf_strext : (fun_strong_ext csf_fun)
}.
\end{verbatim}
\end{quote}
Due to the implicit coercions, the term \verb|csf_fun| is actually a
term of type \verb|(cs_crr S1) -> (cs_crr S2)|. This record type of
functions also illustrates another use of implicit coercions: if
\verb|F:(CSetoid_fun S1 S2)| and \verb|a:S1|, then we can apply
\verb|F| to \verb|a|. The term {\tt (F a)} is expanded by the type
checker to {\tt ((csf\_fun F) a)}.
Constructively, there are naturally occurring functions that are not
well-defined in the above sense. For instance the {\em $n$-th root\/}
$\root n\of x$ in the complex plane; it is possible to define the
$n$-th root of a complex number, but different representations of the
same complex number will sometimes have different complex roots (not
just different representations of the same complex root). So although
the $n$-th root function can be defined it does not respect the setoid
equality. Thus it is necessary to distinguish between {\em functions},
which are `just' terms \verb!f! of functional type \verb!S1->S2!, and
{\em setoid functions}, which should also be strongly extensional (and
hence respect the equality).\footnote{Bishop \cite{bis:67} calls these
\emph{operations} and \emph{functions} respectively.} The
non-well-definedness (constructively) of some functions is
unavoidable. Classically, this non-well-definedness is mirrored by
the fact that a function is not continuous and is not computable on
the representations. For example, the $n$-th root is classically
non-continuous as a function from ${\mathbb C}$ to ${\mathbb C}$. (It
can be made continuous by mapping to {\em sets\/} of roots, with an
appropriate topology on those sets.)
\section{Algebraic structures and coercive sub-typing}\label{hier}
We have defined a number of types in Coq representing algebraic structures
of which the carriers are constructive setoids. Each algebraic type
is defined in terms of the previous one.
\begin{center}
\begin{tabular}{ll}
\verb|CSetoid|&constructive setoids\\
\verb|CSemi_grp|\hbox{\quad}&semi-groups\\
\verb|CMonoid|&abelian monoids\\
\verb|CGroup|&abelian groups\\
\verb|CRing|&rings\\
\verb|CField|&fields\\
\verb|COrdField|&ordered fields\\
\verb|CReals|&`real number structures'
\end{tabular}
\end{center}
We will not present the definitions of these types in detail, but
refer the interested reader to the FTA files \cite{FTA}. The
structures of fields, ordered fields and real numbers are explained in
detail in \cite{geu:niq:01}. A more elaborate discussion of all the
structures and the whole FTA project will appear in \cite{FTApub}.
{From} the level of \verb|CMonoid| up, all structures we deal with are
assumed to be abelian. Henceforth, we will not explicitly mention this
property when talking about the hierarchy: when we speak about groups
we mean abelian groups.
In this paper we only present the definition of the type of rings in
terms of the type of groups; the other definitions follow the same
pattern. The type of rings is defined:
\begin{quote}
\begin{verbatim}
Record CRing : Type :=
{ cr_crr :> CGroup;
cr_one : cr_crr;
cr_mult : (CSetoid_bin_op cr_crr);
cr_proof : (is_CRing cr_crr cr_one cr_mult)
}.
\end{verbatim}
\end{quote}
The function \verb|cr_crr| that gives the underlying group is a
coercion (indicated by the annotation \verb|:>|) which Coq can
silently insert, as explained above (Sect.\ \ref{setoid}). So the
type \verb|CRing| is a coercive subtype of \verb|CGroup|. For details
of coercions in Coq see \cite{sai:97,coq:WWW}. For a more general
introduction into coercive sub-typing see \cite{bar96, luo:99, pol:00}.
The multiplication operation of a ring is a setoid function: it
respects setoid equality. We have types for such setoid functions
called \verb|CSetoid_bin_fun| and \verb|CSetoid_bin_op| (the second is
a specialized case of the first in which the domain and range setoids
are the same).
The defining property \verb|is_CRing| is:
\begin{quote}
\begin{verbatim}
Record is_CRing
[G:CGroup; one:G; mult:(CSetoid_bin_op G)] : Prop :=
{ ax_mult_assoc : (Associative mult);
ax_mult_mon : (is_CMonoid
(Build_CSemi_grp G one mult ax_mult_assoc));
ax_dist : (Distributive mult (csg_op G));
ax_non_triv : one[#]Zero
}.
\end{verbatim}
\end{quote}
This completes the definition of rings in terms of groups.
The general scheme of defining an algebraic structure \verb|B|
in terms of an algebraic structure \verb|A| is:
\begin{verse}
\verb|Record |{\em BName\/}\verb| : Type :=|\\
\verb| { |{\em b\/}\verb|_crr :> |{\em AName\/}\verb|;|\\
\verb| |{\em b\/}\verb|_|$\mbox{\em opName\/}_1$\verb| : |$\sigma_1$\verb|;|\\
\verb| |$\vdots$\\
\verb| |{\em b\/}\verb|_|$\mbox{\em opName\/}_n$\verb| : |$\sigma_n$\verb|;|\\
\verb| |{\em b\/}\verb|_proof : (is_|{\em BName\/}\verb| |{\em b\/}\verb|_crr |%
{\em b\/}\verb|_|$\mbox{\em opName\/}_1$\verb| |\dots\verb| |{\em b\/}\verb|_|$\mbox{\em opName\/}_n$\verb|)|\\
\verb| }.|
\end{verse}
\begin{verse}
\verb|Record is_|{\em BName\/}\\
\verb| [A:|{\em AName\/}\verb|; |$\mbox{\em opName\/}_1$\verb|:|$\sigma_1$%
\verb|; |\dots\verb|; |$\mbox{\em opName\/}_n$\verb|:|$\sigma_n$\verb|] : Prop :=|\\
\verb| { ax_|$\mbox{\em propName\/}_1$\verb| : |$P_1$\verb|;|\\
\verb| |$\vdots$\\
\verb| ax_|$\mbox{\em propName\/}_m$\verb| : |$P_m$\\
\verb| }.|
\end{verse}
Note that {\em BName} is not a structural subtype of {\em AName\/} in
the sense of having at least all the fields of {\em AName}. Instead
{\em AName\/} occurs as a field in {\em BName}. (Records in Coq are
\emph{right associative} and not \emph{extensible}, in the
classification of \cite{pol:00}.) However {\em BName} is a subtype of
{\em AName\/} by the coercion {\em b\/}\verb|_crr|, so that wherever
an {\em AName\/} is expected, a {\em BName} can be used instead.
In Coq, any term can be declared as a coercion: if \verb|f:A->B|, then
we can declare \verb|f| as a coercion by putting
\verb|Coercion f:A>->B|. (See \cite{sai:97} for a detailed account of
coercions in Coq.) Declaring a coercion \verb|f| means that the type
checker will try to insert \verb|f| if the term doesn't type check. If
there are more coercions, the type checker will try them all, so
coercions will be composed. There are some restrictions on coercions:
for obvious reasons, the system does not allow to have two coercions
with the same type at one time. This implies an important restriction
for our algebraic hierarchy: we can not have both a coercion from a
ring to its additive monoid {\em and\/} to its multiplicative monoid.
So, multiple inheritance is not possible in full generality.
In our algebraic hierarchy, we have only used coercions that arise
{from} a {\em field selection}, as shown in the example above where the
coercion {\em b\/}\verb|_crr| selects the first field of the labeled
record type {\em BName\/}. This yields a linear hierarchy of
structures, with field selecting coercions between them, as depicted
in the following diagram, where the names of the coercions are
omitted.
\begin{center}
\verb|CReals >-> COrdField >-> CField >-> CRing >-> CGroup|\\
\verb|CGroup >-> CMonoid >-> CSemi_grp >-> CSetoid|
\end{center}
So, the only multiple inheritance arises from the composition of
coercions: rings inherit structure (properties and operations) from
groups {\em and\/} monoids {\em and\/} semi-groups {\em and\/}
constructive setoids.
\section{Three ways to classify addition}\label{add}
We will now compare three ways to treat addition in Coq. The first is
the way it is done in the standard Coq library, the second is a bridge
to the third, which is the way it is done in the algebraic hierarchy.
\subsection{The standard Coq library: separate additions}
In the naive approach one defines an addition for every new type with
addition that is introduced. In the Coq standard library there are
three different additions for the natural numbers, the integers and
the reals:
\begin{quote}
\begin{verbatim}
plus : nat->nat->nat
Zplus : Z->Z->Z
Rplus : R->R->R
\end{verbatim}
\end{quote}
The properties of these additions must be developed (or assumed) from
scratch each time. For instance the commutativity of the addition is
present three times:
\begin{quote}
\begin{verbatim}
Lemma plus_com : (x,y:nat)(plus x y)=(plus y x).
Lemma Zplus_com : (x,y:Z)(Zplus x y)=(Zplus y x).
Axiom Rplus_com : (x,y:R)(Rplus x y)=(Rplus y x).
\end{verbatim}
\end{quote}
In this approach, the multiplicity continues for every new type that
is introduced: complex numbers, polynomials, matrices, functions, etc.
\subsection{The algebraic structure as a parameter}
The naturals, integers and reals are all commutative groups under
addition, and one can develop the theory of addition uniformly for
groups. This group addition is polymorphic in (i.e.\ parameterized
by) the particular group:
\begin{quote}
\begin{verbatim}
Gplus : (G:Group)(crr G)->(crr G)->(crr G).
\end{verbatim}
\end{quote}
where the carrier function \verb|crr:Group->Set| gives the underlying
set of a group.
For any concrete structure we wish to define, (e.g.\ the naturals) we
must still define addition and prove it satisfies the commutative
group axioms, but two significant advantages are gained. First, the
theory of commutative groups need only be developed once, and will
be inherited by each particular group. We can also declare abstract
groups, which immediately inherit all the properties of groups.
Second, and very important in large scale formalization, there are
uniform names for all the properties of abelian groups. Users of the
formalization need only consider \emph{one} commutative law:
\begin{quote}
\begin{verbatim}
Lemma Gplus_com :
(G:Group; x,y:(crr G))(Gplus G x y)=(Gplus G y x).
\end{verbatim}
\end{quote}
This law is applicable to all groups.
\subsection{Addition in the algebraic hierarchy}
In the previous subsection, we have considered the advantages of
classifying structures as groups. Two refinements are necessary.
\begin{itemize}
\item In our framework there is not just one type of structure, but a
hierarchy of structures: \verb|CSemi_grp|, \verb|CMonoid|,
\verb|CGroup|, \verb|CRing|, \ldots. Addition is declared at the
level of semi-groups, and inherited at more highly specified
levels\footnote{Commutativity of addition is declared at the level of
monoids. This property is then inherited at higher levels. As has
already been mentioned in Section \ref{hier}, all structures from {\tt
CMonoid} up are abelian, also if not explicitly stated.}.
\item Addition is not just an intensional function, but a setoid
function.
\end{itemize}
Each structure is a `subtype' of each simpler structure by a chain of
forgetful coercions
\begin{quote}
\begin{verbatim}
cm_crr : CMonoid->CSemi_grp.
csg_crr : CSemi_grp->CSetoid.
cs_crr : CSetoid->Set.
\end{verbatim}
\end{quote}
applied in the proper order.
The addition function, called \verb|csg_op|, is one of the fields of
the \verb|CSemi_grp| record. It has type:
\begin{quote}
\begin{verbatim}
csg_op : (G:CSemi_grp)
(CSetoid_bin_fun (csg_crr G) (csg_crr G) (csg_crr G)).
\end{verbatim}
\end{quote}
This returns a \verb|CSetoid_bin_fun| which is the type of a binary
setoid function. From it one can retrieve the underlying type
theoretic function by applying \verb|csbf_fun|:
\begin{quote}
\begin{verbatim}
csbf_fun : (S1,S2,S3:CSetoid)(CSetoid_bin_fun S1 S2 S3)->
(cs_crr S1)->(cs_crr S2)->(cs_crr S3).
\end{verbatim}
\end{quote}
Putting this together the sum of \verb|x| and \verb|y| in
a semi-group \verb|G| will be:
$$\verb|(csbf_fun (csg_crr G) (csg_crr G) (csg_crr G) (csg_op G) x y)|$$
The syntax of Coq is powerful enough to allow this to be abbreviated by:
$$\verb|x[+]y|$$
The \verb|G| argument will be determined from the
types of \verb|x| and \verb|y|. See Sect.~\ref{syntax} for
discussion of the complexity of the underlying representation.
The fact that in \verb|CMonoid| the right unit of addition is unique
is stated by the following Lemma.
\begin{quote}
\begin{verbatim}
Lemma cm_unit_unique_rht:
(M:CMonoid; x:M) ((y:M)(y[+]x [=] y)) -> (x [=] Zero).
\end{verbatim}
\end{quote}
Because of coercions, this lemma will work for every structure that can
be coerced to a monoid. Those are the groups, rings, fields, the real
and complex numbers, the polynomials, etc. The two advantages
mentioned in the previous subsection hold across the whole algebraic
hierarchy.
There are some technical restrictions on coercions, necessary to
maintain the meaning of the implicit notations. For example, it is
not possible to define a ring as the `union' of an additive and a
multiplicative monoid, because there can not be two coercions from
rings to monoids, see Section \ref{hier}.
\section{Partial functions and subsetoids}\label{partial}
One of the main problems in formal mathematics is how to deal with
partial functions. The type theoretic way to treat this problem is to
add proof objects as arguments to the functions; this is the approach
that we followed in our framework.
The prototypical partial function is division. In the algebraic
hierarchy the expression representing $x/y$ will have three arguments,
and be written
$$\verb|x[/]y[//]H|$$
where \verb|H:(y[#]Zero)| is a proof that
\verb|y| is apart from zero. This is actually managed by having a
\emph{subsetoid} of non-zero elements. Informally, the division
function might be written:
$$\cdot/\cdot : F \times F_{\ne 0} \to F.$$
Formally we define a type
corresponding to $F_{\ne 0}$ using the notion of a sub-setoid.
The elements of a \verb|subcsetoid_crr|, the carrier of a sub-setoid,
are pairs of an element of setoid \verb!S!, and a proof that the
element satisfies property \verb!P!.
\begin{quote}
\begin{verbatim}
Record subcsetoid_crr [S:CSetoid; P:S->Prop]: Set :=
{ scs_elem :> S;
scs_prf : (P scs_elem)
}.
\end{verbatim}
\end{quote}
An instance of \verb|subcsetoid_crr| can be turned into a setoid in a
canonical way, by inheriting the apartness and equality of \verb!S!,
and showing that they satisfy the required properties. This is done
via the map \verb!Build_SubCSetoid!, which takes a setoid \verb!S! and
a predicate \verb!P! over it, and returns the setoid of elements of
\verb!S! that satisfy \verb!P!.
Using this sub-setoid construction we can define the setoid of the
non-zeroes of a ring, together with functions \verb|nzinj| and
\verb|nzpro| (injection and projection) that relate it to the original
setoid. (We only give the types of the latter two functions.)
\begin{quote}
\begin{verbatim}
Variable F : CRing.
Definition NonZeroP [x:F] : Prop := x[#]Zero.
Definition NonZeros : CSetoid :=
(Build_SubCSetoid F NonZeroP).
Definition nzinj : NonZeros->F := ...
Definition nzpro : (x:F)(x[#]Zero)->NonZeros := ...
\end{verbatim}
\end{quote}
Division in our framework is defined from the reciprocal function.
This is a setoid function on the sub-setoid of the non-zeroes:
\begin{quote}
\begin{verbatim}
cf_rcpcl : (CSetoid_un_op (NonZeros F))
\end{verbatim}
\end{quote}
Division therefore has type
\begin{quote}
\begin{verbatim}
cf_div : (F:CField)F->(NonZeros F)->F
\end{verbatim}
\end{quote}
and the expression \verb|x[/]y[//]H| (parsed as
\verb|x[/](y[//]H)|)
is shorthand for
$$\verb|(cf_div F x (nzpro F y H))|$$
The expression \verb|(nzpro F y H)| represents $y$ considered
as an element of $F_{\ne 0}$.
The proof terms that occur in expressions cause some calculation rules
to have more conditions than one might expect. For instance the lemma
formalizing:
$${x/y\over z} = {x\over y\cdot z}$$
is:
\begin{quote}
\begin{verbatim}
Lemma div_div : (x,y,z:F)(nzy:y[#]Zero)(nzz:z[#]Zero)
(nzyz:(y[*]z)[#]Zero)
(((x[/]y[//]nzy)[/]z[//]nzz) [=] (x[/](y[*]z)[//]nzyz)).
\end{verbatim}
\end{quote}
In this lemma the condition \verb!(y[*]z)[#]Zero! is superfluous,
as it is implied by \verb!y[#]Zero!
and \verb!z[#]Zero!.
However, if we omit it (and plug in a proof using
\verb|nzy| and \verb|nzz| in the place of \verb|nzyz|), then the lemma
is harder to apply in practice.
\section{Syntax and complexity of terms}\label{syntax}
We can't use the customary operator symbols in our syntax because Coq
doesn't support overloading and the customary symbols are already in
use. We indicate that we are using a setoid analogue of a normal
operation by putting the operator in square brackets \verb|[| and
\verb|]|. So an equation like:
$${(x+y)}^2 = x^2 + 2xy + y^2$$
becomes in our syntax:
$$\verb|(x[+]y)[^](2)[=]x[^](2)[+]Two[*]x[*]y[+]y[^](2)|$$
and the equation:
$$p(X) = \sum_{i=0}^n a_i x^i$$
becomes:
$$\verb|p!x[=](Sum (0) n [i:nat](a i)[*]x[^]i)|$$
Clearly our notation could be more readable.
However, the notational features of Coq provide significant benefits,
and the official terms in our framework are much more complex than the
notation suggests. For instance suppose we have \verb|x,y:IR| (where
\verb|IR| is the type of the real numbers) then
$$\verb|x[+]y|$$
is an abbreviation of:
\begin{quote}
\begin{verbatim}
(csbf_fun (csg_crr (cm_crr (cg_crr (cr_crr (cf_crr (cof_crr
(crl_crr IR)))))))
(csg_crr (cm_crr (cg_crr (cr_crr (cf_crr (cof_crr (crl_crr
IR)))))))
(csg_crr (cm_crr (cg_crr (cr_crr (cf_crr (cof_crr (crl_crr
IR)))))))
(csg_op (cm_crr (cg_crr (cr_crr (cf_crr (cof_crr (crl_crr
IR))))))) x y)
\end{verbatim}
\end{quote}
Instead of what seems to be just one function symbol \verb|[+]|, the
term actually contains 33 function symbols. This shows that the terms
in our framework are relatively `heavy'. But note that most of this
big term is inferable coercions. In Luo's coercive sub-typing
\cite{luo:99} these parts of the term are actually elided, not just
suppressed in printing. This may be an important optimization for
large scale formal mathematics.
\section{Conclusion}
We presented a framework for writing algebraic expressions in the
Coq proof assistant.
The features of Coq that made our approach possible were:
\begin{itemize}
\item record types
\item coercive sub-typing
\item implicit arguments
\end{itemize}
Similar features are also available in other systems (for instance
the Mizar system) and therefore
something like our framework can be implemented in those systems.
In practice the framework that we have presented here works well.
There is hardly any duplication of theory despite the great number of
algebraic structures that we defined. For example, the theory of rings
has been used for the rationals, the reals, the complex numbers and
the polynomials. Apart from the reuse of theory, the reuse of notation
(via a form of overloading introduced by the coercion mechanism) is
also very convenient. Moreover this keeps user-level expressions
reasonably concise.
\subsection{Future work}
There are various things that need to be investigated further:
\subsubsection{Better record types.}
As already pointed out, one would like both the multiplicative monoid
and the additive monoid of a ring to be a coercive super-type of the
ring type itself. This is not allowed, because it creates two
coercions of the same type. Also, one would like a sub-setoid to be a
subtype of the setoid it is derived from. This coercion doesn't work
well in the current version of Coq. Further research on how coercions
can be improved is necessary. In \cite{pol:00} a start has been made
with these investigations.
\subsubsection{Structure of the hierarchy.}
The current hierarchy has been designed to make it possible to prove
the fundamental theorem of algebra. This means that it is not as rich
as one would like. For instance we don't have non-commutative
structures (apart from the basis \verb|CSemi_grp|) because they
didn't occur in our work.
One place where the hierarchy might be more refined is between
\verb|CField|, \verb|COrdField| and \verb|CReals|. Currently, the
useful properties of fields of characteristic zero are derived in
\verb|COrdField|. This is not the right place because the complex
numbers are not an ordered field (but they are a field of
characteristic zero) so for the complex numbers these results don't
apply. (We have to restate and prove these results for the complex
numbers separately.) The situation could be remedied by extending the
hierarchy as described in Section \ref{hier} with
\begin{center}
\verb|COrdField >-> CFieldCharzero >-> CField|
\end{center}
Similarly a number of the convergence notions are now defined
only for \verb|CReals|. However this is a subtype of \verb|COrdField|
so again these results don't apply to the complex numbers. But the
complex numbers do have a metric structure, and it would be desirable
to have a type \verb|CMetricField| for this.
This could be done by adding the following to the hierarchy
\begin{center}
\verb|CMetricField >-> CField|
\end{center}
In Coq, we can have both \verb|CMetricField| and \verb|CFieldCharzero|
in the hierarchy (as indicated above), but we can not have coercions
{from} the complex numbers to both types, because this would produce (by
composition of coercions) two coercions from the complex numbers to
\verb|CField|, which is not allowed.
\subsubsection{Partial functions.}
The current way Coq deals with partiality is through proof terms in
the expressions. This is unnatural. The PVS system
\cite{owr:rus:sha:92} offers a different solution: in PVS a partial
function is a total function on its domain. Whether a partial
function is defined on an element is handled through so-called `type
check conditions', which may create extra proof obligations, but don't
show up in syntax. A similar approach is used in Nuprl, that has
subset types. This approach works very well, but the price to be paid
is that type checking becomes undecidable. This is not felt as a
serious problem among PVS users. It is valuable to investigate
whether a similar approach can be adapted to Coq.
\subsubsection{Better syntax.}
The current syntax of our framework is not very readable.
The integers and reals in the Coq standard library
have custom parsers that allow for the more common algebraic notation.
It would be valuable to build a parser like that for the algebraic hierarchy.
\subsubsection{Classical logic.}
The current algebraic hierarchy is completely constructive. For many
people it is irrelevant whether their reasoning is constructive or
not. In their case classical logic would be much easier, and it would
be useful to have a classical variant of the algebraic hierarchy. One
could for instance define a notion of {\em decidable setoid\/} in
which the equality is decidable. Combining this notion with the types
of the algebraic hierarchy then would give a classical algebraic
hierarchy.
\subsection{Acknowledgements}
We acknowledge the support from the EC Calculemus Network. Thanks to
the anonymous referees for valuable comments. Furthermore, we want to
thank Dan Synek, Henk Barendregt and Milad Niqui for valuable feedback
and discussions.
\bibliographystyle{plainnat}
\begin{thebibliography}{10}
\bibitem{bai:99}
A.~Bailey.
\newblock {\em {The machine-checked literate formalisation of algebra in type
theory}}.
\newblock PhD thesis, Manchester University, 1999.
\bibitem{coq:WWW}
B.~Barras et al.
\newblock {\em The Coq Proof Assistant Reference Manual}, 2000.
\newblock URL: \verb||.
\bibitem{bar96} G.~Barthe.
\newblock{Implicit coercions in type systems}.
\newblock In Stefano Berardi and Mario Coppo, editors, {\em Types for
proofs and programs: international workshop {TYPES} '95, Torino,
Italy: selected papers}, vol.\ 1185 of {\em LNCS}, pp.\ 1--15,
Berlin, 1996. Springer-Verlag.
\bibitem{bis:67}
E.~Bishop.
\newblock {\emph{Foundations of Constructive Analysis}}.
\newblock {McGraw-Hill, 1967}.
\bibitem{bou:00}
S.~Boulm\'e.
\newblock {Op\'erateurs de raffinement sur les structures alg\'ebriques}.
\newblock In {\em Actes des Journ\'ees Francophones des Langages Applicatifs}, 2000.
\bibitem{bou:har:hir:men:rio:99}
S.~Boulm\'e, T.~Hardin, D.~Hirschkoff, V.~M\'enissier-Morain, and R.~Rioboo.
\newblock {On the way to certify computer algebra systems}.
\newblock In {\em Proceedings of the Calculemus workshop of FLOC'99\/}
(Federated Logic Conference, Trento, Italy), vol.\ 23 of ENTCS.
Elsevier, 1999.
\bibitem{qed:94}
R.~Boyer.
\newblock {The QED Manifesto}.
\newblock In A.~Bundy, editor, {\em Automated Deduction - CADE 12}, volume 814
of {\em LNAI}, pages 238--251. Springer-Verlag, 1994.
\bibitem{del:may:01}
D.~Delahaye and M.~Mayero.
\newblock {Field: une proc\'edure de d\'ecision pour les nombres r\'eels en
Coq}.
\newblock In {\em Proceedings of JFLA'2001, INRIA}, 2001.
\newblock URL:
\verb||.
\bibitem{FTA} The FTA project,
\verb||.
\bibitem{FTApub} H.~Geuvers, F.~Wiedijk, J.~Zwanenburg, H.~Barendregt,
M.~Niqui, R.~Pollack, Formalizing the Fundamental Theorem of Algebra,
forthcoming.
\bibitem{geu:niq:01}
H.~Geuvers and M.~Niqui.
\newblock {Constructive Reals in Coq: Axioms and Categoricity}.
\newblock To appear in {\em Proceedings of the Workshop Types
2000, Durham UK,} Springer-Verlag, 2002.
\bibitem{geu:wie:zwa:00}
H.~Geuvers, F.~Wiedijk, and J.~Zwanenburg.
\newblock {Equational Reasoning via Partial Reflection}.
\newblock In Mark Aagaard and John Harrison, editors, {\em Theorem Proving in
Higher Order Logics, TPHOLs 2000, Portland}, vol.\ 1869 of {\em LNCS}, pp.\ 162--178, Berlin, 2000.
Springer-Verlag.
\bibitem{geu:wie:zwa:01}
H.~Geuvers, F.~Wiedijk, and J.~Zwanenburg.
\newblock {A Constructive Proof of the Fundamental Theorem of Algebra
without using the Rationals}.
\newblock To appear in {\em Proceedings of the Workshop Types
2000, Durham UK,} Springer-Verlag, 2002.
\bibitem{har:01}
J.~Harrison.
\newblock {Complex quantifier elimination in HOL}.
\newblock In Richard Boulton and Paul Jackson, editors,
{\em TPHOLs 2001, Supplemental Proceedings}, Informatics Research Report,
Division of Informatics, University of Edinburgh, pp.\ 159--174, 2001.
\bibitem{jac:95}
P.~Jackson.
\newblock {\em {Enhancing the Nuprl proof-development system and
applying it to computational abstract algebra}}.
\newblock Ph.D.\ thesis, Cornell University, 1995.
\bibitem{jen:sut:92}
R.~Jenks and R.~Sutor.
\newblock {\em {AXIOM}: The Scientific Computation System}.
\newblock Spring{\-}er-Ver{\-}lag, Berlin, 1992.
\bibitem{kne:81}
M.~Kneser.
\newblock {Erg\"anzung zu einer Arbeit von Hellmuth Kneser \"uber den
Fundamentalsatz der Algebra}.
\newblock {\em Math. Z.}, 177:285--287, 1981.
\bibitem{luo:99}
Z.~Luo.
\newblock {Coercive subtyping}.
\newblock {\em Journal of Logic and Computation}, 9(1), 1999.
\bibitem{mil:00}
R.~Milewski.
\newblock {Fundamental Theorem of Algebra}.
\newblock {\em Journal of Formalized Mathematics}, 12, 2000.
\newblock MML Identifier: \verb|POLYNOM5|.
\bibitem{muz:93}
M.~Muzalewski.
\newblock {\em An Outline of PC Mizar}.
\newblock Fond.\ Philippe le Hodey, Brussels, 1993.
\bibitem{owr:rus:sha:92}
S.~Owre, J.~Rushby, and N.~Shankar.
\newblock {PVS: A prototype verification system}.
\newblock In D.~Kapur, ed., {\em 11th International Conference on Automated
Deduction (CADE)}, vol.\ 607 of {\em LNAI}, pp.\ 748--752, Berlin, 1992. Springer-Verlag.
\bibitem{pol:00}
R.~Pollack.
\newblock {Dependently Typed Records for Representing Mathematical Structure}.
\newblock In Mark Aagaard and John Harrison, editors, {\em Theorem Proving in
Higher Order Logics, TPHOLs 2000, Portland}, vol.\ 1869 of {\em LNCS}, pp.\ 462--479, Berlin, 2000.
Springer-Verlag.
\bibitem{pot:01}
L.~Pottier.
\newblock {Un d\'ebut de formalisation de l'alg\`ebre en Coq et Ctcoq}.
\newblock Web page, 2001.
URL: \hfill\break \verb||.
\bibitem{sai:97}
A.~Sa{\"\i}bi.
\newblock Typing algorithm in type theory with inheritance.
\newblock In {\em Proc.\ of the 24th Symp.\ on Principles of
Programming Languages ({POPL'97})}, pp.\ 292--301, 1997.
\bibitem{wie:99:1}
F.~Wiedijk.
\newblock {Mizar: An impression}.
\newblock Unpublished, 1999.
\newblock URL: \hfill\break
\verb||.
\end{thebibliography}
\end{document}