\documentclass[runningheads]{llncs} \RequirePackage{url} \usepackage{graphicx} \usepackage{alltt} \input{thol.tex} \begin{document} \author{Cezary Kaliszyk and Freek Wiedijk} \title{Certified Computer Algebra on top of an Interactive Theorem Prover} \institute{ \{\texttt{cek},\texttt{freek}\}\texttt{@cs.ru.nl} \\ Institute for Computing and Information Sciences,\\ Radboud University Nijmegen, the Netherlands} \date{\today} \maketitle{} \begin{abstract} We present a prototype of a computer algebra system that is built on top of a proof assistant, {HOL Light}. This architecture guarantees that one can be certain that the system will make no mistakes. All expressions in the system will have precise semantics, and the proof assistant will check the correctness of all simplifications according to this semantics. The system actually \emph{proves} each simplification performed by the computer algebra system. Although our system is built on top of a proof assistant, we designed the user interface to be very close in spirit to the interface of systems like {Maple} and {Mathematica}. The system, therefore, allows the user to easily probe the underlying automation of the proof assistant for strengths and weaknesses with respect to the automation of mainstream computer algebra systems. The system that we present is a prototype, but can be straightforwardly scaled up to a practical computer algebra system. \end{abstract} \section{Introduction} %\subsection{Motivation} % In this paper we study the relationship between two important classes of % computer programs that manipulate mathematical formulas: proof assistants and % computer algebra systems. % A computer algebra system (or `CAS') has at its core a set of algorithms, % which is made available to the user through a friendly interface. The % formulas the algorithms of a computer algebra system manipulate generally do % not have precise semantics. They are simplified in a way that resembles the % style a mathematician simplifies expressions on paper, but for that the % symbols that occur in those formulas do not need a mathematical definition % inside the system. % On the other hand, the mathematical symbols that occur in proof assistants % always have precisely defined semantics. Proof assistants not only manipulate % symbolic expressions, but also theorems that are stated using those symbols. % The basic activity in a proof assistant is not simplification of expressions % but proving of theorems. A proof assistant generally does not have many % algorithms available for automating the application of those theorems, and to % make use of those that are there one needs to have good knowledge of the % prover environment. The interface to a proof assistant is generally less % friendly to a naive user than that of a CAS. Computer algebra systems do not always give correct answers. This happens because those systems do not certify the operations performed. There can be various reasons for errors in a CAS: assumptions can be lost, types of expressions can be forgotten \cite{aslaksen}, the system might get confused between branches of `multi-valued' functions, and of course the algorithms of the system themselves may contain implementation errors \cite{wester}. As an example of the kind of error that we are talking about here, consider the following \textsc{Maple} \cite{maple} session that tries to compute $\int_0^\infty {e^{-(x-1)^2}\over\sqrt{x}} dx$ numerically in two different ways: \begin{alltt} > int(exp(-(x-t)^2)/sqrt(x), x=0..infinity); \end{alltt} $${{1\over 2} {e^{-t^2} \Big({-{3 (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{3\over 4\rlap{\phantom{\tiny g}}}({t^2\over 2}) \over t^{2\rlap{\phantom{x}}}}} + {\textstyle (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{7\over 4}({t^2\over 2})} \Big) \over \pi^{1\over 2}}}$$ \begin{alltt} > subs(t=1,%); \end{alltt} $${{1\over 2} {e^{-1} \big({-3 \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{3\over 4}({1\over 2})} + \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{7\over 4}({1\over 2})\big) \over \pi^{1\over 2}}}$$ \begin{alltt} > evalf(%); \end{alltt} $$0.4118623312$$ \begin{alltt} > evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity)); \end{alltt} $$1.973732150$$ (We are showing \textsc{Maple} here, but all major computer algebra systems make errors like this.) To be sure that results are correct, one may use a proof assistant instead of a CAS. But in that case even calculating simple things, like adding fractions or calculating a derivative of a polynomial becomes a non-trivial activity, which requires significant experience with the system. %\subsection{Approach} Our approach is to implement a computer algebra system on top of a proof assistant. For our prototype we chose the LCF-style theorem prover \textsc{HOL Light} \cite{hollight}. Thanks to this, we obtain a CAS system where the user can be sure of the correctness of the results. Such a system has strong semantics, that is all variables have types, all functions have precise definitions in the logic of the prover and for every simplification there is a theorem that ensures the correctness of this simplification.\footnote{In \textsc{HOL Light} \emph{simplification} is implemented through what in the LCF world is called \emph{conversions}. A {conversion} is a function that takes a term and returns an equational theorem. The theorem has the given term on its left side and a simplified version of the term on the right side. In this paper `simplification' should \emph{not} be taken to be a fixed reduction hard-wired into the logic of the proof assistant, the way it is in type theoretical systems like \textsc{Coq} \cite{coqman}.} The interface of our computer algebra system resembles most CAS systems. It has a simple read-evaluate-print loop. The language of the formulas typed into the system is as close as possible to the language in which formulas are generally entered in CAS and to the language in which mathematics is done on paper. Interaction with the system currently looks like this\footnote{ The `\texttt{\&}', `\texttt{Cx}' and `\texttt{\#}' are coercions to real, complex and floating point numbers }: \begin{holnb} In1 := (3 + 4 DIV 2) EXP 3 * 5 MOD 3 Out1 := 250 In2 := vector [\&2; \&2] - vector [\&1; \&0] + vec 1 Out2 := vector [\&2; \&3] In3 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) + \&7 + exp (exp x))) Out3 := \Lam{}x. exp x pow 2 * exp (exp x) + exp x * exp (exp x) + -- \&12 * sin (\&2 * x) In4 := N (exp (\&1)) 10 Out4 := #2.7182818284 + ... (exp (\&1)) 10 F In5 := 3 divides 6 \Conj{} EVEN 12 Out5 := T In6 := Re ((Cx (\&3) + Cx (\&2) * ii) / (Cx (-- \&2) + Cx (\&7) * ii)) Out6 := \&8 / \&53 \end{holnb} \begin{holnb} In7 := x + \&1 - x / \&1 + \&7 * (y + x) pow 2 Out7 := \&7 * x pow 2 + \&14 * x * y + \&7 * y pow 2 + \&1 In8 := sum (0,5) (\Lam{}x. \&x * \&x) Out8 := \&30 \end{holnb} %\subsection{Related work} One can distinguish three categories of systems that try to fill the gap between computer algebra and proof assistants: \begin{itemize} \item Theorem provers inside computer algebra systems: \begin{itemize} \item \textsc{Analytica} \cite{analytica98}, %analytica92 \item \textsc{Theorema} \cite{theorema00}, \item \textsc{RedLog} \cite{redlog}, % - logical extension of \textsc{Reduce} \item logical extension of \textsc{Axiom} \cite{logicalaxiom}. \end{itemize} \item Frameworks for mathematical information exchange between systems: \begin{itemize} \item \textsc{MathML} \cite{mathml03}, \item \textsc{OpenMath} \cite{openmath}, \item \textsc{OMSCS} \cite{omscs}, \item \textsc{MathScheme} \cite{mathscheme}, \item \textsc{Logic Broker} \cite{logicbroker}. \end{itemize} \item Bridges between theorem provers and computer algebra systems, also referred to as ad-hoc information exchange solutions: \begin{itemize} \item \textsc{PVS} and \textsc{Maple} \cite{maplepvs}, \item \textsc{HOL} and \textsc{Maple} \cite{maplehol98}, \item \textsc{Isabelle} and \textsc{Maple} \cite{mapleisabelle}, \item \textsc{NuPrl} and \textsc{Weyl} \cite{weylnuprl}, \item \textsc{Omega} and \textsc{Maple/GAP} \cite{sapper}, \item \textsc{Isabelle} and \textsc{Summit} \cite{isabellesumit}. \end{itemize} \end{itemize} An important distinction that one can make within the category of bridges is the \emph{degree of trust} between the prover and the CAS. In some of these solutions the prover uses the simplification of the CAS as an axiom, i.e., without checking its correctness. But in other solutions the prover takes the CAS output and then builds a verified theorem out of it. In this case there are again two possibilities: either the result is verified independently of how the CAS obtained it, or the system takes a trace of the rules that the CAS applied, and then uses that as a suggestion for what theorems should be used to construct a proof of the result. In the work that we referred to here either the proof assistant is built inside the CAS, or the proof assistant and the CAS are next to each other. In our work however, we have the CAS inside the proof assistant. Of course in many proof assistants there already is CAS-like functionality, in particular many proof assistants have arithmetic procedures or even powerful decision procedures. However, we do not just provide the functionality, but also build a \emph{system} that can be used in a similar way as most other computer algebra systems are used. In our system it is the first time that anyone pursued the combination of a CAS \emph{inside} a proof assistant (in which all simplifications are validated), with an interface that has the customary CAS look and feel. Our way of combining theorem proving and computer algebra has advantages over the ones presented above. All calculations done by our system are certified by the architecture of our system. All formulas defined inside it have types assigned, all defined operators have explicit semantics and all simplifications performed have theorems associated with them. No translation of formulas or semantics is needed, as the CAS shares the internal data structures of the proof assistant. There is no need to worry about mistakes in the implementation of the CAS, since all conversions are certified using the logic of the underlying prover. There is no verification required after the result is obtained, thanks to the creation of theorems alongside with the results. All simplifications performed by our architecture are completely certified, that is if a certificate for a particular simplification does not exist \cite{henk} it can not be performed. All variables used in \textsc{HOL Light} conversions have to be typed, so working in a proof assistant might seem less flexible than a traditional CAS implementation, but the abundance of decision procedures for HOL show that this probably is not a strong limitation. %\subsection{Contents} The paper is organized as follows: in Section \ref{arch} we present the architecture of the system. In Section \ref{knowledge} we talk about the knowledge base. Finally in Section \ref{conclusion} we present a conclusion. \section{Architecture}\label{arch} We present a general architecture for a certified computer algebra system, and we will describe an implementation prototype. The source for the prototype is available from \url{http://www.cs.ru.nl/~cek/holcas/}. For the implementation we chose the proof assistant \textsc{HOL Light} \cite{hollight}. The factors that influenced our choice were: the possibility to manipulate terms to create the conversions, prove theorems and implement the system in the same language\footnote{\textsc{HOL Light} is written in \textsc{OCaml} and is provided as an extension of it}, as well as a good library of analysis and algebra. The system created is rather a proof of concept than a real product, which is why the efficiency of the underlying prover was not a decisive factor. In particular we perform all computations inside the proof assistant's logic, sometimes with the help of decision procedures. Our system is divided in three independent parts (Fig. 1): the user interface (input-response loop), the abstract algorithm of dealing with a formula (we will call this \textit{the CAS conversion}), and the knowledge that is specific to the CAS system. That architecture allows the user both to use it as a computer algebra system, as well as making it usable in the context of theorem proving\footnote{\textit{The CAS conversion} can be applied to a goal to be proved using \texttt{CONV\_TAC}.}. \begin{figure}[htb] \centering \includegraphics[width=.9\textwidth]{arch} \caption{Architecture of a CAS inside a TP system with responsibilities of the parts of our implementation marked. The prover is not marked on the figure, since all parts make use of it, by using it's type of terms and theorems, as well as tactics and conversions to build them.} \end{figure} \subsection{Input-response loop} The system displays a prompt, where one can write expressions to be simplified and commands. It is necessary to distinguish expressions to be computed or simplified from commands that represent actions that do not evaluate anything, like listing theorems or modifying and printing assumptions. Every expression that is not recognized as a command is passed to \textit{the CAS conversion}, which will try to compute or simplify the expression. The theorem given back by \textit{the CAS conversion} is the certificate that the output is correct. If \textit{the CAS conversion} is not able to simplify the term, it returns an instance of reflexivity, and the result is then the same as the input. In most CASs variables can be used without declaring them, but for certain algebraic operations one can define a variable to be of a particular type (necessary for example in \textsc{Magma}). Our system can handle expressions in both ways. The free variables are typed using \textsc{HOL Light} type inference, but one can also require a specific type with the \texttt{assumetype} command (described in section 3.4). Most computer algebra systems allow one to reuse previously typed in expressions and calculated outputs. One may calculate \texttt{In1 + Out2}. The loop has to have access to all expressions entered, theorems proved and outputs. In our framework every expression entered is stored with its type, so when it is reused, parsing the same expression, even in a different context, gives the same type. \subsection{Abstract CAS conversion} To be able to benefit from the CAS simplification in theorem proving, it is useful to have the CAS functionality available as a single conversion (that we call here \textit{the CAS conversion}). Since the underlying prover can be further developed and new theorems can be proved later, it is useful to separate \textit{the CAS conversion} from the knowledge that it uses. For this reason \textit{the CAS conversion} is parametrized. The general idea behind \textit{the CAS conversion} is to try to apply all sub-conversions from the knowledge base at all positions in the term until it is saturated (Fig. 2). Applying the same conversions to a modified term is necessary, since some conversions return terms, parts of which can be again simplified. Particular implementations may include mechanisms to increase efficiency or to provide termination of simplification. We are not particularly aiming at completeness for the algorithms in \textit{the CAS conversion}, since completeness in practice can only be realized for rather basic theories. However any mathematically correct algorithm that exists for existing computer algebra systems can be implemented as a \textsc{HOL Light} conversion too, that does the calculation while building the correctness proof in parallel. Examples include conversions that perform algorithms for integration, conversions that perform splitting and joining for branching calculations, or conversions that simplify terms involving higher order operations (like summation). \begin{figure}[htb] \centering \includegraphics[width=.9\textwidth]{casconv} \caption{Our implementation of \textit{the CAS conversion} first tries to look up the term in a built-in cache (for efficiency). If the term is an application or an abstraction, then it tries to simplify subterms recursively (not performed if the term is known not to be expandable or is a suggestion that should not be expanded, for example \texttt{NUMERAL} or \texttt{assuming}). Finally it tries to apply all conversions from the knowledge base to the term.} \end{figure} \section{CAS-like knowledge}\label{knowledge} %The knowledge of a computer algebra system is substantially different from %that of a proof assistant. Usually the main part of a CAS's knowledge %consists of algorithms that just manipulate formulas, and usually the theory %on which they are based is not represented inside the system. On the other %hand, the primary part of a proof assistant is a large collection of %definitions and theorems. %There are different possible approaches we implement to the creation of %theorems that certify correctness of algorithms implementing CAS-style %simplifications. In certain cases a theorem is built alongside with the term %analyzed. Sometimes it is sufficient to do a calculation in \textsc{OCaml} %code and only verify the result in the logic. For example a factorization of %big integers or polynomials can be simply verified by multiplying them %out. This is where our approach is similar to the ``bridge'' approach. The %important difference is that an algorithm for a calculation \emph{together} %with a certification form a single conversion that can be introduced in the %knowledge base. %\subsection{Knowledge base} The knowledge base is a separate part of the system. The knowledge is kept in a discrimination net (a structure that allows matching a term to a number of patterns efficiently). There is an interface on the theorem prover level that allows introducing knowledge to the knowledge base in the following three forms: \begin{itemize} \item Rewrite rules, for example:\\ \texttt{|- \Fa{}z. abs (norm z) = norm z} \item Conditional rewrite rules, for example:\\ \texttt{|- \Fa{}x. \&0 <= x ==> abs x = x} \item Conversions meant to be used with an argument that matches a certain pattern and return ad-hoc rewrite rules. An ad-hoc rewrite rule is a theorem that is generated to be used for rewriting the formula, but it is not added to the knowledge base (although our implementation keeps all rewritten theorems in cache, implemented as a hash-table, for efficiency reasons). For example the \textsc{HOL Light} conversion \texttt{DIVIDES\_CONV} takes terms that match the pattern \texttt{n divides m} and then returns ad-hoc rewrite rules for the given data like \texttt{|- 33 divides 123453 <=> T}. \end{itemize} \textit{The CAS conversion} has to check whether the given term matches one of the rewrite rules and ad-hoc rewrite rules in the knowledge base. For efficiency it keeps all theorems and conversions included in the knowledge base in a discrimination net. To allow matching conversions with even less overhead, optional patterns for matching associated with conversions can be provided. The discrimination net is not changed, the particular used instances are only added to the cache. %\subsection{Knowledge representation} To resemble a CAS system, the formulas processed by the system should be in the ``evaluation'' form and not in ``verification'' form. Let us compare the ways in which one writes differentiation in the \textsc{HOL Light} library and the way it is written in our CAS: \begin{alltt} \Fa{}x. (f diffl (g x)) x \Func{} diff f = g (f diffl (g x)) x \Func{} diff f x = g x \end{alltt} In \textsc{HOL Light} the \texttt{diffl} predicate takes three arguments: the function (on the left of the predicate), the value of its derivative and the point. To write a general derivative we need to generalize the point and replace the value with the derivative function in this point. Even then it is still a binary predicate. In most computer algebra systems there exists a simple \texttt{diff} operator, that takes a function and returns its derivative. Using the Hilbert's choice operator, we created a such function, defined: \texttt{diff f = \Lam{}x. \Hilbert{}v. (f diffl v) x}. We also created a conversion that is able to calculate the derivative of a function, if \textsc{HOL Light}'s \texttt{DIFF\_CONV} can. Just like we defined a functional form of differentiation, we also defined a functional integration operator. Using these we can then compute the following expressions in the system: \begin{holnb} In9 := dint (\&1,\&2) sin Out9 := -- \&1 * cos (\&2) + cos (\&1) In10 := dint (\&1,\&2) (\Lam{}x. x pow n) Out10 := \&1 / \&(n + 1) * \&2 pow (n + 1) + -- \&1 * \&1 / \&(n + 1) * \&1 pow (n + 1) In11 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) + \&7 + exp (exp x))) (\&2) Out11 := exp (exp (\&2)) * exp (\&2) pow 2 + exp (exp (\&2)) * exp (\&2) + -- \&12 * sin (\&4) In12 := diff (\Lam{}x. dint (x,x + \&2) (\Lam{}x. x pow 3)) Out12 := \Lam{}x. \&6 * x pow 2 + \&12 * x + \&8 \end{holnb} %If a function is not differentiable, or the system does not know how to %differentiate it, then the conversion is not able to simplify it, and the input is %returned unchanged. Our differentiation and integration definitions do not work well with partial functions. An approach for defining them in such a way that partial functions are handled better will be described in Section \ref{conclusion}. \subsection{Numerical approximations} In complex calculations computer algebra systems provide users with numerical approximations. They are usually implemented with an approximation algorithm, which keeps an error bound with every calculation. In a proof assistant a numerical approximation must have its semantics completely defined, and the algorithm has to respect the approximation definition and theorems that specify its properties. The two main ways of rounding a real number are down to an integer and towards the nearest integer. Both these operations do not give rise to a computable function (see for example \cite{lester}). In \cite{vuillemin} it is shown that if one computes non-deterministically either one of those values then one does get a computable function. We will use a conversion that calculates the value rounded both down and to nearest value, that terminates when one of those calculations terminate. We propose to define the numerical approximation of a given number \texttt{x} to a precision \texttt{p} as identical to the number itself: \texttt{N x p = x}. It is only a hint for the system that the number has to be simplified to a decimal fraction plus a rest. It is the rest, that determines in which form is the number given: rounded down or rounded to the nearest. For rest defined in this way we provide a theorem, that states that the approximation can be different from the exact value only on the last digit, and the difference is less than one. In the following \textsc{HOL Light} definitions, \verb|N| is the numerical approximation of a number to a precision (following the convention of \textsc{Mathematica}) and \verb|...| is the rest of a number to the given precision with an additional argument that specifies the form of the rest. \verb|T| stands for rounding to nearest and \verb|F| stands for rounding down. \begin{holnb} ... x p F = x - floor (&10 pow p * x) / &10 pow p ... x p T = x - floor (&10 pow p * x + &1 / &2) / &10 pow p |- abs(... x p v - x) < &1 / &10 pow p \end{holnb} The system is able to compute some numerical approximations with this scheme: \begin{holnb} In13 := N (\&1 / \&3) 8 Out13 := #0.33333333 + ... (\&1 / \&3) 8 F In14 := N (sqrt #5.123456789) 8 Out14 := #2.26350542 + ... (sqrt #5.123456789) 8 F In15 := N (dint (#0.1,#0.4) exp) 7 Out15 := #0.3866537 + ... (-- \&1 * exp #0.1 + exp (\&2 / \&5)) 7 F \end{holnb} \subsection{Assumptions} In most CASs there is a possibility to make type assumptions or binary assumptions about variables. Examples include assuming a variable to be greater than zero, greater than another variable, natural or real. There are various methods of introducing assumptions in computer algebra systems: \begin{itemize} \item Assumptions associated with a simplification\\ in \textsc{Mathematica}: \verb|Simplify[Sin[n Pi], Element[n,Integers]]| \item Global list of assumptions\\ in \textsc{Maple}: \verb|assume(x>0); sqrt(x*x);| \item Asking the user for conditions on variables (e.g. \textsc{Maxima}) \item Adding assumptions automatically and silently to the prover environment (e.g. \textsc{MathXpert}) \end{itemize} In our system we keep a global list of assumptions, which are Boolean properties that may be later used to instantiate assumptions of rewrite rules and ad-hoc rewrite rules. In a big CAS the number of rules that can be used is so big that asking the user seems not to be a good choice. Also automated assuming will probably not behave too well in such a situation. An assumption can be introduced by the user either using \texttt{assume}, which takes a Boolean, or \texttt{assumetype} which takes a typed variable. An assumption associated with a single simplification of a sub-term may be also introduced using \texttt{assuming}. The latter method temporarily changes the assumptions list to simplifying the sub-expression. The assumptions will be added to the assumptions of the theorem generated by \textit{the CAS conversion}, which is why changing the assumptions list is only useful at the top-level of the expression to simplify. The global list of assumptions is used by the conversions from the knowledge base, therefore we consider is a part of the latter. To ensure the usage of variables with correct types, type checking has to have access to this list. When an expression is typed in the system it is type-checked in a particular context. This context includes types already assigned to all free variables from the assumptions list, as well as all variables for which types have been assumed with \verb|assumetype|. To do this, the latter are kept in another global list. \looseness=-1 For example, $\sqrt{x^2}$ cannot be simplified to $x$, since we don't know whether $x$ is positive or not. Also $\frac{x}{x}$ cannot be simplified to $1$, since it is possible that $x = 0$. \begin{holnb} In16 := sqrt (x * x) Out16 := abs x In17 := x / x Out17 := x * inv x \end{holnb} When an assumption about $x$ is introduced, stating that it is greater then $1$, numeric things about $x$ can be proved, and both of the above formulas can be simplified: \begin{holnb} In18 := assume (x > \&1) Out18 := T In19 := x > #0.5 Out19 := T In20 := sqrt (x * x) Out20 := x In21 := x / x Out21 := \&1 \end{holnb} There are two ways in which assumptions are used: direct and indirect. The first way is to use an assumption directly in the derivation in unchanged form. It can be used to a prove a reflexive theorem or to fill the requirement of a certain conditional rewrite rule (or a conditional ad-hoc rewrite rule). An assumption may be used as an indirect step in the derivation, for example simplifying $abs(x)$ to $x$ requires $x \ge 0$, and the assumption $x > 1$ can be used for this. \subsection{Manipulating assumptions} A CAS has to provide a mechanism for adding assumptions and listing defined assumptions. In our prototype we added the \texttt{assumptions} and \texttt{about} commands, which resemble their \textsc{Maple} equivalents. \begin{holnb} Command: about Argument: x `x > &1` \end{holnb} An issue that is hard to handle in any approach are errors that may be caused by incorrect parsing and printing. We try to be as close as possible to the original \textsc{HOL Light}'s parsing and printing mechanism. In fact, the system currently uses HOL's term printing (with special output for errors) but, when parsing, the system has to add typing information and distinguish commands from terms. Special output is added, so that the user always knows when a given string has been interpreted as a command. To further lower the risk of parsing and printing problems, we add the \texttt{theorems} command. It allows printing all theorems defined in a session. The standard \textsc{HOL Light} theorem printing function is used for this. It is especially useful for conversions that use assumptions, because in that it case the assumptions that have been actually used will be shown. Below are the first five theorems proved by the examples from this document: \begin{holnb} Command: theorems |- (3 + 4 DIV 2) EXP 3 * 5 MOD 3 = 250 |- vector [&2; &2] - vector [&1; &0] + vec 1 = vector [&2; &3] |- diff (diff (\Lam{}x. &3 * sin (&2 * x) + &7 + exp (exp x))) = (\Lam{}x. exp x pow 2 * exp (exp x) + exp x * exp (exp x) + -- &12 * sin (&2 * x)) |- N (exp (&1)) 10 = #2.7182818284 + ... (exp (&1)) 10 F |- 3 divides 6 \Conj{} EVEN 12 <=> T \end{holnb} \section{Conclusion}\label{conclusion} Our work integrates computer algebra and proof assistant technology. We will now look at how our architecture compares with what one gets by just having a CAS or a proof assistant. Developing a system according to our architecture (i.e., where the algorithms not only generate the results, but also generate certificates of the correctness of those results) will be slower than the development of traditional CAS systems (because that only has to generate the results). As far as the performance of the system is concerned, our architecture will be somewhat slower than a traditional CAS as well. This is mostly because generating the certificates for all simplifications also takes time. However, we expect this slow-down over traditional CAS to only multiply the running time by a constant factor. Our expectation is not experiment based, but based on the architecture, we trace what a traditional CAS does and provide proofs for every step. When we compare our architecture to the way that one normally does CAS-like manipulations in an interactive theorem prover, the main difference is the interaction model. Our CAS system does not interactively work on propositions that are to be proved, but instead takes an expression and automatically simplifies it. %\subsection{Future work} Our primary focus is to extend the knowledge base with a formalization of multivalued functions, to be able to handle more complicated expressions, like the \textsc{Maple} example of a complex function with multiple branches given in the introduction. Another important feature that we plan to investigate are the coercions that many proof assistants use, like the embedding of the integers in the real numbers or the real numbers in the complex numbers. Currently a user of our prototype needs to use the `\texttt{\&}' and `\texttt{Cx}' symbols for this (as is customary in the \textsc{HOL Light} library). A small improvement to the current situation might be to overload the `\texttt{\&}' operator, but we would rather not make the user write these functions at all. An issue that our approach does not cover is completeness of the conversions. In the case of rewrite rules the completeness is clear. But in the case of arbitrary algorithms, it is not guaranteed by our architecture that a given conversion will always terminate and never fail. %\subsection{Outlook} % We presented an architecture for a certified computer algebra system, and % addressed some issues that were encountered when using this architecture. We % also presented the details of a prototype of our architecture that was % implemented on top of a state-of-the-art proof assistant. Although the % prototype is not a powerful CAS at the moment, we believe it can be extended % into one, just by extending the knowledge base that the system uses. We believe that both computer algebra systems and proof assistants currently have a problem. In computer algebra the lack of explicit semantics and the lack of verification of the results inside the system makes the systems less reliable than one would like them to be. In proof assistants the powerful symbolic manipulations that are taken for granted in computer algebra often are missing and, even when present, it takes work and expertise to make use of it. We claim that the architecture that we present here can solve both problems simultaneously. The computer algebra systems will get explicit semantics and certification. And the proof assistants will get CAS-like functionality that will make them more powerful and easier to use than they are today. \bibliographystyle{plain} \bibliography{all} \end{document}