\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,.6}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\definecolor{slideorange}{rgb}{1,.5,0}
\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\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\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{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\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{-20em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut merging the procedural and declarative proof styles}

\red{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

%Summer School and Conference
\green{Mathematics, Algorithms and Proofs} \\
{\small ICTP},
Trieste, Italy \\
{\small 2008\hspace{3pt}08\hspace{3pt}25, 14\hspace{1pt}:\hspace{1.8pt}00}
\smallskip

\green{Mathematical Logic and Computers} \\
satellite workshop of {\small ALC} 10 \\
Kobe, Japan \\
{\small 2008\hspace{3pt}08\hspace{3pt}31, 14\hspace{1pt}:\hspace{1.8pt}50}

\end{slide}

\begin{slide}
\sectiontitle{which system is best for formal mathematics?}
\slidetitle{80 out of \green{\advirecord{a1}{100 theorems}}\adviplay{a1}}
\vbox to 0pt{\small
\vspace{-1.1em}
\begin{tabular}{lr}
\enskip 1. The Irrationality of the Square Root of 2 & \llap{$\ge {\sf 17}$} \\
\noalign{\vspace{-\smallskipamount}}
\enskip 2. \red{Fundamental Theorem of Algebra} & 4 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 3. The Denumerability of the Rational Numbers & 6 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 4. Pythagorean Theorem & 6 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 5. \red{Prime Number Theorem} & 2 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 6. \red{G\"odel's Incompleteness Theorem} & 3 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 7. Law of Quadratic Reciprocity & 4 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 8. The Impossibility of Trisecting the Angle and Doubling the Cube$\quad$ & 1 \\
\noalign{\vspace{-\smallskipamount}}
\enskip 9. The Area of a Circle & 1 \\
\noalign{\vspace{-\smallskipamount}}
10. Euler's Generalization of Fermat's Little Theorem & 4 \\
\noalign{\vspace{-\smallskipamount}}
11. The Infinitude of Primes & 6 \\
\noalign{\vspace{-\smallskipamount}}
\gray{12. The Independence of the Parallel Postulate} & \gray{0} \\
\noalign{\vspace{-\smallskipamount}}
13. \red{Polyhedron Formula} & 1 \\
\noalign{\vspace{-\smallskipamount}}
\phantom{00. }\dots
\end{tabular}
\vss
}
\adviwait
\adviplay[slidegreen]{a1}

\vfill
\end{slide}

\begin{slide}
\slidetitle{five systems}
\medskip

\begin{center}
\hspace{2.1em}%
\begin{tabular}{llrcc}
\llap{\setbox0=\hbox{{\advirecord{b}{$\mbox{\small HOL}\;\Bigg\{\enskip\quad$}}}\ht0=-1em\dp0=-1em\raise -.92em\box0}%
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/usa.eps}$\quad$ &
{{\small HOL} Light} & $\enskip\;\;$\blue{69} &$\,$& \advirecord{c1}{\red{procedural}} \\
\noalign{\smallskip}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/uk.eps} &
{{{ProofPower}}} & \blue{42} && \advirecord{c2}{\red{procedural}} \\
\noalign{\smallskip}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/germany.eps} &
{Isabelle} & \blue{40} && \advirecord{c3}{\green{declarative} $+$ \red{procedural}} \\
\noalign{\smallskip}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/france.eps} &
{Coq} & \blue{39} && \advirecord{c4}{\red{procedural}} \\
\noalign{\smallskip}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/poland.eps}
\includegraphics[width=14pt]{/home/freek/talks/nmc/pix/flags/japan.eps} &
{Mizar} & \blue{45} && \advirecord{c5}{\green{declarative}}
\end{tabular}\hspace{-2.5em}\strut
\end{center}
\adviwait
\adviplay{b}
\adviwait
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay{c4}
\adviplay{c5}

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural versus declarative}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\gray{
\begin{picture}(5,5)
\white{%
\put(0.5,4.5){\makebox(0,0){\advirecord{s1}{\rule{\unitlength}{\unitlength}}}}
\put(1.5,4.5){\makebox(0,0){\advirecord{s2}{\rule{\unitlength}{\unitlength}}}}
\put(2.5,4.5){\makebox(0,0){\advirecord{s3}{\rule{\unitlength}{\unitlength}}}}
\put(3.5,4.5){\makebox(0,0){\advirecord{s4}{\rule{\unitlength}{\unitlength}}}}
\put(3.5,3.5){\makebox(0,0){\advirecord{s5}{\rule{\unitlength}{\unitlength}}}}
\put(2.5,3.5){\makebox(0,0){\advirecord{s6}{\rule{\unitlength}{\unitlength}}}}
\put(1.5,3.5){\makebox(0,0){\advirecord{s7}{\rule{\unitlength}{\unitlength}}}}
\put(0.5,3.5){\makebox(0,0){\advirecord{s8}{\rule{\unitlength}{\unitlength}}}}
\put(0.5,2.5){\makebox(0,0){\advirecord{s9}{\rule{\unitlength}{\unitlength}}}}
\put(0.5,1.5){\makebox(0,0){\advirecord{s10}{\rule{\unitlength}{\unitlength}}}}
\put(0.5,0.5){\makebox(0,0){\advirecord{s11}{\rule{\unitlength}{\unitlength}}}}
\put(1.5,0.5){\makebox(0,0){\advirecord{s12}{\rule{\unitlength}{\unitlength}}}}
\put(1.5,1.5){\makebox(0,0){\advirecord{s13}{\rule{\unitlength}{\unitlength}}}}
\put(2.5,1.5){\makebox(0,0){\advirecord{s14}{\rule{\unitlength}{\unitlength}}}}
\put(2.5,0.5){\makebox(0,0){\advirecord{s15}{\rule{\unitlength}{\unitlength}}}}
\put(3.5,0.5){\makebox(0,0){\advirecord{s16}{\rule{\unitlength}{\unitlength}}}}
\put(4.5,0.5){\makebox(0,0){\advirecord{s17}{\rule{\unitlength}{\unitlength}}}}
}%
\advirecord{s0}{
\put(0,5){\line(1,0){5}}
\put(.5,4.5){\makebox(0,0){\black{\scriptsize $0$}}}
\put(0,4){\line(1,0){3}}
\put(1,3){\line(1,0){2}}
\put(2,2){\line(1,0){1}}
\put(4,2){\line(1,0){1}}
\put(3,1){\line(1,0){2}}
\put(4.5,.5){\makebox(0,0){\black{\scriptsize $\infty$}}}
\put(0,0){\line(1,0){5}}
\put(0,0){\line(0,1){5}}
\put(1,1){\line(0,1){2}}
\put(2,0){\line(0,1){1}}
\put(3,1){\line(0,1){2}}
\put(4,2){\line(0,1){2}}
\put(5,0){\line(0,1){5}}
}%
\adviplay[slidegray]{s0}%
\end{picture}
}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{s1}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s1}%
\adviplay[slidelightgray]{s2}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s2}%
\adviplay[slidelightgray]{s3}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s3}%
\adviplay[slidelightgray]{s4}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s4}%
\adviplay[slidelightgray]{s5}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s5}%
\adviplay[slidelightgray]{s6}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s6}%
\adviplay[slidelightgray]{s7}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s7}%
\adviplay[slidelightgray]{s8}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s8}%
\adviplay[slidelightgray]{s9}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s9}%
\adviplay[slidelightgray]{s10}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s10}%
\adviplay[slidelightgray]{s11}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s11}%
\adviplay[slidelightgray]{s12}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s12}%
\adviplay[slidelightgray]{s13}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s13}%
\adviplay[slidelightgray]{s14}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s14}%
\adviplay[slidelightgray]{s15}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s15}%
\adviplay[slidelightgray]{s16}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s16}%
\adviplay[slidelightgray]{s17}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s17}%
\adviplay[slidegray]{s0}%

