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

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

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large \advirecord{title}{formal proof sketches}\adviplay{title} \& Lamport-style proofs}

Freek Wiedijk \\
University of Nijmegen

TYPES 2003 \\
Torino

2003 05 03, 11:00
%\adviwait
%\adviplay[slidered]{title}
\end{slide}

\begin{slide}
\sectiontitle{formal proof sketches}
\slidetitle{\textbf{problem 1:} what to do with formal proofs?}
end product of a formalization project: tar file of scripts
\adviwait

what people look at: the statements of the lemmas \\
%\adviwait
\red{proof scripts are `write only'}
\adviwait
\bigskip

many projects: \green{presenting formal proofs in natural language}
\adviwait
\medskip

MoWGLI project (Bologna, INRIA, Saarbr\"ucken, Berlin, Nijmegen)
\begin{center}
\textbf{Coq script} $\stackrel{\sf Coq\,}{\relbar\joinrel\longrightarrow}$ Coq XML $\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ OMDoc XML \advirecord{HTML}{$\stackrel{\sf XSLT}{\relbar\joinrel\relbar\joinrel\longrightarrow}$ \textbf{English} HTML}\adviplay{HTML}
\end{center}
\adviwait
%\adviplay[slidegray]{HTML}
%\adviwait
\medskip

generated text should become better \\
currently: rather verbose
%\adviwait
%(folding of subproofs doesn't help much)
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{problem 2:} only formalization of the interesting parts?}
Peter Aczel (at TYPES 2002 meeting): \\
getting mathematicians interested in formalization
%\adviwait

\red{light weight formalization} \\
don't prove everything: support reasoning with gaps
\adviwait
\bigskip

Leslie Lamport: \green{\textbf{How to Write a Proof}} (1993) \\
recursive clarification process: \red{hierarchical proofs} \\
\adviwait
not formal
\adviwait
\medskip

IMP project (Paul Cairns \& Jeremy Gow, London): implementation \\
interactive course notes: \green{Elements of Euclidean and Metric Topology}$\hspace{-2em}$ %\\
%\adviwait
%used in actual topology courses

experience: structure not easily understood
\vfill
\end{slide}

\begin{slide}
\slidetitle{an informal proof}
%\green{prover comparison}: proofs of \red{irrationality of $\sqrt{2}$} \\
%%\adviwait
%\textbf{HOL Light}: 29 lines, \textbf{Mizar}: 44 lines, \textbf{Coq}: 68 lines, \textbf{PVS}: 77 lines, \textbf{Isabelle}: 114 lines
%%\adviwait
%%($+$ ten more systems)
%\adviwait
%\medskip
%
Hardy \& Wright, \green{An Introduction to the Theory of Numbers}%: \textbf{7 lines}
%\adviwait
\medskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}
\begin{center}
\setlength{\fboxsep}{.5em}
$\hspace{-2em}$\framebox{\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}}$\hspace{-2em}$
\end{center}
\end{quote}
\vss
}
\vfill
\end{slide}

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

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{quote}\small
\advirecord{a1}{\textbf{theorem} Th43: sqrt 2 is irrational} \\
%$\,$:: \textbf{Pythagoras' theorem}}$\hspace{-1em}$ \\
\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

\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{;}}\\
\green{:: \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[slideblue]{c6b}
\adviplay[slideblue]{c7b}
\adviplay[slideblue]{c10b}
\adviplay[slideblue]{c11b}
\adviplay[slideblue]{c11d}
\adviplay[slideblue]{c12a}
\adviplay[slideblue]{c13a}
\adviplay[slideblue]{c13c}
\adviplay[slideblue]{c34}
\adviplay[slideblue]{c35a}
\adviplay[slideblue]{c36}
\adviplay[slideblue]{c40a}
\adviplay[slideblue]{c41a}
\adviplay[slideblue]{c41c}
\adviplay[slideblue]{c46b}
\adviplay[slideblue]{c46d}
\adviplay[slideblue]{c51b}
\adviplay[slideblue]{c51d}
\adviplay[slideblue]{c53b}
\adviplay[slideblue]{c53d}
\adviplay[slideblue]{c54a}
\adviplay[slideblue]{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}
\slidetitle{incomplete but completable proofs}
formal proof sketch: \textbf{only} `inference errors' \\
\adviwait
completable into a checkable proof by adding:
\begin{itemize}
\item[$\bullet$]
\textbf{steps} %\\
%\advirecord{e1}{not only subproofs, but also steps in-between!} %\\
%\advirecord{e2}{problems for automated theorem provers} \advirecord{e3}{(Josef Urban's MPTP)}
\item[$\bullet$]
\textbf{labels/references} %\\
%\advirecord{e4}{informal proofs also have some references, but!}
\end{itemize}
\adviwait
%\adviplay{e1}
%\adviwait
%\adviplay{e2}
%\adviwait
%\adviplay{e3}
%\adviwait
%\adviplay{e4}
%\adviwait
\medskip

\red{formal} proof sketches \\
\adviwait
correctness: semi-decidable
\adviwait
\bigskip

\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{center}
\begin{picture}(300,50)
\put(40,24){\makebox(0,0){no proofs}}
\put(40,10){\line(0,1){8}}
\advirecord{f1a}{\put(260,10){\line(0,1){8}}}%
\advirecord{f2a}{\put(40,14){\line(1,0){220}}}%
\advirecord{f3a}{\put(260,24){\makebox(0,0){full proofs}}}%
\put(150,0){\makebox(0,0){\blue{formal proof sketch spectrum}}}
\advirecord{f1b}{\put(160,10){\line(0,1){8}}}%
\advirecord{f2b}{\put(40,14){\line(1,0){120}}}%
\advirecord{f3b}{\put(160,24){\makebox(0,0){full proofs}}}%
\advirecord{fx1}{\green{\put(120,31){\vector(0,-1){17}}}}
\advirecord{fx2}{\put(120,49){\makebox(0,0){\green{`human level'}}}}
\advirecord{fx3}{\put(120,38){\makebox(0,0){\green{formal proof sketches}}}}
\end{picture}
\end{center}
\adviplay{f1a}\adviplay{f2a}\adviplay{f3a}
\adviwait
\adviplay{fx1}\adviplay{fx2}\adviplay{fx3}
\adviwait
\adviplay[white]{f1a}\adviplay[white]{f2a}\adviplay[white]{f3a}
\adviplay{f1b}\adviplay{f2b}\adviplay{f3b}
\vss}
\vfill
\end{slide}

\begin{slide}
\slidetitle{declarative proof style}
formal proof sketches (in this talk): \green{Mizar system}
\adviwait
\medskip

some reinventions of Mizar proof style:
\begin{itemize}
\item[$\bullet$]
Markus Wenzel's Isar language for the Isabelle system
\item[$\bullet$]
Henk Barendregt's `math mode' plans for the Coq system
\end{itemize}
\adviwait
\medskip

\red{forward reasoning} \\
\notion{label}\textbf{:} \notion{statement} \textbf{by} \notion{references}\textbf{;}
%\adviwait
%\medskip

\red{natural deduction}
\begin{tabular}{lcl}
$\to$-introduction &$\,\to\,$& \textbf{assume} \notion{proposition}\textbf{;} \vspace{-\smallskipamount}\\
$\exists$-elimination &$\,\to\,$& \textbf{consider} \notion{variable} \textbf{such that} \notion{proposition}\textbf{;} \vspace{-\smallskipamount}\\
etc.
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch grammar}
\vbox to 0pt{
\vspace{-\bigskipamount}
\vspace{-\smallskipamount}
\begin{tabular}{rcl}
statement &=& proposition \advirecord{d1}{justification} \\
% &$|$& \advirecord{d2}{$[\,$label \textbf{:}$\,]$} term \textbf{=} term \advirecord{d3}{justification} \vspace{-\smallskipamount}\\
% && \quad $\{$\textbf{.=} term \advirecord{d4}{justification}$\}$ \vspace{-\smallskipamount}\\
proposition &=& \advirecord{d5}{$[\,$label \textbf{:}$\,]$} formula \\
% formula &=& {\dots} $\;\;|\;\;$ \textbf{thesis} \vspace{-\smallskipamount}\\
justification &=& \advirecord{d6a}{$[\,$\textbf{by} label $\{$\textbf{,} label$\}\,]$} \vspace{-\smallskipamount}\\
 &\advirecord{d6b}{$|$}& \textbf{proof} $\{$step \textbf{;}$\}$ $[\,$cases$\,]$ \textbf{end} \\
step &=& \advirecord{d7}{$[\,$\textbf{then}$\,]$} statement
% $\;\;|\;\;$ \textbf{set} variable \textbf{=} term
 \vspace{-\smallskipamount}\\
 &$|$& \textbf{assume} proposition
 \vspace{-\smallskipamount}\\
 &$|$& \textbf{let} variable $\{$\textbf{,} variable$\}$ \vspace{-\smallskipamount}\\
 &$|$& \advirecord{d8a}{$($}\textbf{thus} \advirecord{d8b}{$|$ \textbf{hence}$)$} statement \vspace{-\smallskipamount}\\
 &$|$& \advirecord{d9}{$[\,$\textbf{then}$\,]$} \textbf{consider} variable $\{$\textbf{,} variable$\}$ \vspace{-\smallskipamount}\\
 && \quad \textbf{such} \textbf{that} proposition \advirecord{d10}{justification} \vspace{-\smallskipamount}\\
 &$|$& \textbf{take} term $\{$\textbf{,} term$\}$ \\
cases &=& \textbf{per} \textbf{cases} \advirecord{d11}{justification} \textbf{;} \vspace{-\smallskipamount} \\
 && \quad $\big\{$\textbf{suppose} proposition \textbf{;} $\{$step \textbf{;}$\}\big\}\hspace{-3em}$
\end{tabular}
\adviplay{d1}
\adviplay{d2}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviplay{d6a}
\adviplay{d6b}
\adviplay{d7}
\adviplay{d8a}
\adviplay{d8b}
\adviplay{d9}
\adviplay{d10}
\adviplay{d11}
\adviwait
\adviplay[slidegray]{d1}
\adviplay[slidegray]{d2}
\adviplay[slidegray]{d3}
\adviplay[slidegray]{d4}
\adviplay[slidegray]{d5}
\adviplay[slidegray]{d6a}
\adviplay[slidegray]{d6b}
\adviplay[slidegray]{d7}
\adviplay[slidegray]{d8a}
\adviplay[slidegray]{d8b}
\adviplay[slidegray]{d9}
\adviplay[slidegray]{d10}
\adviplay[slidegray]{d11}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{generating formal proof sketches?}
\green{full Mizar formalization $\relbar\joinrel\longrightarrow$ formal proof sketch}
\adviwait
\medskip

systematic procedure (works surprisingly well)
\adviwait
\begin{itemize}
\item[$\bullet$]
remove all labels/references
\adviwait
\item[$\bullet$]
remove `in-between' steps % (and maybe some sub-proofs)
\end{itemize}
\adviwait
\medskip

but how to locate the \red{important steps} in a proof?
\adviwait
\begin{itemize}
\item[$\bullet$]
\textbf{user tagging} \\
%\adviwait
no support for this in the Mizar language \adviwait (yet)
\adviwait
\item[$\bullet$]
\textbf{heuristics} \\
%\adviwait
but: no good heuristics known to me \\
so formal proof sketches can't be generated automatically \adviwait (yet)
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof development cycle}
% \xymatrix{
% \mbox{informal text}\adviwait\ar@{->}[r] & \mbox{formal proof sketch}\adviwait\ar@(dr,ul)@{->}[rrd] &&\\
% & \mbox{\advirecord{g}{formal proof sketch}} && \mbox{full formalization}\adviwait\ar@{-}[ll]\adviplay{g}
% }
\vspace{-\bigskipamount}
$$\xymatrix@=1.5em{
\mbox{informal text}\adviwait\ar@{->}[d] \\
\mbox{formal proof sketch}\adviwait\ar@(dr,ul)@{->}[rd] & \mbox{\advirecord{g}{formal proof sketch}} \\
& \mbox{full formalization}\adviwait\ar@{.}[u]\adviplay{g}
}$$
\adviwait

\blue{\textbf{comparing sizes:}}
\begin{center}
%formal proof sketch $\;\ll\;$ full formalization \advirecord{h}{${\mathop{\;\ll\;}\limits_{\sf\green{in\;practice}}}$ generated language}$\hspace{-1em}$
formal proof sketch $\;\ll\;$ full formalization $\;\ll\;$ generated language
\end{center}
%\adviwait
%\adviplay{h}
\adviwait
\medskip

human attention span is important \\
%\adviwait
\red{presentation should be much smaller than the formalization} %\\
%\adviwait
%(`more explanation' is not the same as `easier to understand'!)
%\adviwait

%proof presentation: should be \green{road map to the full formal proof} \\

\adviwait
\medskip
(\blue{folding sub-proofs}: doesn't help!)

\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketches from IMP web pages}
\begingroup
$$
\smallskip
\hspace{-1em}
\def\xxx#1#2{{\mathop{\mbox{{\small\strut}#1}}\limits_{\textcolor{slidegreen}{\textsf{\small{\tiny\strut} #2 lines}}}}}
\xymatrix@=1.5em{
\xxx{\red{\textbf{informal proof}}}{14} \adviwait \ar[d] \\
\xxx{\textbf{formal proof sketch}}{18} \ar[d] \\
\xxx{full formalization}{113} \adviwait }
\qquad
\xymatrix@=1.5em{
\xxx{\red{\textbf{Lamport-style proof}}}{3{\tiny $\,$}\ldots 70} \adviwait \ar[dd] \\
& \advirecord{t1}{\xxx{formal proof sketch}{32}} \\
\xxx{in Mizar syntax}{111} \ar[d] &
\advirecord{t2}{\xxx{`optimized' formalization}{106}}
\\ % \ar[u] \\
\xxx{full formalization}{284} \adviwait \ar@(u,d)[ur]
\save[ur]\ar[uur]\restore
\adviplay{t1}
\adviplay{t2}
}
\hspace{-3em}
$$
\endgroup
\vfill
\end{slide}

\begin{slide}
\slidetitle{informal proof}
\textbf{Theorem} \\
Open intervals are connected

\textbf{Proof} \\
\rightskip=0pt
The proof proceeds by contradiction. Suppose that $(a,b)$ were not
connected. Then there would be a pair of non-empty disjoint proper
open subsets, $U$, $V$ say, of $(a,b)$ whose union would be
$(a,b)$. This implies a `gap' so we use the completeness of the real
line to show that there can't be a gap. \red{To do this, find a supremum of
some interval which must be contained in $U$.} Note that there is a small
open ball about the supremum which because $U$ and $V$ are open must be
contained wholly within one or other of them. However, in both cases,
this leads to a contradiction: if the ball is in $U$ then the ball
contains points in $U$ exceeding the supremum; if the ball is in $V$
\green{then there are points in the ball also in $U$} by definition of the supremum.
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch} % from informal proof}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\begin{flushleft}\footnotesize
\textbf{theorem} (.a,b.) is connected \\
\textbf{proof} \\
\quad \textbf{assume} (.a,b.) is not connected\textbf{;} \\
\quad \textbf{consider} U\textbf{,}V \textbf{being} non empty open Subset of {\scriptsize REAL}\textbf{,} u\textbf{,}v \textbf{such that}  \\
\qquad U {\scriptsize\raise1pt\hbox{/$\backslash$}} V = $\{\}$ \& U {\scriptsize\raise1pt\hbox{$\backslash$/}} V = (.a,b.) \& u in U \& v in V \& u $<$ v\textbf{;} \\
\quad \red{\textbf{reconsider} X = $\{$ x : (.u,x.) c= U $\}$ \textbf{as} Subset of {\scriptsize REAL}\textbf{;}} \\
\quad \red{\textbf{set} s = sup X\textbf{;}} \\
\quad \textbf{per cases;} \\
\quad \textbf{suppose} s in U\textbf{;} \\
\qquad \textbf{consider} e \textbf{such that} e $>$ 0 \& Ball(s,e) c= U\textbf{;} \\
\qquad ex x st x in Ball(s,e) \& x $>$ s\textbf{;} \\
\qquad \textbf{thus} contradiction\textbf{;} \\
\quad \textbf{suppose} s in V\textbf{;} \\
\qquad \textbf{consider} e \textbf{such that} e $>$ 0 \& Ball(s,e) c= V\textbf{;} \\
\qquad \green{ex x st x in Ball(s,e) \& x in U\textbf{;}} \\
\qquad \textbf{thus} contradiction\textbf{;} \\
\textbf{end;}
\end{flushleft}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Lamport-style proof}
\bigskip
\bigskip

\begin{center}
\textbf{IMP web page in Mozilla}
\end{center}
\vfill
\adviwait
\adviembed{/home/freek/talks/types2003/demo/run}

\end{slide}

\begin{slide}
\slidetitle{the morals}
\begin{itemize}
\item[$\bullet$]
\red{sub-proofs are a bad idea} \\
%\adviwait
it destroys the natural `linear structure' of the proof
\adviwait

\item[$\bullet$]
\red{references are a bad idea} \\
%\adviwait
(at least they are not needed in an informal proof)
\adviwait
\smallskip

and duplicate labels are definitely a bad idea
\adviwait
\medskip

\item[$\bullet$]
\green{formal proof sketches are a good idea} \\
%\adviwait
able to match the structure of all these proofs
%\adviwait
%\smallskip
%
%(really: Mizar is a good idea)
\end{itemize}
\bigskip
\adviwait

\textbf{adapting IMP technology for generating formal proof sketches?}

\vfill
\end{slide}

\end{document}