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

\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}
\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{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large integrating Coq-style and Mizar-style proof}

Freek Wiedijk \\
Radboud University Nijmegen

%small Types workshop \\
\red{High Level Languages for Proofs} \\
LAMA, Universit\'e de Savoie \\ near Chamb\'ery \\
2005 04 13, 11:30
\end{slide}

\begin{slide}
\sectiontitle{intro}
\slidetitle{outline of the talk}

\begin{enumerate}
\item
why not be happy with the proof languages that we already have?
\smallskip
%\adviwait

\item
\textbf{`formal proof sketches'}

formal proofs that can be read like normal mathematical proofs
\smallskip
%\adviwait

\item
\textbf{\red{`luxury mathmode'}}

formal proofs that can be written in a mixture of the Coq-way \\ and the Mizar-way

\end{enumerate}

\vfill
\end{slide}

\begin{slide}
\slidetitle{requirements for a formal proof language}

\begin{itemize}
\item[$\bullet$]
\strut\advirecord{a1}{\strut\rlap{\hspace{5cm}(yes, you forgot!)}}\advirecord{a0}{writing proofs}\adviplay{a0}

\item[$\bullet$]
\strut\advirecord{a2}{\strut\rlap{\hspace{5cm}`readable'}}reading proofs

\item[$\bullet$]
\strut\advirecord{a3}{\strut\rlap{\hspace{5cm}`robust'}}modifying proofs

\item[$\bullet$]
\strut\advirecord{a4}{\strut\rlap{\hspace{5cm}`portable'}}porting proofs
\adviwait

\begin{itemize}
\smallskip
\item
between different systems

\item
between different versions of the same system

\vfill
\end{itemize}

\adviwait
\adviplay[slidegreen]{a3}
\adviwait
\adviplay[slidegreen]{a2}
\adviwait
\adviplay[slidegreen]{a4}
\adviwait
\adviplay[slidered]{a0}

\end{itemize}

\end{slide}

\begin{slide}
\sectiontitle{why more than Mizar?}
\slidetitle{automatically determining the statements}
\begin{itemize}
\item[$\bullet$]
\textbf{intros versus let/assume}

\begin{alltt}
\green{theorem} \advirecord{c1}{even n} -> \advirecord{c2}{odd n} -> False
\green{proof}
  \advirecord{a3}{\rlap{intros.}}\advirecord{a1}{assume \advirecord{b1}{even n};}
  \advirecord{a2}{assume \advirecord{b2}{odd n};}
\end{alltt}
\adviplay{c1}
\adviplay{c2}
\adviwait
\adviplay{a1}
\adviplay[slidered]{b1}
\adviplay[slidered]{c1}
\adviwait
\adviplay{a2}
\adviplay[slidered]{b2}
\adviplay[slidered]{c2}
\adviwait
\adviplay[white]{a1}
\adviplay[white]{a2}
\adviplay[white]{b1}
\adviplay[white]{b2}
\adviplay[slideblue]{a3}
\adviwait
\vspace{-.8\bigskipamount}

\item[$\bullet$]
\textbf{calculating the cases for a proof by induction}
\adviwait
\medskip

\item[$\bullet$]
\textbf{backward chaining and rewriting}

\begin{alltt}\smallskip
  \blue{apply.}\smallskip
  \blue{rewrite.}
\end{alltt}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{why more than \rlap{Coq?}\phantom{Mizar?}}
\slidetitle{informal proof}
%Hardy \& Wright, \green{An Introduction to the Theory of Numbers}%: \textbf{7 lines}
%\medskip
\vspace{-\medskipamount}

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}
\begin{center}
\setlength{\fboxsep}{.5em}
$\hspace{-2em}$\color{slidegray}\framebox{\color{black}\hspace{.1em}\parbox{\linewidth}{
\textbf{Theorem 43 (Pythagoras' theorem).} {$\sqrt{2}$ is irrational.}
\medskip

\rightskip=0pt
The traditional proof ascribed to Pythagoras runs
as follows.  If $\sqrt{2}$ is rational, then the equation
$$a^2 = 2b^2 \eqno{\textsf{(4.3.1)}}$$
is soluble in integers $a$, $b$ with $(a,b) = 1$.  Hence $a^2$ is even, and there%-
fore $a$ is even.  If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even,
contrary to the hypothesis that $(a,b) = 1$.
\hfill$\Box$%
\smallskip
}\hspace{.3em}\color{slidegray}}\color{black}$\hspace{-2em}$
\end{center}
\end{quote}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{`formal proof sketch'}
%\green{exactly same reasoning, using Mizar syntax}
%\medskip
\vspace{-\medskipamount}

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}\small
\advirecord{a1}{\textbf{theorem} Th43: sqrt 2 is irrational} \\
\advirecord{a2}{\textbf{proof}} \\
\advirecord{a3}{\quadskip \textbf{assume} sqrt 2 is rational\textbf{;}} \\
\advirecord{a4}{\quadskip \textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}} \\
\advirecord{a5}{4\_3\_1: a\char`^2 = 2$\,*\,$b\char`^2 \textbf{and}} \\
\advirecord{a6}{\quadskip\quadskip a,b are\_relative\_prime\textbf{;}} \\
\advirecord{a7}{\quadskip a\char`^2 is even\textbf{;}} \\
\advirecord{a8}{\quadskip a is even\textbf{;}} \\
\advirecord{a9}{\quadskip \textbf{consider} c \textbf{such that} a = 2$\,*\,$c\textbf{;}} \\
\advirecord{a10}{\quadskip 4$\,*\,$c\char`^2 = 2$\,*\,$b\char`^2\textbf{;}} \\
\advirecord{a11}{\quadskip 2$\,*\,$c\char`^2 = b\char`^2\textbf{;}} \\
\advirecord{a12}{\quadskip b is even\textbf{;}} \\
\advirecord{a13}{\quadskip \textbf{thus} contradiction\textbf{;}} \\
\advirecord{a14}{\textbf{end;}}
\end{quote}
\adviplay{a1}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviplay{a5}
\adviplay{a6}
\adviplay{a7}
\adviplay{a8}
\adviplay{a9}
\adviplay{a10}
\adviplay{a11}
\adviplay{a12}
\adviplay{a13}
\adviplay{a14}
\vss
}
\adviwait
\vbox to 0pt{
\vspace{-2.2\bigskipamount}
\begin{quote}
\rightskip=0pt
\advirecord{b1}{\textbf{theorem} Th43: {sqrt 2 is irrational} $\,$:: \textbf{Pythagoras' theorem}}
\medskip

\advirecord{b2}{\textbf{proof}$\,$} \advirecord{b3}{assume sqrt 2
is rational;} \advirecord{b4}{consider $a,b$ such that}
\advirecord{b5}{$$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$
and} \advirecord{b6}{$a,b$ are\_relative\_prime;} \advirecord{b7}{$a\mathbin{\hat{}}2$ is even;}
\advirecord{b8}{$a$ is even;} \advirecord{b9}{consider $c$ such that $a = 2\mathbin{*}c$;} \advirecord{b10}{$4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$;} \advirecord{b11}{$2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$;} \advirecord{b12}{$b$ is
even;} \advirecord{b13}{thus contradiction;} \hfill \advirecord{b14}{end;}
\end{quote}
\adviplay[white]{a1}\adviplay{b1}\adviwait[.8]
\adviplay[white]{a2}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a3}\adviplay{b3}\adviplay{b2}\adviwait[.8]
\adviplay[white]{a4}\adviplay{b4}\adviwait[.8]
\adviplay[white]{a5}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a6}\adviplay{b6}\adviplay{b5}\adviwait[.8]
\adviplay[white]{a7}\adviplay{b7}\adviwait[.8]
\adviplay[white]{a8}\adviplay{b8}\adviwait[.8]
\adviplay[white]{a9}\adviplay{b9}\adviwait[.8]
\adviplay[white]{a10}\adviplay{b10}\adviwait[.8]
\adviplay[white]{a11}\adviplay{b11}\adviwait[.8]
\adviplay[white]{a12}\adviplay{b12}\adviwait[.8]
\adviplay[white]{a13}\adviplay{b13}\adviwait[.8]
\adviplay[white]{a14}\adviplay{b14}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{full formalization}
%\green{filling out the formal proof sketch to a checkable Mizar text}
%\medskip
\vspace{-1.4\medskipamount}

\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c1}{\textbf{theorem} Th43: sqrt 2 is irrational}\\
\advirecord{c2}{\textbf{proof}}\\
\advirecord{c3}{\quad \textbf{assume} sqrt 2 is rational\textbf{;}}\\
\advirecord{c4}{\quad \textbf{then} }\advirecord{c5}{\textbf{consider} a\textbf{,}{\tiny $\,$}b \textbf{such that}}\\
\advirecord{c6a}{A1: }\advirecord{c6b}{b {\tiny \raise.8pt\hbox{$<>$}} 0 \textbf{and}}\\
\advirecord{c7a}{A2: }\advirecord{c7b}{sqrt 2 = a/b \textbf{and}}\\
\advirecord{c8}{A3: }\advirecord{c9}{a,{\tiny $\,$}b are\_relative\_prime}\advirecord{c10a}{ \textbf{by} Def1}\advirecord{c10b}{\textbf{;}}\\
\advirecord{c11a}{A4: }\advirecord{c11b}{b\^{}2 {\tiny \raise.8pt\hbox{$<>$}} 0}\advirecord{c11c}{ \textbf{by} A1,{\tiny $\,$}{\tiny SQUARE\_}1:73}\advirecord{c11d}{\textbf{;}}\\
\advirecord{c12a}{\quad 2 = (a/b)\^{}2}\advirecord{c12b}{ \textbf{by} A2,{\tiny $\,$}{\tiny SQUARE\_}1:def 4}\\
\advirecord{c13a}{\qquad .= a\^{}2/b\^{}2}\advirecord{c13b}{ \textbf{by} {\tiny SQUARE\_}1:69}\advirecord{c13c}{\textbf{;}}\\
\advirecord{c14}{\quad \textbf{then}}\\
\advirecord{c15}{4\_3\_1: a\^{}2 = 2$\,*\,$b\^{}2}\advirecord{c16}{ \textbf{by} A4,{\tiny $\,$}{\tiny REAL\_}1:43}\advirecord{c17}{\textbf{;}}\\
\advirecord{c18}{\quad a\^{}2 is even}\advirecord{c19}{ \textbf{by} 4\_3\_1,{\tiny $\,$}{\tiny ABIAN}:def 1}\advirecord{c20}{\textbf{;}}\\
\advirecord{c21}{\quad \textbf{then}}\\
\advirecord{c22}{A5: }\advirecord{c23}{a is even}\advirecord{c24}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c25}{\textbf{;}}\\
\blue{:: \textbf{continue in next column}}
\end{flushleft}
}\hfill\parbox{15em}{
\begin{flushleft}\scriptsize
\advirecord{c26}{\quad \textbf{then} }\advirecord{c27}{\textbf{consider} c \textbf{such that}} \\
\advirecord{c28}{A6: }\advirecord{c29}{a = 2$\,*\,$c}\advirecord{c30}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c31}{\textbf{;}} \\
\advirecord{c32}{A7: }\advirecord{c33}{4$\,*\,$c\^{}2 =}\advirecord{c34}{ (2$\,*\,$2)$\,*\,$c\^{}2}\\
\advirecord{c35a}{\qquad .= 2\^{}2$\,*\,$c\^{}2}\advirecord{c35b}{ \textbf{by} {\tiny SQUARE\_}1:def 3}\\
\advirecord{c36}{\qquad .= }\advirecord{c37}{2$\,*\,$b\^{}2}\advirecord{c38}{ \textbf{by} A6,{\tiny $\,$}4\_3\_1,{\tiny $\,$}{\tiny SQUARE\_}1:68}\advirecord{c39}{\textbf{;}}\\
\advirecord{c40a}{\quad 2$\,*\,$(2$\,*\,$c\^{}2) = (2$\,*\,$2)$\,*\,$c\^{}2}\advirecord{c40b}{ \textbf{by} {\tiny AXIOMS}:16}\\
\advirecord{c41a}{\qquad .= 2$\,*\,$b\^{}2}\advirecord{c41b}{ \textbf{by} A7}\advirecord{c41c}{\textbf{;}}\\
\advirecord{c42}{\quad \textbf{then} }\advirecord{c43}{2$\,*\,$c\^{}2 = b\^{}2}\advirecord{c44}{ \textbf{by} {\tiny REAL\_}1:9}\advirecord{c45}{\textbf{;}}\\
\advirecord{c46a}{\quad \textbf{then} }\advirecord{c46b}{b\^{}2 is even}\advirecord{c46c}{ \textbf{by} {\tiny ABIAN}:def 1}\advirecord{c46d}{\textbf{;}}\\
\advirecord{c47}{\quad \textbf{then} }\advirecord{c48}{b is even}\advirecord{c49}{ \textbf{by} {\tiny PYTHTRIP}:2}\advirecord{c50}{\textbf{;}}\\
\advirecord{c51a}{\quad \textbf{then} }\advirecord{c51b}{2 divides a \& 2 divides b}\advirecord{c51c}{ \textbf{by} A5,{\tiny $\,$}Def2}\advirecord{c51d}{\textbf{;}}\\
\advirecord{c52}{\quad \textbf{then}}\\
\advirecord{c53a}{A8: }\advirecord{c53b}{2 divides a gcd b}\advirecord{c53c}{ \textbf{by} {\tiny INT\_}2:33}\advirecord{c53d}{\textbf{;}}\\
\advirecord{c54a}{\quad a gcd b = 1}\advirecord{c54b}{ \textbf{by} A3,{\tiny $\,$}{\tiny INT\_}2:def 4}\advirecord{c54c}{\textbf{;}}\\
\advirecord{c55}{\quad \textbf{hence} contradiction}\advirecord{c56}{ \textbf{by} A8,{\tiny $\,$}{\tiny INT\_}2:17}\advirecord{c57}{\textbf{;}}\\
\advirecord{c58}{\textbf{end;}}
\end{flushleft}
}
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay{c5}
\adviplay{c9}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c23}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviplay{c33}
\adviplay{c37}
\adviplay{c39}
\adviplay{c43}
\adviplay{c45}
\adviplay{c48}
\adviplay{c50}
\adviplay{c55}
\adviplay{c57}
\adviplay{c58}
\adviwait
\adviplay[slidegreen]{c6b}
\adviplay[slidegreen]{c7b}
\adviplay[slidegreen]{c10b}
\adviplay[slidegreen]{c11b}
\adviplay[slidegreen]{c11d}
\adviplay[slidegreen]{c12a}
\adviplay[slidegreen]{c13a}
\adviplay[slidegreen]{c13c}
\adviplay[slidegreen]{c34}
\adviplay[slidegreen]{c35a}
\adviplay[slidegreen]{c36}
\adviplay[slidegreen]{c40a}
\adviplay[slidegreen]{c41a}
\adviplay[slidegreen]{c41c}
\adviplay[slidegreen]{c46b}
\adviplay[slidegreen]{c46d}
\adviplay[slidegreen]{c51b}
\adviplay[slidegreen]{c51d}
\adviplay[slidegreen]{c53b}
\adviplay[slidegreen]{c53d}
\adviplay[slidegreen]{c54a}
\adviplay[slidegreen]{c54c}
\adviwait
\adviplay[slidered]{c4}
\adviplay[slidered]{c14}
\adviplay[slidered]{c21}
\adviplay[slidered]{c26}
\adviplay[slidered]{c42}
\adviplay[slidered]{c46a}
\adviplay[slidered]{c47}
\adviplay[slidered]{c51a}
\adviplay[slidered]{c52}
\adviwait
\adviplay[slidered]{c6a}
\adviplay[slidered]{c7a}
\adviplay[slidered]{c8}
\adviplay[slidered]{c11a}
\adviplay[slidered]{c22}
\adviplay[slidered]{c28}
\adviplay[slidered]{c32}
\adviplay[slidered]{c53a}
\adviwait
\adviplay[slidered]{c10a}
\adviplay[slidered]{c11c}
\adviplay[slidered]{c12b}
\adviplay[slidered]{c13b}
\adviplay[slidered]{c16}
\adviplay[slidered]{c19}
\adviplay[slidered]{c24}
\adviplay[slidered]{c30}
\adviplay[slidered]{c35b}
\adviplay[slidered]{c38}
\adviplay[slidered]{c40b}
\adviplay[slidered]{c41b}
\adviplay[slidered]{c44}
\adviplay[slidered]{c46c}
\adviplay[slidered]{c49}
\adviplay[slidered]{c51c}
\adviplay[slidered]{c53c}
\adviplay[slidered]{c54b}
\adviplay[slidered]{c56}
%\adviwait
%\adviplay{c6b}
%\adviplay{c7b}
%\adviplay{c10b}
%\adviplay{c11b}
%\adviplay{c11d}
%\adviplay{c12a}
%\adviplay{c13a}
%\adviplay{c13c}
%\adviplay{c34}
%\adviplay{c35a}
%\adviplay{c36}
%\adviplay{c40a}
%\adviplay{c41a}
%\adviplay{c41c}
%\adviplay{c46b}
%\adviplay{c46d}
%\adviplay{c51b}
%\adviplay{c51d}
%\adviplay{c53b}
%\adviplay{c53d}
%\adviplay{c54a}
%\adviplay{c54c}
%\adviplay{c4}
%\adviplay{c14}
%\adviplay{c21}
%\adviplay{c26}
%\adviplay{c42}
%\adviplay{c46a}
%\adviplay{c47}
%\adviplay{c51a}
%\adviplay{c52}
%\adviplay{c6a}
%\adviplay{c7a}
%\adviplay{c8}
%\adviplay{c11a}
%\adviplay{c22}
%\adviplay{c28}
%\adviplay{c32}
%\adviplay{c53a}
%\adviplay{c10a}
%\adviplay{c11c}
%\adviplay{c12b}
%\adviplay{c13b}
%\adviplay{c16}
%\adviplay{c19}
%\adviplay{c24}
%\adviplay{c30}
%\adviplay{c35b}
%\adviplay{c38}
%\adviplay{c40b}
%\adviplay{c41b}
%\adviplay{c44}
%\adviplay{c46c}
%\adviplay{c49}
%\adviplay{c51c}
%\adviplay{c53c}
%\adviplay{c54b}
%\adviplay{c56}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{luxury mathmode}
\slidetitle{Coq-style proof}
\def\grayhrule{\vspace{-.75em}\advirecord{b}{\gray{\rule{.94\linewidth}{0.04em}}\llap{\vbox to 0pt{
\footnotesize
\let\gray=\black
\vspace{.8\smallskipamount}
%\hbox{\strut\gray{1 subgoal                          }}\vspace{-\smallskipamount}
%\vspace{1.2\medskipamount}
\hbox{\strut\gray{\ \ n : nat                          }}\vspace{-\smallskipamount}
\vspace{.3\smallskipamount}
\hbox{\strut\gray{\ \ IHn : even n -> odd n -> False   }}\vspace{-\smallskipamount}
\vspace{.3\smallskipamount}
\hbox{\strut\gray{\ \ ============================     }}\vspace{-\smallskipamount}
\vspace{.3\smallskipamount}
\hbox{\strut\gray{\ \ \ even (S n) -> odd (S n) -> False}}
\vss}}}\vspace{-.3em}}%
\def\extra{\vspace{-1.1em}}%
\begin{alltt}
\green{Lemma Example : \red{forall n, even n -> odd n -> False}.}
\green{Proof.}
\blue{induction n.}
\blue{intros.}
\blue{inversion H0.}
\grayhrule
\blue{intros.}
\blue{inversion_clear H.}
\blue{inversion_clear H0.}
\blue{auto.}
\green{Qed.}
\end{alltt}                             
\adviwait
\adviplay{b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar-style proof}
\begingroup
\let\blue=\black
\let\rred=\red
\let\red=\black
\begin{alltt}
\green{theorem Example:} \rred{forall n, even n -> odd n -> False}
\green{proof}
 \gray{A1:} \red{even 0 -> odd 0 -> False}
 \green{proof} \blue{assume} that \red{even 0} and \gray{H0:} \red{odd 0};
  \blue{thus} \red{False} \gray{by odd_ind,H0};
 \green{end;}
 \green{now} \blue{let} n be nat;
  \blue{assume} \gray{IHn:} \red{even n -> odd n -> False};
  \blue{assume} that \gray{H:} \red{even (S n)} and \gray{H0:} \red{odd (S n)};
  \gray{H1:} \red{odd n} \gray{by even_ind,H};  \gray{H2:} \red{even n} \gray{by odd_ind,H0};
  \blue{thus} \red{False} \gray{by IHn,H1,H2};
 \green{end;}
 \blue{hence} thesis \gray{by nat_ind,A1};
\green{end;}
\end{alltt}
\endgroup
\vspace{-13pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{`\texttt{sort | uniq}'}

\strut\quad\parbox{12em}{\tiny
\begin{flushleft}
\bigskip
%\texttt{============================}\\
\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{ forall n :\ nat, even n -> odd n -> False}
\adviwait
\vspace{1.7\medskipamount}

\smallskip
%\texttt{============================}\\
\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{ even 0 -> odd 0 -> False}
\adviwait
\vspace{1.5\medskipamount}

\texttt{H :\ even 0}\\
\texttt{H0 :\ odd 0}\\
%\texttt{============================}\\
\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{ False}
\adviwait
\vspace{1.5\medskipamount}

\texttt{n :\ nat}\\
\advirecord{a1}{\texttt{IHn :\ even n -> odd n -> False}}\adviplay{a1}\\
%\texttt{============================}\\
\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{ even (S n) -> odd (S n) -> False}
\adviwait
\vspace{1.5\medskipamount}

\texttt{n :\ nat}\\
\advirecord{a2}{\texttt{IHn :\ even n -> odd n -> False}}\adviplay{a2}\\
\texttt{H :\ even (S n)}\\
\texttt{H0 :\ odd (S n)}\\
%\texttt{============================}\\
\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{ False}
%\adviwait
\vspace{\medskipamount}

\strut\quad{\scriptsize$\blue{\vdots}$}
\end{flushleft}
}\hfill\adviwait$\blue{\longrightarrow}$\hfill
\parbox{12em}{\tiny
\begin{flushleft}
\texttt{ False}\\
\texttt{ even (S n) -> odd (S n) -> False}\\
\texttt{ even 0 -> odd 0 -> False}\\
\texttt{ forall n :\ nat, even n -> odd n -> False}\\
%\texttt{============================}\\
%\vspace{-\smallskipamount}\darkgray{\rule{2.6cm}{0.06em}}\vspace{-.2\smallskipamount}\\
\texttt{H :\ even (S n)}\\
\texttt{H :\ even 0}\\
\texttt{H :\ even n}\\
\texttt{H0 :\ odd (S n)}\\
\texttt{H0 :\ odd 0}\\
\texttt{H1 :\ odd n}\\
\advirecord{a0}{\texttt{IHn :\ even n -> odd n -> False}}\adviplay{a0}\\
\texttt{n :\ nat}
\bigskip
\end{flushleft}
}
\adviwait
\adviplay[slidered]{a0}
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\vbox to 0pt{%
\def\flinter{{\tiny $\,$}}
\vspace{-.8\bigskipamount}
\begin{alltt}
\advirecord{zzz}{\advirecord{x1}{\green{now}}
 \advirecord{x21}{A1:} \advirecord{x22}{\green{now}
  assume \advirecord{x26}{H: even 0}; 
  assume \advirecord{x27}{H0: odd 0};
  thus \advirecord{x28}{False} by \blue{[\advirecord{x25}{     ?4     }\advirecord{x24}{\llap{inversion H0}}\flinter]},H,H0;
 \green{end;}}
 \advirecord{x8}{A2:} \advirecord{x9}{even 0 -> odd 0 -> False} \advirecord{x10}{by \blue{[\advirecord{x11}{intros}\advirecord{x12}{\llap{  ?2  }}]}}\advirecord{x13}{,}\advirecord{x14}{A1}\advirecord{x15}{;}
 \advirecord{x16}{A3:} \advirecord{x17}{\green{now} let \advirecord{x17a}{n be nat};
  assume IHn: \advirecord{x18}{even n -> odd n -> False};\medskip
  thus \advirecord{x19}{even (S n) -> odd (S n) -> False} by \blue{[  \advirecord{x20}{?3}  ]},IHn\phantom{,H1,H};\toolong
 \green{end;}}
 \advirecord{x2}{thus} \advirecord{x2a}{forall n, even n -> odd n -> False}
  \advirecord{x2b}{by} \advirecord{x3}{\blue{[\advirecord{x4}{induction n}\advirecord{x5}{\llap{    ?1     }}]}}\advirecord{x6}{,}\advirecord{x6a}{A2}\advirecord{x6b}{,}\advirecord{x6c}{A3}\advirecord{x7}{;\toolong
\green{end;}}}
\end{alltt}
\adviplay{x1}
\adviplay{x2}
\adviplay[slidered]{x2a}
\adviplay{x2b}
\adviplay{x3}
\adviplay[slidered]{x5}
\adviplay{x7}
\adviwait
\adviplay{x2a}
\adviplay[white]{x5}
\adviplay[slidered]{x4}
\adviwait
\adviplay{x6}
\adviplay[slidered]{x6a}
\adviplay[slidered]{x8}
\adviplay{x9}
\adviplay{x10}
\adviplay[slideblue]{x12}
\adviplay{x15}
\adviwait
\adviplay{x6b}
\adviplay[slidered]{x6c}
\adviplay[slidered]{x16}
\adviplay{x17}
\adviplay{x17a}
\adviplay{x18}
\adviplay{x19}
\adviplay[slideblue]{x20}
\adviwait
\adviplay[slideblue]{x4}
\adviplay{x6a}
\adviplay{x6c}
\adviplay{x8}
\adviplay{x16}
\adviplay[slidered]{x9}
\adviplay[slidered]{x12}
\adviwait
\adviplay{x9}
\adviplay[white]{x12}
\adviplay[slidered]{x11}
\adviwait
\adviplay{x13}
\adviplay[slidered]{x14}
\adviplay[slidered]{x21}
\adviplay{x22}
\adviplay[slideblue]{x25}
\adviplay{x26}
\adviplay{x27}
\adviplay{x28}
\adviwait
\adviplay[slideblue]{x11}
\adviplay{x14}
\adviplay{x21}
\adviplay[slidered]{x25}
\adviplay[slidered]{x26}
\adviplay[slidered]{x27}
\adviplay[slidered]{x28}
\adviwait
\adviplay[white]{x25}
\adviplay[slidered]{x24}
\adviplay{x26}
\adviplay{x27}
\adviplay{x28}
\adviwait
\adviplay[slideblue]{x24}
\adviwait
\adviplay[slidered]{x17a}
\adviplay[slidered]{x18}
\adviplay[slidered]{x19}
\adviplay[slidered]{x20}
\vss
}
\vspace{-13pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{integration}
\begin{itemize}
\item[$\bullet$]
\textbf{proof with goals and tactics}
\begin{eqnarray*}
\mbox{proof} &=& \mbox{list of tactics} \\
\mbox{proof state} &=& \mbox{proof obligation that diminishes until it vanishes}
\end{eqnarray*}

\item[$\bullet$]
\textbf{alternative proposed here}
\begin{eqnarray*}
\mbox{proof} &=& \mbox{\green{both} tactics and statements \green{mixed together}} \\
\mbox{proof state} &=& \mbox{declarative proof that \green{grows until it is complete}}
\end{eqnarray*}
\end{itemize}
\medskip
\adviwait

\red{two ways of working on a proof:}
\begin{itemize}
\item[$\bullet$]
manually editing and rechecking the proof (the Mizar way)
\item[$\bullet$]
applying a tactic at an unjustified step (the Coq way)
\end{itemize}
\vspace{-3pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{implementation}
\slidetitle{tiny subset of Mizar}
\begin{eqnarray*}
\red{\langle\mbox{proof}\rangle} &::=& \langle\mbox{label}\rangle\ \textbf{:}\ \textbf{now} \\
\noalign{\vspace{-\smallskipamount}}
&& \quad \green{\langle\mbox{intro}\rangle}^* \\
\noalign{\vspace{-\smallskipamount}}
&& \quad \red{\langle\mbox{proof}\rangle}^* \\
\noalign{\vspace{-\smallskipamount}}
&& \quad \textbf{thus}\ \langle\mbox{statement}\rangle\ \textbf{by}\ {\langle\mbox{justification}\rangle}\ \textbf{;}\qquad \\
\noalign{\vspace{-\smallskipamount}}
&& \textbf{end ;} \\
\noalign{\medskip}
\green{\langle\mbox{intro}\rangle} &::=& \textbf{let}\ \langle\mbox{variable}\rangle\ \textbf{be}\ \langle\mbox{type}\rangle\ \textbf{;} \\
&\phantom{::=}\llap{$|\;$}& \textbf{assume}\ \langle\mbox{label}\rangle\ \textbf{:}\ \langle\mbox{statement}\rangle\ \textbf{;} \\
\noalign{\medskip}
{\langle\mbox{justification}\rangle} &::=& \advirecord{e1}{\rlap{$\{\ \textbf{,}\ \langle\mbox{label}\rangle\ \}$}}\advirecord{e2}{\blue{\langle\mbox{tactic}\rangle}\ \{\ \textbf{,}\ \langle\mbox{label}\rangle\ \}}
\end{eqnarray*}
\adviplay{e1}
%\adviwait
\adviplay[white]{e1}
\adviplay{e2}
\vfill
\end{slide}

\begin{slide}
\slidetitle{simplification of proofs}
{example of one of the proof rewriting rules}
\begin{center}
\medskip
\begin{tabular}{lcl}
\textbf{now} \\
\noalign{\vspace{-1.5\smallskipamount}}
\quad \dots && \textbf{now} \\
\noalign{\vspace{-1.2\smallskipamount}}
\quad \textbf{now} && \quad \dots \\
\noalign{\vspace{-\smallskipamount}}
\qquad \textbf{let} \green{var}$\,$; && \quad \textbf{consider} \green{var} \textbf{such} \textbf{that} \\
\noalign{\vspace{-\smallskipamount}}
\qquad \textbf{assume} \gray{label$\,$:} \green{statement$_1$}; && \gray{label$\,$:} \green{statement$_1$} \textbf{by} \dots; \\
\noalign{\vspace{-\smallskipamount}}
\qquad \dots &\green{$\longrightarrow\;$}& \quad \dots \\
\noalign{\vspace{-\smallskipamount}}
\qquad \textbf{thus} \red{statement$_2$} \textbf{by} \dots; && \quad \textbf{thus} \red{statement$_2$} \textbf{by} \dots; \\
\noalign{\vspace{-\smallskipamount}}
\quad \textbf{end}; && \textbf{end}; \\
\noalign{\vspace{-\smallskipamount}}
\quad \textbf{thus} \red{statement$_2$} \textbf{by} \dots; \\
\noalign{\vspace{-\smallskipamount}}
\textbf{end};
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
%\sectiontitle{prototype}
\slidetitle{prototype in HOL Light}
\vspace{2em}
\begin{center}
\setlength{\fboxrule}{.5pt}
\red{\fbox{\quad\strut\textbf{\red{demo}}\quad}}
\end{center}
\vspace{9em}

\begin{alltt}
\green{let EXAMPLE = prove
 (}{`!n. ~(EVEN n) <=> ODD n`},
  \blue{INDUCT_TAC} \green{THEN} \blue{ASM_REWRITE_TAC[EVEN; ODD]}\green{);;}
\end{alltt}
\vspace{-5em}
\adviwait
\adviembed{/home/freek/talks/luxury1/xtermhol}%
\vfill
\end{slide}

\begin{slide}
\sectiontitle{conclusion}
\slidetitle{desires \& doubts}

\blue{desires}
\begin{itemize}
\item[$\bullet$]
{working on \red{formal proof sketch} and \red{formalization} together}
\adviwait

\item[$\bullet$]
{having the freedom to \red{mix the ways of working in Mizar and Coq}}

\end{itemize}
\adviwait
\medskip\smallskip

\blue{doubts}
\begin{itemize}
\item[$\bullet$]
\green{approach still reasonable when you get large/non-intuitive subgoals?}

\end{itemize}

\vfill
\end{slide}

\end{document}