\begin{itemize}
\item[$\bullet$]
\textbf{procedural}

\begingroup
\strut\small
\red{{%
\adviwait
\adviplay[slidelightgray]{s17}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s17}%
E
\adviplay[slidelightgray]{s16}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s16}%
E
\adviplay[slidelightgray]{s15}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s15}%
S
\adviplay[slidelightgray]{s14}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s14}%
E
\adviplay[slidelightgray]{s13}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s13}%
N
\adviplay[slidelightgray]{s12}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s12}%
E
\adviplay[slidelightgray]{s11}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s11}%
S
\adviplay[slidelightgray]{s10}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s10}%
S
\adviplay[slidelightgray]{s9}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s9}%
S
\adviplay[slidelightgray]{s8}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s8}%
W
\adviplay[slidelightgray]{s7}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s7}%
W
\adviplay[slidelightgray]{s6}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s6}%
W
\adviplay[slidelightgray]{s5}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s5}%
S
\adviplay[slidelightgray]{s4}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s4}%
E
\adviplay[slidelightgray]{s3}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s3}%
E
\adviplay[slidelightgray]{s2}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s2}%
E
\adviplay[slidelightgray]{s1}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s1}%
\adviplay[slidegray]{s0}
}}
\endgroup

{{\small HOL}, Coq, {\advirecord{t1}{Isabelle}}\adviplay{t1}}

\adviwait
\medskip
\item[$\bullet$]
\textbf{declarative}

\begingroup
\strut\scriptsize
\green{{%
\adviwait
(0,0)
\adviplay[slidelightgray]{s1}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s1}%
(1,0)
\adviplay[slidelightgray]{s2}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s2}%
(2,0)
\adviplay[slidelightgray]{s3}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s3}%
(3,0)
\adviplay[slidelightgray]{s4}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s4}%
(3,1)
\adviplay[slidelightgray]{s5}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s5}%
(2,1)
\adviplay[slidelightgray]{s6}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s6}%
(1,1)
\adviplay[slidelightgray]{s7}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s7}%
(0,1)
\adviplay[slidelightgray]{s8}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s8}%
(0,2)
\adviplay[slidelightgray]{s9}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s9}%
(0,3)
\adviplay[slidelightgray]{s10}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s10}%
(0,4)
\adviplay[slidelightgray]{s11}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s11}%
(1,4)
\adviplay[slidelightgray]{s12}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s12}%
(1,3)
\adviplay[slidelightgray]{s13}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s13}%
(2,3)
\adviplay[slidelightgray]{s14}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s14}%
(2,4)
\adviplay[slidelightgray]{s15}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s15}%
(3,4)
\adviplay[slidelightgray]{s16}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s16}%
(4,4)\toolong
\adviplay[slidelightgray]{s17}\adviplay[slidegray]{s0}\adviwait\adviplay[white]{s17}%
\adviplay[slidegray]{s0}%
}}\toolong
\endgroup

{Mizar, {\advirecord{t2}{Isabelle}}\adviplay{t2}}

\end{itemize}
\adviwait
\adviplay[slideblue]{t1}
\adviplay[slideblue]{t2}

\vspace{-4pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the state of the art in formal mathematics}

\begin{itemize}
\item[$\bullet$]
\red{Georges Gonthier} \\
\red{\textbf{Coq}} \\
\red{Four Color Theorem}, \blue{2004}
\smallskip
%\adviwait

Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas \\
\green{The four colour theorem} \\
%Journal of Combinatorial Theory Series B {70}$\,$(1), 1997
{43 pp.}

\medskip
\adviwait

\item[$\bullet$]
\red{John Harrison} \\
\red{\textbf{{\small HOL}}} \\
\red{Prime Number Theorem}, \blue{2008}
\smallskip
%\adviwait

Donald Newman \\
\green{Analytic Number Theory}, chapter VII \\
%Graduate Texts in Mathematics 177, Springer, 1997}
{9 pp.}

\end{itemize}

\vspace{-14pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the systems}
\medskip

