\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.92,.8}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-4em}$}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large computer algebra inside a proof assistant}

\red{Freek Wiedijk} \\
Radboud University Nijmegen

{{\small TYPES} workshop \green{Constructive analysis, types and exact real numbers}} \\
Radboud University Nijmegen \\
2005 10 03, 15:30
\end{slide}

\begin{slide}
\sectiontitle{computer algebra versus proof assistants}
\slidetitle{when things get tedious \hfill (the problem with proof assistants)}
\begin{eqnarray*}
\noalign{\vspace{-\bigskipamount}}
\noalign{problems from a small Mizar formalization:}
\noalign{\medskip}
x=i/n\;,\;\; n=m+1 &\red{\vdash}& n!\cdot x=i\cdot m! \\
\noalign{\smallskip}
{k\over n}\ge 0 &\red{\vdash}& \left|{n-k\over n}-1\right|={k\over n} \\
n\ge 2\;,\;\; x={1\over n+1} &\red{\vdash}& {x\over 1-x}<1 \adviwait\\
\noalign{\medskip}
\noalign{Jeremy Avigad, Isabelle:}
\noalign{\medskip}
\quad 0 \le n \le \big({K \over 2}\big)\, x \;,\;\; C > 0 \;,\;\; 0 < \varepsilon < 1 &\red{\vdash}& \Big(1 + {\varepsilon \over 3(C + 3)}\Big)\, n < K x
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\slidetitle{calculating \hbox to 6.69em{\vbox to 0pt{\vss$\displaystyle \int_0^\infty {e^{-(x-1)^2}\over\sqrt{x}} dx$}\hss} \hfill (the problem with computer algebra)}
\begin{alltt}\adviwait
> int(exp(-(x-t)^2)/sqrt(x), x=0..infinity);\adviwait
\end{alltt}
$$\green{{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}}}\adviwait$$
\begin{alltt}
> subs(t=1,%);
\end{alltt}
$$\green{{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}}}\adviwait$$
\begin{alltt}
> evalf(%);
\end{alltt}
$$\advirecord{d1}{0.4118623312}\adviplay[slidegreen]{d1}\adviwait$$
\begin{alltt}
> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));
\end{alltt}
$$\advirecord{d2}{1.973732150}\hspace{.5em}\adviplay[slidegreen]{d2}
\adviwait
\adviplay[slidered]{d1}
\adviplay[slidered]{d2}
$$

\vspace{-1em}
\vfill
\end{slide}

\def\tto{\;\longrightarrow\hspace{-1.4em}\longrightarrow\;}

