\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}