\begin{center}
\begin{tabular}{ccl}
\red{\advirecord{d1a}{\fbox{\strut\quad\advirecord{d1b}{\textbf{\small HOL}}\quad}}}\adviplay{d1b} && \rlap{\white{\advirecord{f1}{$\leftarrow$ unpleasant proof language}}}\green{\advirecord{e1}{\rlap{$\leftarrow$ most theorems}}} \\
\noalign{\smallskip}
\white{\fbox{\strut \black{\advirecord{d2}{\textbf{Isabelle}}}}}\adviplay{d2} \\
\noalign{\smallskip}
\white{\fbox{\strut \gray{\advirecord{d3}{\textbf{Coq}}}}}\adviplay{d3} && \gray{\advirecord{e3a}{$\leftarrow$ four color theorem}\advirecord{e3b}{ $+$ {intuitionistic weirdness}}} \\
\noalign{\smallskip}
\red{\advirecord{d4a}{\fbox{\strut\hspace{.68em}\advirecord{d4b}{\textbf{Mizar}}\hspace{.68em}}}}\adviplay{d4b} && \rlap{\white{\advirecord{f4a}{$\leftarrow$ only weak automation}\advirecord{f4b}{ $+$ {closed architecture}}}}\green{\advirecord{e4}{$\leftarrow$ most mathematical}}
\end{tabular}
\end{center}
\adviwait
\adviplay[slidegreen]{e1}
\adviwait
\adviplay[slidegreen]{e3a}
\adviwait
\adviplay[slidegreen]{e4}
\adviwait
\adviplay[slidegreen]{e3b}
\adviwait
\adviplay[slidegray]{d3}
\adviplay[slidegray]{e3a}
\adviplay[slidegray]{e3b}
\adviwait
\adviplay[slidered]{d1a}
\adviplay[slidered]{d1b}
\adviplay[slidered]{d4a}
\adviplay[slidered]{d4b}
\adviwait
\adviplay[white]{e3a}
\adviplay[white]{e3b}
\adviplay[white]{e1}
\adviplay[white]{e4}
\adviplay[slidegreen]{f1}
\adviplay[slidegreen]{f4a}
\adviwait
\adviplay[slideblue]{d2}
%\adviwait
%\adviplay{d2}
%\adviplay[slidegreen]{f4b}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{{\small HOL} Light}
\slidetitle{overview}
\vspace{-1.4em}
\vbox to 0pt{
\vspace{-1.0em}
\hfill\includegraphics[height=7em]{/home/freek/papers/cursus/pics/johnh.eps}\strut
\vss
}
1972$\,$--$\,$today \\
$
\blue{
\mbox{LCF} \to \mbox{{\small HOL}} \to \Bigg\{\!
\begin{array}{l} \mbox{\small HOL4} \\
\noalign{\vspace{-\smallskipamount}}
\mbox{\textbf{{\small HOL} Light}} \\
\noalign{\vspace{-\smallskipamount}}
\mbox{ProofPower} \end{array}
}
$

$\mbox{Robin Milner} \to \mbox{Mike Gordon} \to \textbf{John Harrison}$ \\
$\mbox{Stanford, US} \to \mbox{Cambridge, UK} \to \mbox{Portland, US}$
\medskip
%\adviwait

\green{higher order logic} $\;=$
weak, typed set theory
\medskip
\adviwait

\red{very nice open architecture} \\
only 394 lines of ocaml code need to be trusted
\smallskip
\adviwait

\red{relatively strong automation}% \\
%\red{very open architecture}

\vspace{-5pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example: session}
\hbox to 0pt{\vbox to 0pt{
\vspace{1.4em}
\hfill\advirecord{u}{\includegraphics[width=6.5em]{/home/freek/talks/miz3/pics/proof.eps}\hspace{-2pt}}\strut
\vss}\hss}%
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
        HOL Light 2.20++, built 11 March 2008 on OCaml 3.09.2 with ckpt\medskip
val it : unit = ()
# \adviwait\green{g `!n. nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2`;;}\adviwait\adviplay{u}\adviwait
val it : goalstack = 1 subgoal (1 total)\medskip
\red{`!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2`}\medskip
# \adviwait\green{e INDUCT_TAC;;}\adviwait
val it : goalstack = 2 subgoals (2 total)\medskip
  0 [`nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2`]\medskip
`nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2`\medskip
\red{`nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2`}\medskip
# \adviwait\green{e (ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;}\adviwait
val it : goalstack = 1 subgoal (2 total)\medskip
\red{`(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2`}\medskip
#
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example: session (continued)}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
\red{`(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2`}\medskip
# \adviwait\green{e ARITH_TAC;;}\adviwait
val it : goalstack = 1 subgoal (1 total)\medskip
  \red{0 [`nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2`]\medskip
`nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2`}\medskip
# \adviwait\green{e (ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;}\adviwait
val it : goalstack = 1 subgoal (1 total)\medskip
  \red{0 [`nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2`]\medskip
`(if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =\toolong
 (SUC n * (SUC n + 1)) DIV 2`}\medskip
# \adviwait\green{e ARITH_TAC;;}\adviwait
val it : goalstack = No subgoals\medskip
#
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{lemmas and tactics}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
# \green{NSUM_CLAUSES_NUMSEG;;}
val it : thm =
  \red{|- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\\
     (!m n.
          nsum (m..SUC n) f =
          (if m <= SUC n then nsum (m..n) f + f (SUC n) else nsum (m..n) f))}\toolong
# \adviwait\green{INDUCT_TAC;;}
val it : tactic = <fun>
# \green{ASM_REWRITE_TAC;;}
val it : thm list -> tactic = <fun>
# \green{ARITH_TAC;;}
val it : tactic = <fun>
#
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example: in the file}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
\advirecord{f7}{let \green{\advirecord{f6}{ARITHMETIC_PROGRESSION_SIMPLE}} = prove
 (\red{\advirecord{f1}{`!n. nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2`}},
  \gray{\advirecord{f5}{\advirecord{f2}{INDUCT_TAC} THEN \advirecord{f3}{ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]} THEN
  \advirecord{f4}{ARITH_TAC}}});;}
\end{alltt}
\endgroup
\vss}
\adviplay{f1}
\adviplay{f2}
\adviplay{f3}
\adviplay{f4}
\adviplay{f5}
\adviplay{f6}
\adviplay{f7}
\adviwait
\adviplay[slidegreen]{f1}
\adviplay[slidegreen]{f2}
\adviplay[slidegreen]{f3}
\adviplay[slidegreen]{f4}
\adviwait
\adviplay[slidered]{f1}
\adviplay[slidegray]{f2}
\adviplay[slidegray]{f3}
\adviplay[slidegray]{f4}
\adviplay[slidegray]{f5}
\adviplay[slidegreen]{f6}
\adviplay{f7}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar}
\slidetitle{overview}
\vspace{-1.4em}
\vbox to 0pt{
\vspace{-1.4em}
\hfill\includegraphics[height=10em]{/home/freek/papers/cursus/pics/andrzej.eps}\strut
\vss
}
1973$\,$--$\,$today \\
\textbf{Andrzej Trybulec} \\
Bia\l ystok, Poland
\medskip
%\adviwait

first order logic $+$ \\
\green{Tarski-Grothendieck set theory} \\
$=$ ZFC $+$ arbitrarily large inaccessible cardinals
\medskip
\adviwait

\red{very nice natural language-like proof language} \\
very nice type system
\medskip
\adviwait

\red{MML $=$ Mizar Mathematical Library} \\
2.2 million lines of code, 55 thousand lemmas