\begin{slide}
\slidetitle{simplification and assumptions}
\begin{alltt}
> sqrt(x^2);\adviwait\medskip
\end{alltt}
\begin{eqnarray*}
\mbox{if we know}\quad \green{x \ge 0} &\;\mbox{then}\;& \green{\sqrt{x^2} \tto x} \adviwait\\
\noalign{\medskip}
\mbox{if we know}\quad \green{x \le 0} &\mbox{then}& \green{\sqrt{x^2} \tto -x} \adviwait\\
\noalign{\medskip}
\red{\mbox{nothing known about }\,x} &\mbox{then}& \red{\sqrt{x^2} \tto \black{\dots}} \adviwait\\
\noalign{\bigskip}
&& \qquad\mbox{\green{leave it unchanged?}} \adviwait\\
&& \qquad\mbox{\green{ask the user for the sign of $\,x\,$?}}\hspace{-1em} \adviwait\\
&& \qquad\mbox{\green{rewrite it to $\,{\it sign}(x)\cdot x\,$?}} \adviwait\\
&& \qquad\mbox{\green{do something else?}}
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\slidetitle{`read-eval-print' versus decision procedures}
\begin{itemize}
\item[$\bullet$]
\textbf{what computer algebra gives}

{`answer' unknown in advance}, but just one answer \\
always a trivial answer possible \\
\advirecord{a1}{bad administration of assumptions}
\begin{center}
\begin{tabular}{lclcl}
\red{`simplify'} && $\advirecord{a2}{\Gamma}\adviplay{a2}$ &$\!\vdash\!$& $t = \red{?}$ \\
\red{`solve'} && $\advirecord{a3}{\Gamma\,,}\adviplay{a3}\; \red{{?} = {?}}$ &$\!\vdash\!$& $t = u$
\end{tabular}
\end{center}
\adviwait
\adviplay[slidegreen]{a1}
\adviplay[slidegreen]{a2}
\adviplay[slidegreen]{a3}
\adviwait
\adviplay[white]{a2}
\adviplay[white]{a3}
\adviwait
\smallskip

\item[$\bullet$]
\textbf{what proof assistants need}

{many possible `answers' should be handled} \\
problems often too difficult to solve \\
\green{precise administration of assumptions}
\begin{center}
\begin{tabular}{lclcl}
\rlap{\red{`decide'}}\phantom{`simplify'} && $\green{\Gamma}\phantom{\,,\; {{?} = {?}}}$ &$\!\stackrel{\red{?}}{\vdash}\!$& $t = u$ \\
\end{tabular}
\end{center}

\end{itemize}
\vspace{-.5em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{MathXpert}
\slidetitle{system for teaching high school mathematics}
\vspace{-\bigskipamount}
\vbox to 0pt{
\vspace{-1.8em}
\hfill\includegraphics[width=6em]{/home/freek/talks/typesreal/pics/michael.eps}
\vss
}
\green{computer algebra system, Michael Beeson, 1997}
\smallskip

\begin{itemize}
\item[$\bullet$]
just high school mathematics \\
\green{`algebra', trig, limits, integrals} \\
not as powerful as Maple or Mathematica

\item[$\bullet$]
everything very much looks like in high school textbooks
\adviwait

%\item[$\bullet$]
%automatic simplifier (`AutoFinish') operates like a human

\item[$\bullet$]
\red{system explains step by step how it got its results} %\\
\adviwait

\item[$\bullet$]
\red{designed by a logician, so much more correct than other systems}
\adviwait

\end{itemize}
\bigskip

\blue{started out as a research project to show feasibility of idea $\;\Rightarrow\;$ \adviwait\\
sold to a commercial company $\;\Rightarrow\;$ \adviwait
company went bankrupt $\;\Rightarrow\;$ \adviwait\\
now privately marketed through the web}

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{MathXpert \textbf{demo}}
\bigskip

\begin{center}
\large
`$\;$simplify \red{$\big({\sqrt{2}}^{\sqrt{2}}\big)\!\strut^{\sqrt{2}}\;$}'
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{operations}
Mathpert is operated by repeatedly going through:
\begin{itemize}
\item[$\bullet$]
\green{select a sub-expression}

\item[$\bullet$]
\green{select an `operation' to apply to it} \\
(with `ShowStep' or `AutoStep' the system selects the step)

\item[$\bullet$]
very occasionally you have to supply an argument to the operation

\end{itemize}
\adviwait
\medskip
\vbox to 0pt{
\hfill\includegraphics[height=11em]{/home/freek/talks/typesreal/pics/operation.eps}\hspace{-4em}
\vss
}

\begin{tabular}{rl}
169 & menus \\
\noalign{\vspace{-\smallskipamount}}
1852 & menu items \\
\noalign{\vspace{-\smallskipamount}}
\red{1702} & \red{operations}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{C source code of a MathXpert operation}
\begingroup
\def\{{\char`\{}%
\def\}{\char`\}}%
\def\supnsqrt{$\,{}^n\!\surd$}%
\begin{alltt}
MEXPORT_ALGEBRA \red{int} EXPORT
      \red{\green{rootexp}(term t, term arg, term *next, char *reason)}
  /*   \blue{{\supnsqrt}x = x^(1/n)}   */
\{ term n,x;
  if(FUNCTOR(t) != ROOT)
     return 1;
  n = ARG(0,t);
  x = ARG(1,t);
  *next = make_power(x,make_fraction(one,n));
  HIGHLIGHT(*next);
  strcpy(reason,\blue{"${\supnsqrt}x = x^(1/n)$"});
  return 0;
\}
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{the `prove-refute-assume' paradigm}
calculation has a list of \green{current assumptions} \adviwait\\
built-in \green{`prover'} to deduce statements from these assumptions
\adviwait
\bigskip

if conditions need to be satisfied for an operation then if MathXpert \dots
\begin{itemize}
\item[$\bullet$]
can \red{prove} the condition, it performs the operation

\item[$\bullet$]
can \red{refute} the condition, it refuses the operation

\item[$\bullet$]
cannot prove nor refute the condition, then
it \\ \red{adds it to the assumptions} and performs the operation

\end{itemize}
\bigskip
\adviwait

prover uses \blue{non-standard analysis} \\
non-standard analysis not visible to the user!

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the MathXpert architecture inside the HOL world}
\slidetitle{HOL Light}
\vspace{-\bigskipamount}
\vbox to 0pt{
\vspace{-1.5em}
\hfill\includegraphics[width=4.5em]{/home/freek/talks/typesreal/pics/john.eps}
\vss
}
\green{proof assistant, John Harrison, 1998}
\smallskip

\begin{itemize}
\item[$\bullet$]
reimplementation of the venerable \red{HOL system}
\adviwait

\item[$\bullet$]
\blue{`the most perfect program ever written'} (Tom Hales)
\adviwait

\item[$\bullet$]
smallest `de Bruijn criterion' kernel that I know of
\adviwait

\item[$\bullet$]
largest number formalized from a list of 100 well-known theorems \\
\blue{\url{http://www.cs.ru.nl/~freek/100/}} \\
currently 54 theorems \adviwait\\
Coq has 27\adviwait, Mizar has 30\adviwait, all systems together 63
\adviwait

\item[$\bullet$]
used to formalize floating point hardware at Intel

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{operations versus lemmas}
\begingroup
\def\\{\char`\\}%
\begin{alltt}
let \green{ROOTEXP} = prove
 (\red{`&0 < x /\\ 0 < n ==> root(n) x = x^(&1/ &n)`},
  STRIP_TAC THEN
  SUBGOAL_THEN `?m. n = SUC m`
    (CHOOSE_THEN (fun th -> REWRITE_TAC[th])) THENL
  [ASM_MESON_TAC[num_CASES; LT_REFL]; ALL_TAC] THEN
  ASM_SIMP_TAC[POWER; ROOT_LN; REAL_MUL_LID; real_div]);;
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{ML type for MathXpert operations}
\textbf{C}
\begingroup
\def\xdots{{\sf\textsl{operationname}}}%
\begin{alltt}
\red{int \black{\xdots}(term \green{t}, term \green{arg}, term *\green{next}, char *\green{reason})}\toolong
\end{alltt}
\endgroup
\adviwait
\medskip

\textbf{ML}
\begingroup
\def\xdots{{\sf \dots}}%
\def\ydots{{\sf\textsl{operationname}}}%
\begin{alltt}
type \blue{operation} =
       \red{term option -> term list -> term -> thm list * thm};;\toolong
let ({\ydots}:\blue{operation}) = fun \green{arg ass t} -> {\xdots};;
\end{alltt}
\endgroup
%\adviwait
\medskip

returns theorems:
\vspace{-\medskipamount}
\begin{eqnarray*}
\green{\tt ass}' &\vdash& \green{\tt ass} \\
\green{\tt ass}' &\vdash& \green{\tt t} = \green{\tt next}
\end{eqnarray*}
\adviwait
C: returnvalue $\ne 0$ $\,\longrightarrow\,$ ML: throws an exception \adviwait\\
`\green{\texttt{reason}}' not supported

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{`MathXpert in HOL' \textbf{demo}}
\bigskip

\begin{center}
\large
`$\;$show that \red{$\big({\sqrt{2}}^{\sqrt{2}}\big)\!\strut^{\sqrt{2}} = 2\;$}'
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{unimplemented MathXpert features}
\begin{itemize}
\item[$\bullet$]
{99.8\% of the operations}
\adviwait

\item[$\bullet$]
\red{`AutoStep'}
\vspace{-1.5\bigskipamount}
\begingroup
\def\xdots{{\sf\dots}}
\def\xthm{\black{$\stackrel{\begin{array}{c}\hbox to 0pt{\hss$\scriptstyle\beta{\sf -expansion}$\hss}\\\noalign{\vspace{-\medskipamount}}\downarrow\\\noalign{}\end{array}}{\tt \green{term}}$}}
\begin{alltt}
let (one_step: \green{term list -> term -> \xthm * operation}) =\toolong
     \xdots;;
\end{alltt}
\endgroup
\adviwait

\item[$\bullet$]
interesting operations for the current focus
\adviwait

\item[$\bullet$]
dependence of the behavior of the operations on the \green{user model}
\end{itemize}
\adviwait
\medskip
\smallskip

\blue{features that are rather alien to the HOL Light world:}
\begin{itemize}
\item[$\bullet$]
{point \& click interface}
\adviwait

\item[$\bullet$]
\red{graphs}

\end{itemize}

\vspace{-.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{MathXpert operations versus HOL conversions}
\textbf{conversions}
\begingroup
\begin{alltt}
type conv      =               term ->            thm;;\toolong
\end{alltt}
\vspace{-.9\bigskipamount}
\endgroup
$$\advirecord{b1}{\hspace{13.4em}\phantom{{\varepsilon}\;\;\;}t \enskip\mapsto\hspace{4.3em} \phantom{{\varepsilon}\;\,,\;\,}\vdash t = t'\phantom{{\Gamma}\,}\hspace{-3.1em}}$$

\textbf{operations}
\begingroup
\def\xdots{\llap{\sf \dots}}
\begin{alltt}
type operation =
              \xdots -> \advirecord{b4}{term list}\adviplay{b4} -> term -> \advirecord{b5}{thm list}\adviplay{b5} * thm;;\toolong
\end{alltt}
\endgroup
\medskip
\advirecord{b2}{with an empty assumption list this becomes:}
$$\advirecord{b3}{\hspace{13.4em}\green{\varepsilon}\;\;\; t \enskip\mapsto\hspace{4.3em} \green{\varepsilon}\;\,,\;\,\red{\Gamma}\,\vdash t = t'\hspace{-3.1em}}$$
\adviwait
\adviplay{b1}
\adviwait
\adviplay{b2}
\adviplay{b3}
\adviplay[slidegreen]{b4}
\adviplay[slidegreen]{b5}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{conclusion}
\slidetitle{the real puzzle of how to put computer algebra in proof assistants}
how to fit \red{quite different interfaces} into a nice coherent whole?
\begin{itemize}
\item[$\bullet$]
\textbf{proof assistants}

goal that is changed by \blue{applying tactics} \\
{successive states are steps in a proof}
%\adviwait
\medskip

\item[$\bullet$]
\textbf{computer algebra systems}

\blue{read-eval-print} \\
{successive states can be completely unrelated}

\end{itemize}
\adviwait
\bigskip

apart from this interaction issue: \\
\green{(semantically correct) computer algebra fits cleanly inside a proof assistant\toolong}

\vfill
\end{slide}

\end{document}