\vspace{-3pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
theorem \green{\advirecord{g12d}{Th1:}}
  \red{\advirecord{g1}{(for i holds s.i = i) implies for n holds Partial_Sums(s).n = n*(n + 1)/2}}\toolong
proof
  \blue{\advirecord{g}{\advirecord{g2}{assume
\advirecord{g2a}{A1:} for i holds s.i = i};
  \advirecord{g3}{defpred X[Element of NAT] means Partial_Sums(s).$1 = $1*($1 + 1)/2};
  \advirecord{g4}{Partial_Sums(s).0 = s.0 \advirecord{g4a}{by \advirecord{g12a}{SERIES_1:def 1}}
    .= 0*(0 + 1)/2 \advirecord{g4b}{by A1}};
  \advirecord{g5a}{then}
\advirecord{g13a}{A2}: \advirecord{g5}{X[0]};
\advirecord{g13b}{A3}: \advirecord{g10}{\advirecord{g6a}{now} \advirecord{g7a}{let n};
    \advirecord{g7b}{assume X[n]};
    then \advirecord{g8}{Partial_Sums(s).(n + 1) = n*(n + 1)/2 + s.(n + 1) \advirecord{g8a}{by \advirecord{g12b}{SERIES_1:def 1}}\toolong
      .= n*(n + 1)/2 + (n + 1) \advirecord{g8b}{by A1}};
    \advirecord{g9}{hence X[n + 1]};
  \advirecord{g6b}{end};}
  thus \advirecord{g11}{for n holds X[n]} from \advirecord{g12c}{NAT_1:sch 1}(\advirecord{g13c}{A2},\advirecord{g13d}{A3});}}
end;
\end{alltt}
\endgroup
\vss}
\adviplay{g}
\adviplay{g1}
\adviplay{g2}
\adviplay{g2a}
\adviplay{g3}
\adviplay{g4}
\adviplay{g4a}
\adviplay{g4b}
\adviplay{g5a}
\adviplay{g5}
\adviplay{g6a}
\adviplay{g6b}
\adviplay{g7a}
\adviplay{g7b}
\adviplay{g8}
\adviplay{g8a}
\adviplay{g8b}
\adviplay{g9}
\adviplay{g10}
\adviplay{g11}
\adviplay{g12a}
\adviplay{g12b}
\adviplay{g12c}
\adviplay{g12d}
\adviplay{g13a}
\adviplay{g13b}
\adviplay{g13c}
\adviplay{g13d}
\adviwait
\adviplay[slidered]{g1}
\adviwait
\adviplay{g1}
\adviplay[slidered]{g2}
\adviplay{g2a}
\adviwait
\adviplay{g2}
\adviplay[slidered]{g3}
\adviwait
\adviplay{g3}
\adviplay[slidered]{g4}
\adviplay{g4a}
\adviplay{g4b}
\adviwait
\adviplay{g4}
\adviplay{g4a}
\adviplay{g4b}
\adviplay[slidered]{g5a}
\adviplay[slidered]{g5}
\adviwait
\adviplay{g5a}
\adviplay{g5}
\adviplay[slidered]{g6a}
\adviplay[slidered]{g6b}
\adviwait
\adviplay{g6a}
\adviplay{g6b}
\adviplay[slidered]{g7a}
\adviplay[slidered]{g7b}
\adviwait
\adviplay{g7a}
\adviplay{g7b}
\adviplay[slidered]{g8}
\adviplay{g8a}
\adviplay{g8b}
\adviwait
\adviplay{g8}
\adviplay{g8a}
\adviplay{g8b}
\adviplay[slidered]{g9}
\adviwait
\adviplay[slidegreen]{g6a}
\adviplay[slidegreen]{g6b}
\adviplay[slidegreen]{g7a}
\adviplay[slidegreen]{g7b}
\adviplay[slidegreen]{g8}
\adviplay[slidegreen]{g8a}
\adviplay[slidegreen]{g8b}
\adviplay[slidegreen]{g9}
\adviplay[slidegreen]{g10}
\adviplay[slidegreen]{g12b}
%\adviwait
\adviplay{g6a}
\adviplay{g6b}
\adviplay{g7a}
\adviplay{g7b}
\adviplay{g8}
\adviplay{g8a}
\adviplay{g8b}
\adviplay{g9}
\adviplay{g10}
\adviplay{g12b}
\adviplay[slidered]{g11}
\adviplay[slideblue]{g13a}
\adviplay[slideblue]{g13b}
\adviplay[slideblue]{g13c}
\adviplay[slideblue]{g13d}
\adviwait
\adviplay{g11}
\adviplay{g13a}
\adviplay{g13b}
\adviplay{g13c}
\adviplay{g13d}
\adviwait
\adviplay[slidegreen]{g12a}
\adviplay[slidegreen]{g12b}
\adviplay[slidegreen]{g12c}
%\adviplay[slidegreen]{g12d}

\vfill
\end{slide}

\begin{slide}
\slidetitle{lemmas}
\begin{alltt}\footnotesize
definition
  let s be Real_Sequence;
  func Partial_Sums(s) -> Real_Sequence means
\green{:: SERIES_1:def 1}
    \red{it.0 = s.0 & for n holds it.(n + 1) = it.n + s.(n + 1)};
end;
\end{alltt}
\medskip
\adviwait
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}\footnotesize
scheme \green{:: NAT_1:sch 1}
  Ind \{ P[Nat] \} : \red{for k being Element of NAT holds P[k]}
provided
  \red{P[0]}
and
  \red{for k being Element of NAT st P[k] holds P[k + 1]};
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the best of both worlds}
\slidetitle{a proof assistant that is not \textbf{too} frustrating}
\adviwait\red{\advirecord{h1}{{\small HOL}}, \green{\advirecord{h2}{Isabelle,}} \red{\advirecord{h3}{Coq, Mizar}}}
\adviplay{h1}\adviplay{h2}\adviplay{h3}\adviwait\\
\adviplay[slidered]{h1}\adviplay[slidegreen]{h2}\adviplay[slidered]{h3}%
I know three intimately\adviwait\\
\blue{they are all frustrating in different ways\adviwait}
\bigskip

\begin{itemize}
\item[$\bullet$]
\textbf{just learn Isabelle\exclspace!}
$$\green{\mbox{Isabelle} = \mbox{{\small HOL}-like system} + \mbox{Mizar-like proofs}}\adviwait$$
%\blue{probably neither {\small HOL}-like nor Mizar-like enough for me}
\blue{does not \textbf{integrate} the procedural and declarative proof styles} % \adviwait (yet)}

\medskip
\adviwait
\item[$\bullet$]
\textbf{build an $(n + 1)\,$st system\exclspace!}

%(why should I think I can do better?)

\smallskip
\adviwait
\item[$\bullet$]
\textbf{improve an existing system\exclspace!}
%\adviwait
%
%making HOL more Mizar-like? \adviwait
%making Mizar more HOL-like?
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{current attempt: improve {\small HOL}\exclspace!}
\vspace{0pt}

\begin{center}
\gray{\advirecord{i5}{yet another} Mizar-style proof language on top of {\small HOL} Light\qquad\strut} \\
\red{\advirecord{i}{Mizar-style proofs as \textbf{first class objects}}} \\
\red{\advirecord{i4}{Mizar-style \textbf{user interface}}}
\adviwait
\adviplay[slidegray]{i5}
\end{center}
\bigskip
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{`A Mizar Mode for {\small HOL}}' by \green{John Harrison}\hfill \blue{{\small TPHOL}s {1996}}%\\
%\advirecord{i1}{{\small\texttt{Examples/mizar.ml}}}

\item[$\bullet$]
\textbf{Mizar Light}\hfill \blue{{\small TPHOL}s {2001}}

\item[$\bullet$]
\textbf{Mizar Light II}\hfill \gray{unpublished}%\\
%\advirecord{i2}{{\small\texttt{Mizarlight/miz2a.ml}}}

\item[$\bullet$]
\textbf{`Changing proof style'} by \green{John Harrison}\hfill \blue{{\small HOL} Light tutorial}%\\
%\advirecord{i3}{{\small\texttt{Tutorial/Changing\char`\_proof\char`\_style.ml}}}

\item[$\bullet$]
\textbf{\red{Mizar Light III}}%\hfill \red{new\exclspace!}%
%\adviwait
%\adviplay[slidegreen]{i1}%
%\adviplay[slidegreen]{i2}%
%\adviplay[slidegreen]{i3}%
\adviwait
\adviplay[slidered]{i}%
\adviwait
\adviplay[slidered]{i4}%

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{evolution of Mizar Light syntax}
\begin{itemize}
\small
\item[$\bullet$]
\textbf{Mizar Light}
\begin{alltt}\footnotesize
\green{prove(`a ==> a`,
  ASSUME_A(0,`a:bool`) THEN
  THUS_A(1,`a:bool`) (BY [0][]));;}
\end{alltt}

\smallskip
%\adviwait
\item[$\bullet$]
\textbf{Mizar Light II}
\begin{alltt}\footnotesize
\green{theorem "a ==> a"
 [assume "a";
  hence "a"];;}
\end{alltt}

\smallskip
%\adviwait
\item[$\bullet$]
\textbf{Mizar Light III}
\begin{alltt}\footnotesize
\red{a ==> a
proof
  assume a;
  thus a;
end;}
\end{alltt}

\end{itemize}

\vspace{-9pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the example in Mizar Light}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
\green{\advirecord{j}{\red{\advirecord{j1}{!n. nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2}}
proof
  \red{\advirecord{j2}{nsum(0..0) (\\i. i) = 0}} by \black{NSUM_CLAUSES_NUMSEG};
    \red{\advirecord{j3}{.= (0*(0 + 1)) DIV 2}} [A1] by \blue{\advirecord{j8}{ARITH_TAC}};
  now let {n} be \red{\advirecord{j4}{num}};
    assume \red{\advirecord{j5}{nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2}};
    \red{\advirecord{j6}{nsum(0..SUC n) (\\i. i) = (n*(n + 1)) DIV 2 + SUC n}}
      by \black{NSUM_CLAUSES_NUMSEG},\blue{\advirecord{j12}{ARITH_RULE `{\advirecord{j11}{0 <= SUC n}}`}};
    thus \red{\advirecord{j7}{.= ((SUC n)*(SUC n + 1)) DIV 2}} by \blue{\advirecord{j9}{ARITH_TAC}};
  end;
qed by \blue{\advirecord{j10}{INDUCT_TAC}},A1;}}
\end{alltt}
\endgroup
\vss}
\vspace{12.5em}

\adviplay{j}
\adviplay{j1}
\adviplay{j2}
\adviplay{j3}
\adviplay{j4}
\adviplay{j5}
\adviplay{j6}
\adviplay{j7}
\adviplay{j8}
\adviplay{j9}
\adviplay{j10}
\adviplay{j11}
\adviplay{j12}
\adviwait
\adviplay[slidegreen]{j}%
\adviplay{j1}%
\adviplay{j2}%
\adviplay{j3}%
\adviplay{j4}%
\adviplay{j5}%
\adviplay{j6}%
\adviplay{j7}%
\adviplay{j8}%
\adviplay{j9}%
\adviplay{j10}%
\adviplay{j11}%
\adviplay{j12}%
$\bullet$ \green{Mizar proof language} \\
\adviwait
\adviplay[slidered]{j1}%
\adviplay[slidered]{j2}%
\adviplay[slidered]{j3}%
\adviplay[slidered]{j4}%
\adviplay[slidered]{j5}%
\adviplay[slidered]{j6}%
\adviplay[slidered]{j7}%
$\bullet$ \red{{\small HOL} Light statements} without quotes\exclspace! \\
\adviwait
\adviplay[slideblue]{j8}%
\adviplay[slideblue]{j9}%
\adviplay[slideblue]{j10}%
\adviplay[slideblue]{j11}%
\adviplay[slideblue]{j12}%
$\bullet$ \blue{{\small HOL} Light tactics in the justifications\exclspace!}

\adviwait
\vspace{-10em}
\vbox to 0pt{
%\vspace{3pt}
%\hfill\includegraphics[height=11.5em]{/home/freek/talks/miz3/pics/lars1.eps}\hspace{0em}
\vspace{1.2em}
\hfill\includegraphics[height=9em]{/home/freek/talks/miz3/pics/lars3.eps}\hspace{-2em}
\vss}

\vspace{-17pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{tactics in justifications?}

$$\red{\langle\mbox{statement}\rangle}\texttt{\small\ by }\blue{\langle\mbox{tactic}\rangle}\texttt{\small ,}\,\langle\mbox{theorem}\rangle\texttt{\small ,}\,\dots\texttt{\small ,}\,\green{\langle\mbox{label}\rangle\texttt{\small ,}\,\dots}\texttt{\small ;}\bigskip\medskip$$

\begin{itemize}
\item[$\bullet$]
\blue{$\langle\mbox{tactic}\rangle$} should have {\small ML} type\blue{\texttt{\small\ thm list} \texttt{\small ->} \texttt{\small tactic}}
\adviwait

\item[$\bullet$]
the step naturally corresponds to a certain \red{goal}

the \green{$\langle\mbox{label}\rangle$}s label the \green{assumptions} in that goal
\adviwait

\item[$\bullet$]
just keep the assumptions in the goal that occur in the list
\adviwait

\item[$\bullet$]
\blue{run the tactic} with both theorems and assumptions as argument
\adviwait

\item[$\bullet$]
if the tactic succeeds: turn resulting subgoals into statements

these should all be in the list

\end{itemize}

\vfill
\end{slide}

\def\hole{\char`\#}

\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\def\bar{\hbox to 0pt{\hss$|$\hss}}
\begin{alltt}\footnotesize










now
  thus \green{\bar} [A1] by {\hole};
end;
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize










now
  thus \red{\advirecord{l1}{!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2}} \advirecord{l5}{[A1] by \red{\advirecord{l2}{\hole}}\rlap{\white{\advirecord{l7}{;}}}\green{\advirecord{l8}{INDUCT_TAC}}\advirecord{l9}{;}}\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay[slidegreen]{l1}
\adviplay{l2}
\adviplay{l5}
\adviplay{l7}
\adviwait
\adviplay[slidered]{l1}
\adviplay[slidered]{l2}
\adviwait
\adviplay[white]{l7}
\adviplay[slidegreen]{l8}
\adviplay{l9}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize




now
  \advirecord{k4}{\red{\advirecord{k8}{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2}} [A1] by \red{\advirecord{k6}{\hole}};}
  \advirecord{k5}{now [A2]
    let n be num;
    assume nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A3];
    thus nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A4] by \red{\advirecord{k7}{\hole}};\toolong
  end;}
  thus \advirecord{k1}{!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2} [A5] by \advirecord{k2}{INDUCT_TAC},\advirecord{k3a}{A1},\advirecord{k3b}{A2};\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay[slidered]{k1}
\adviplay[slidegreen]{k2}
\adviplay{k3a}
\adviplay{k3b}
\adviplay{k4}
\adviplay{k5}
\adviplay{k6}
\adviplay{k7}
\adviplay{k8}
\adviwait
\adviplay{k1}
\adviplay{k2}
\adviplay[slideblue]{k3a}
\adviplay[slideblue]{k4}
\adviplay[slideblue]{k6}
\adviplay[slideblue]{k8}
%\adviwait
\adviplay{k3a}
\adviplay{k4}
\adviplay{k6}
\adviplay{k8}
\adviplay[slideblue]{k3b}
\adviplay[slideblue]{k5}
\adviplay[slideblue]{k7}
%\adviwait
\adviplay{k3b}
\adviplay{k5}
\adviplay[slidered]{k6}
\adviplay[slidered]{k7}
\adviwait
\adviplay[slidered]{k8}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize




now
  \red{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2} [A1]
    by \red{\hole}\rlap{\white{\advirecord{m3}{;}}}\advirecord{m}{\green{\advirecord{m1}{REWRITE_TAC,NSUM_CLAUSES_NUMSEG}};}
  now [A2]
    let n be num;
    assume nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A3];
    thus nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A4] by \red{\hole};\toolong
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A5] by INDUCT_TAC,A1,A2;\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay{m3}
\adviwait
\adviplay[white]{m3}
\adviplay{m}
\adviplay[slidegreen]{m1}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize



now
  \red{\advirecord{n3}{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2}} [A1] by \red{\advirecord{n1}{\hole}}\rlap{\white{\advirecord{n7}{;}}}\green{\advirecord{n8}{ARITH_TAC}}\advirecord{n9}{;}
  \advirecord{n5}{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2} [A2]
    by \advirecord{n6}{REWRITE_TAC,NSUM_CLAUSES_NUMSEG},A1;
  now [A3]
    let n be num;
    assume nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A4];
    thus nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A5] by \advirecord{n2}{\hole};\toolong
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A6] by INDUCT_TAC,A2,A3;\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay[slidered]{n5}
\adviplay[slidegreen]{n6}
\adviplay{n1}
\adviplay{n2}
\adviplay{n3}
\adviplay{n7}
\adviwait
\adviplay{n5}
\adviplay{n6}
\adviplay[slidered]{n1}
\adviplay[slidered]{n2}
%\adviwait
\adviplay[slidered]{n3}
\adviwait
\adviplay[white]{n7}
\adviplay[slidegreen]{n8}
\adviplay{n9}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize



now
  \blue{\advirecord{o3}{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2}} \blue{\advirecord{o7}{[A1]}} by \advirecord{o6}{ARITH_TAC};
  \blue{\advirecord{o4}{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2 [A2]}}
    by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
  now [A3]
    let n be num;
    assume \blue{\advirecord{o5}{nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A4]}};
    thus \red{\advirecord{o1}{nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2}} [A5] by \red{\advirecord{o2}{\hole}};\toolong
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A6] by INDUCT_TAC,A2,A3;\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay{o1}
\adviplay{o2}
\adviplay[slidered]{o3}
\adviplay{o4}
\adviplay{o5}
\adviplay[slidegreen]{o6}
\adviplay{o7}
\adviwait
\adviplay{o3}
\adviplay{o6}
\adviplay{o7}
\adviplay[slidered]{o1}
\adviplay[slidered]{o2}
\adviwait
\adviplay[slideblue]{o3}
\adviplay[slideblue]{o7}
\adviplay[slideblue]{o4}
\adviplay[slideblue]{o5}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize



now
  \blue{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 [A1]} by ARITH_TAC;
  \blue{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2 [A2]}
    by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
  now [A3]
    let n be num;
    assume \blue{nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A4]};
    thus \red{nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2} [A5]
      by \red{\hole}\rlap{\white{\advirecord{p1}{;}}}\green{\advirecord{p2}{REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4}}\advirecord{p3}{;}
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A6] by INDUCT_TAC,A2,A3;\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay{p1}
\adviwait
\adviplay[white]{p1}
\adviplay[slidegreen]{p2}
\adviplay{p3}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize

now
  \blue{\advirecord{q3}{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 [A1]}} by ARITH_TAC;
  \blue{\advirecord{q4}{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2 [A2]}}
    by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
  now [A3]
    let n be num;
    assume \blue{\advirecord{q5}{nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A4]}};
    \red{\advirecord{q1}{(if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2 =\toolong
      (SUC n * (SUC n + 1)) DIV 2}} [A5] by \red{\advirecord{q2}{\hole}}\rlap{\white{\advirecord{q8}{;}}}\green{\advirecord{q9}{ARITH_TAC}}\advirecord{q10}{;}
    thus \advirecord{q6}{nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2} [A6]
      by \advirecord{q7}{REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4},A5;
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 [A7] by INDUCT_TAC,A2,A3;\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay{q1}
\adviplay{q2}
\adviplay{q3}
\adviplay{q4}
\adviplay{q5}
\adviplay[slidered]{q6}
\adviplay[slidegreen]{q7}
\adviplay{q8}
\adviwait
\adviplay{q6}
\adviplay{q7}
\adviplay[slidered]{q1}
\adviplay[slidered]{q2}
\adviplay[slideblue]{q3}
\adviplay[slideblue]{q4}
\adviplay[slideblue]{q5}
\adviwait
\adviplay[white]{q8}
\adviplay[slidegreen]{q9}
\adviplay{q10}

\vfill
\end{slide}

\addtocounter{slide}{-1}
\begin{slide}
\slidetitle{growing a proof procedurally}
\vbox to 0pt{
\vspace{-1.98em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize

now
  \advirecord{r1}{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2} \lightgray{\advirecord{r6}{[A1]}} \lightgray{\advirecord{r7}{by ARITH_TAC}};
  \advirecord{r2}{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2} \lightgray{\advirecord{r8}{[A2]}}
    \lightgray{\advirecord{r9}{by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1}};
  now \lightgray{\advirecord{r10}{[A3]}}
    let n be num;
    \advirecord{r3}{assume nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2} \lightgray{\advirecord{r14}{[A4]}};
    \advirecord{r4}{(if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2 =\toolong
      (SUC n * (SUC n + 1)) DIV 2} \lightgray{\advirecord{r16}{[A5]}} \lightgray{\advirecord{r11}{by}} \lightgray{\advirecord{r5}{ARITH_TAC}};
    thus nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2 \lightgray{\advirecord{r12}{[A6]
      by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4,A5}};
  end;
  thus !n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2 \lightgray{\advirecord{r15}{[A7]}} \lightgray{\advirecord{r13}{by INDUCT_TAC,A2,A3}};\toolong
end;
\end{alltt}
\endgroup
\vss}
\adviplay{r1}
\adviplay{r2}
\adviplay{r3}
\adviplay[slidered]{r4}
\adviplay[slidegreen]{r5}
\adviplay{r6}
\adviplay{r7}
\adviplay{r8}
\adviplay{r9}
\adviplay{r10}
\adviplay{r11}
\adviplay{r12}
\adviplay{r13}
\adviplay{r14}
\adviplay{r15}
\adviplay{r16}
\adviwait
\adviplay{r1}
\adviplay{r2}
\adviplay{r3}
\adviplay{r4}
\adviplay{r5}
\adviplay{r6}
\adviplay{r7}
\adviplay{r8}
\adviplay{r14}
\adviwait
\adviplay[slidelightgray]{r5}
\adviplay[slidelightgray]{r6}
\adviplay[slidelightgray]{r7}
\adviplay[slidelightgray]{r8}
\adviplay[slidelightgray]{r9}
\adviplay[slidelightgray]{r10}
\adviplay[slidelightgray]{r11}
\adviplay[slidelightgray]{r12}
\adviplay[slidelightgray]{r13}
\adviplay[slidelightgray]{r14}
\adviplay[slidelightgray]{r15}
\adviplay[slidelightgray]{r16}
\adviwait
\adviplay[slideblue]{r4}
\adviplay[slideblue]{r1}

\vfill
\end{slide}

\begin{slide}
\slidetitle{text typed while `growing' the proof}
\begingroup
\def\\{\char`\\}%
\def\menu{}%
%\vspace{-1.98em}
\begin{alltt}\footnotesize
\strut\red{!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2}\menu
\green{INDUCT_TAC\menu
REWRITE_TAC,NSUM_CLAUSES_NUMSEG\menu
ARITH_TAC\menu
REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4\menu
ARITH_TAC\menu}
\end{alltt}
\endgroup
\bigskip
\adviwait

\gray{this corresponds to the traditional session:}
\begin{alltt}\footnotesize
\strut\gray{g \red{`!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`};;
e \green{INDUCT_TAC};;
e (\green{ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]});;
e \green{ARITH_TAC};;
e (\green{ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]});;
e \green{ARITH_TAC};;}
\end{alltt}

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

\begin{slide}
\slidetitle{merging the declarative and procedural proof styles}
two ways of working on a Mizar Light proof:
\begin{itemize}
\smallskip
\item[$\bullet$]
\textbf{the declarative way}: free form text editing \\
\green{just type and edit the proof yourself}
\medskip

\item[$\bullet$]
\textbf{the procedural way}:\\
\green{generate new steps by executing a tactic at an unjustified line}

\end{itemize}
\bigskip
\adviwait

\red{both freely mixed}
\medskip
\adviwait

\textbf{\red{not two `modes' in the proof script}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar-style error messages}
\vbox to 0pt{
\vspace{-1.65em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
\strut\white{\advirecord{s}{!n. nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2
proof
  nsum(0..0) (\\i. i) = (0*(0 + 1)) DIV 2;
  now let n be nat;
    assume nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2;
    thus nsum(0..SUC n) (\\i. i) = ((SUC n)*(SUC n + 1)) DIV 2 by #;
  end;
qed;}}
\end{alltt}
\endgroup
\vss}
\adviplay[slidegray]{s}
\adviwait
\adviplay[white]{s}
\vbox to 0pt{
\vspace{-4.25em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
!n. nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2
proof
  nsum(0..0) (\\i. i) = (0*(0 + 1)) DIV 2;
\green{::                                      #1}
  now let n be nat;
\green{::                #6}
    assume nsum(0..n) (\\i. i) = (n*(n + 1)) DIV 2;
    thus nsum(0..SUC n) (\\i. i) = ((SUC n)*(SUC n + 1)) DIV 2 by \red{#};
  end;
qed;
\green{:: #1}
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{porting formal mathematics}
\slidetitle{formalization for the future}
currently, {when a proof assistant dies its mathematical library dies} \\
\adviwait
\blue{formal proof languages should be \textbf{generic}}
\medskip
\adviwait

{three approaches to porting formal mathematics:}
\begin{itemize}
\smallskip
\item[$\bullet$]
\textsl{convert the low-level `proof objects'} \\
\adviwait
\green{works}\adviwait, but \red{no converted proofs on the user-level}
\adviwait

\smallskip
\item[\gray{\advirecord{t3}{$\bullet$}}\adviplay{t3}]
\gray{\advirecord{t1}{\textsl{port procedural scripts using similar tactics in the other system\toolong}}} \\
\gray{\advirecord{t2}{does not work}}

\adviplay{t1}
\adviwait
\adviplay[slidered]{t2}
\adviwait
\adviplay[slidegray]{t1}
\adviplay[slidegray]{t2}
\adviplay[slidegray]{t3}
\adviwait

\smallskip
\item[$\bullet$]
\textsl{port declarative scripts by just translating the statements} \\
\blue{all declarative proof languages are basically the same\exclspace!} \\
\green{works} \adviwait\red{approximately\adviwait,} but \green{\textsl{with converted proofs on the user-level\exclspace!\toolong}}

\end{itemize}

\vspace{-11pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the HOL Light example (repeat)}
\vbox to 0pt{
\vspace{-1.2em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
let ARITHMETIC_PROGRESSION_SIMPLE = prove
 (`!n. nsum(1..n) (\\i. i) = (n*(n + 1)) DIV 2`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
  ARITH_TAC);;
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Mizar Light conversion of the HOL Light example}
\vbox to 0pt{
\vspace{-1.65em}
\begingroup
\def\\{\char`\\}
\begin{alltt}\footnotesize
\strut\red{!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2}
proof
  \red{(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2} by \green{ARITH_TAC};
  \red{nsum (1..0) (\\i. i) = (0 * (0 + 1)) DIV 2} [A1]
    by \green{ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]};
  \red{!n. nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2
      ==> nsum (1..SUC n) (\\i. i) = (SUC n * (SUC n + 1)) DIV 2}
  proof
    let n be num;
    \red{assume nsum (1..n) (\\i. i) = (n * (n + 1)) DIV 2} [A2];
    \red{(if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =\toolong
      (SUC n * (SUC n + 1)) DIV 2} by \green{ARITH_TAC};
  qed by \green{ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]},A2;
qed by \green{INDUCT_TAC},A1;
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Mizar example (repeat)}
\vbox to 0pt{
\vspace{-1.65em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
{\strut}theorem
  (for i holds s.i = i) implies for n holds Partial_Sums(s).n = n*(n + 1)/2\toolong
proof
  assume
A1: for i holds s.i = i;
  defpred X[Element of NAT] means Partial_Sums(s).$1 = $1*($1 + 1)/2;
  Partial_Sums(s).0 = s.0 by SERIES_1:def 1
    .= 0*(0 + 1)/2 by A1;
  then
A2: X[0];
A3: now let n;
    assume X[n];
    then Partial_Sums(s).(n + 1) = n*(n + 1)/2 + s.(n + 1) by SERIES_1:def 1\toolong
      .= n*(n + 1)/2 + (n + 1) by A1
    hence X[n + 1];
  end;
  thus for n holds X[n] from NAT_1:sch 1(A2,A3);
end;
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Mizar Light conversion of the Mizar example}
\vbox to 0pt{
\vspace{-1.65em}
\begingroup
\def\\{\char`\\}%
\begin{alltt}\footnotesize
{\strut}\red{!s. (!i. s i = i) ==> !n. nsum(0..n) s = (n*(n + 1)) DIV 2}
proof
  let s be \red{num->num};
  assume \red{!i. s i = i} [A1];
  \blue{set {X = {\\n. (nsum(0..n) s = (n*(n + 1)) DIV 2)}};}
  \red{nsum(0..0) s = s 0} by \green{NSUM_CLAUSES_NUMSEG'};
    \gray{.= 0} by A1;
    \red{.= 0*(0 + 1) DIV 2} \gray{by ARITH_TAC};
  \red{X 0} [A2];
  now [A3] let n be \red{num};
    assume \red{X n};
    \red{nsum(0..n + 1) s = (n*(n + 1)) DIV 2 + s (n + 1)} by \green{NSUM_CLAUSES_NUMSEG'};\toolong
      \red{.= (n*(n + 1)) DIV 2 + (n + 1)} by A1;
    thus \red{X (n + 1)} \gray{by ARITH_TAC};
  end;
  \red{!n. X n} by \gray{MATCH_MP_TAC},\green{num_INDUCTION'},A2,A3;
qed;
\end{alltt}
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{outlook}
\slidetitle{Mizar Light III is not \textbf{just} vaporware$\,$\dots}
implementation currently just starting
\medskip
\adviwait

\blue{what is there:}
\begin{itemize}
\item[$\bullet$]
\green{parser and checker} (including tactics in the justifications$\exclspace$!)

\item[$\bullet$]
\red{all examples in this talk are processed correctly}

\end{itemize}
\medskip
\adviwait

\blue{what is not there \adviwait (yet):\adviwait}
\begin{itemize}
\item[$\bullet$]
proper error messages

\item[$\bullet$]
a Mizar-style user interface

\item[$\bullet$]
\green{`growing' a proof by executing tactics}

\item[$\bullet$]
conversion from procedural {\small HOL} Light or Mizar \adviwait (or other systems)

\end{itemize}

\vspace{-17pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the history and future of mathematics}

\begin{tabular}{c}
\includegraphics[height=8em]{/home/freek/talks/miz3/pics/euclid.eps} \\
Euclid \\
\textbf{proof}
\end{tabular}\adviwait\hfill
\begin{tabular}{c}
\includegraphics[height=8em]{/home/freek/talks/miz3/pics/cauchy.eps} \\
Cauchy \\
\textbf{rigor}
\end{tabular}\adviwait\hfill
\begin{tabular}{c}
\includegraphics[height=8em]{/home/freek/talks/miz3/pics/debruijn.eps} \\
de Bruijn \\
\red{\textbf{formality}}
\end{tabular}\hspace{0em}
\bigskip
\smallskip
\adviwait

\blue{needed for this third revolution of \red{formality} to happen:}
\begin{itemize}
\item[$\bullet$]
\green{formalization should be much closer to traditional mathematics}
\adviwait

\item[$\bullet$]
\green{full automation of high school mathematics}

\end{itemize}

\vspace{-4pt}
\vfill
\end{slide}

\end{document}