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

Freek Wiedijk \\
Radboud University Nijmegen

2004 11 01, 15:00
\end{slide}

\begin{slide}
\sectiontitle{two desires}
\slidetitle{\textbf{desire 1:} a remark by Christine Paulin}
%the two main proof styles found in \textbf{interactive} proof asistants
\begin{itemize}
\item[$\bullet$]
\strut\rlap{\advirecord{c1}{\hspace{12em}$\longleftarrow$ better for computer science}\advirecord{c3}{?}}\textbf{procedural proofs}

\green{Coq, NuPRL, PVS, HOL, Isabelle/tactics}

{
`lists of tactics' \\
90\% of the steps are backward steps \\
proof scripts unreadable
}
\item[$\bullet$]
\strut\rlap{\advirecord{c2}{\hspace{12em}$\longleftarrow$ better for mathematics}}\textbf{declarative proofs}

\green{Mizar, Hyperproof, Tutch, Declare, Isabelle/Isar}

{
`lists of statements' \\
90\% of the steps are forward steps \\
proof scripts are like mathematical text
}
\end{itemize}
\medskip
\adviwait
\adviplay[slidered]{c2}
\adviwait
\adviplay[slidered]{c1}
%\adviwait
\adviplay[slidered]{c3}
\vspace{-14pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{desire 2:} what mathematicians want}
Royal Society discussion meeting in London
\begin{center}
\red{`the nature of mathematical proof'}
\end{center}
private talk with {Paul J. Cohen}
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\textbf{formalizations should look like mathematical texts}

\green{`{}``type'' is computer jargon'}

\item[$\bullet$]
\textbf{formalizations should be developed top-down}

\green{work from axioms}

\item[$\bullet$]
\textbf{proof assistants should hold a dialog}

\green{in case of unclarities, the system should just ask the user}

\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{desire 3:} saving legacy formal proofs for posterity}
{John Harrison}: \\
\red{declarative proofs might better survive their system}
\adviwait
\bigskip

\begin{center}
\green{statements resemble each other between systems} \\
\green{$\Downarrow$} \\
\green{declarative proofs resemble each other between systems}
\bigskip

\begin{itemize}
\item[$\bullet$]
they will not check (differences in `justification' power) but
\item[$\bullet$]
they will be useful as a basis for `porting' a proof
\end{itemize}
\bigskip
\adviwait
\end{center}

\blue{but how about existing libraries of procedural proofs?} \\
\red{conversion of procedural proofs to declarative proofs}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{five ingredients}
\slidetitle{\textbf{ingredient 1:} Coq-style procedural 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{\textbf{ingredient 2:} Mizar-style declarative proof}
%\vspace{-1.65\bigskipamount}
\begin{alltt}
\green{theorem Example:} \red{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}
\vspace{-13pt}
\vfill
\end{slide}

\if 0
\begin{slide}
\slidetitle{\textbf{ingredient 3:} NuPRL-style proof presentation}
\vbox to 0pt{%
\vspace{-.8\bigskipamount}
\begingroup
\footnotesize
\def\\{{\char`\\}}%
\def\|{{\char`\|}}%
\def\greenvdash{$\green{\vdash}$}%
\begin{alltt}
\greenvdash \red{forall n : nat, even n -> odd n -> False}
\|
\blue{induction n.}
\|\\
\| \greenvdash \red{even 0 -> odd 0 -> False}
\| \|
\| \blue{intros.}
\| \|
\| \gray{H :} \red{even 0}
\| \gray{H0 :} \red{odd 0}
\| \greenvdash \red{False}
\| \|
\| \blue{inversion H0.}
 \\
  \gray{n :} \red{nat}
  \gray{IHn :} \red{even n -> odd n -> False}
  \greenvdash \red{even (S n) -> odd (S n) -> False}
  \|
\end{alltt}
\endgroup
\vss
}
\vfill
\end{slide}

%\begin{slide}
%\slidetitle{NuPRL-style proof presentation (continued)}
%
%\begingroup
%\footnotesize
%\def\\{{\char`\\}}%
%\def\|{{\char`\|}}%
%\def\greenvdash{$\green{\vdash}$}%
%\begin{alltt}
%  \|
%  \blue{intros.}
%  \|
%  \gray{H :} \red{even (S n)}
%  \gray{H0 :} \red{odd (S n)}
%  \greenvdash \red{False}
%  \|
%  \blue{inversion_clear H.}
%  \|
%  \gray{H1 :} \red{odd n}
%  \|
%  \blue{inversion_clear H0.}
%  \|
%  \gray{H :} \blue{even n}
%  \|
%  \blue{auto.}
%\end{alltt}
%\endgroup
%\vfill
%\end{slide}
\fi

\begin{slide}
\slidetitle{\textbf{ingredient 3:} ALF-style interface}
\vbox to 0pt{%
\vspace{-.8\bigskipamount}
\begingroup
\scriptsize
\setlength{\fboxrule}{.5pt}
\def\Foo{\xred{{?1}$\,$}}
\let\key=\relax
\let\xred=\red
\let\red=\relax
\def\graylater#1{\advirecord{a}{{#1}}}
\begin{alltt}
\green{Example} = 
\key{fun} n : \red{nat} \key{=>}
\red{nat_ind} (\key{fun} n0 : \red{nat} \key{=>} \red{even n0 -> odd n0 -> False})
  (\key{fun} (_ : \red{even 0}) (H0 : \red{odd 0}) \key{=>}
   \graylater{\key{let} H1 :=
     \key{match} \red{H0} \key{in} (\red{odd n}) \key{return} (\red{n = 0 -> False}) \key{with}
     \key{|} odd_S n H1 \key{=>}
         \key{fun} H2 : \red{S n = 0} \key{=>}
         \key{let} H :=
           \key{let} H1 :=
             \red{eq_ind} (\red{S n})
               (\key{fun} e : \red{nat} \key{=>}
                \key{match} \red{e} \key{return} \red{Prop} \key{with}
                \key{|} O \key{=>} \red{False}
                \key{|} S _ \key{=>} \red{True}
                \key{end}) \red{I 0 H2} \key{in}
           \red{False_ind} (\red{even n -> False}) \red{H1} \key{in}
         \red{H H1}
     \key{end} \key{in}
   \red{H1} (\red{refl_equal 0})})
  (\key{fun} (n0 : \red{nat}) (_ : \red{even n0 -> odd n0 -> False}) \key{=>}
   \Foo) n
\end{alltt}
\adviplay{a}
\adviwait
\adviplay[slidegray]{a}
\endgroup
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{ingredient 4:} INRIA-style proof presentation}
two ways of generating a natural language proof presentation
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{starting from the lambda term}

\green{works badly with terms from automated tactics}
%\adviwait
\medskip

\item[$\bullet$]
\textbf{starting from the `proof tree'}

\begin{tabular}{rl}
nodes: & tactics \\
edges: & subgoals
\end{tabular}
\bigskip

\blue{Fr\'ed\'erique Guilhot,
Hanane Naciri,
Lo\"\i c Pottier}
\medskip
%\adviwait

compare subgoals with their descendants one level below \\
\red{different syntax depending on which parts of subgoals are the same}

\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{ingredient 5:} Mizar-style proof optimization}
\begingroup
\def\statement{\textsf{\textbf{statement}}}
\def\sfdots{\textsf{\dots}}%
\begin{alltt}
\sfdots
A4: \statement by A1,\advirecord{d1}{A2};
\advirecord{d2}{A5: \statement by A3,A4;}
A6: \statement by A4,A5;
\sfdots
\end{alltt}
\endgroup
\adviplay{d1}
\adviplay{d2}
\adviwait
\adviplay[slidered]{d1}
\adviplay[slidegreen]{d2}
\begin{itemize}
\item[$\bullet$]
\texttt{\red{relprem}} will tell you which references are not necessary
\item[$\bullet$]
\texttt{\green{relinfer}} will tell you which statements can be skipped
%\adviwait
\end{itemize}
\begingroup
\def\statement{\textsf{\textbf{statement}}}
\def\sfdots{\textsf{\dots}}
\begin{alltt}
\sfdots
A4: \statement by A1;
A6: \statement by A3,A4;
\sfdots
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\sectiontitle{declarative proofs from tactics}
\slidetitle{`\texttt{sort | uniq}'}

observation: subgoals only change gradually over time
\bigskip

keep every line in the subgoals just \textbf{once} \\
\green{all subgoals can be \textbf{merged} into a single declarative proof}
\bigskip
\bigskip

\red{proposal: use \textbf{incomplete} declarative proofs as proof states}

\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{a framework allowing for both proof styles}
\begin{itemize}
\item[$\bullet$]
\textbf{traditional 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

\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}
\slidetitle{proof trees to proofs: a tiny subset of the Mizar proof language}
\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}
\green{example of one of the proof rewriting rules}
\begin{center}
\begin{tabular}{lcl}
\textbf{now} \\
\noalign{\vspace{-\smallskipamount}}
\quad \dots && \textbf{now} \\
\noalign{\vspace{-\smallskipamount}}
\quad \textbf{now} && \quad \dots \\
\noalign{\vspace{-\smallskipamount}}
\qquad \dots &$\longrightarrow\;$& \quad \dots \\
\qquad \textbf{thus} \red{statement} \textbf{by} \dots && \quad \textbf{thus} \red{statement} \textbf{by} \dots \\
\quad \textbf{end;} && \textbf{end;} \\
\quad \textbf{thus} \red{statement} \textbf{by} \dots \\
\textbf{end;}
\end{tabular}
\end{center}
\vfill
\end{slide}

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

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

\begin{slide}
\sectiontitle{system?}
\slidetitle{M-mode?}
two different approaches to get to a luxurious proof assistant
\medskip
\begin{itemize}
\item[$\bullet$]
\textbf{luxurious interface on top of existing proof assistant}

approach used by Isar on top of Isabelle \\
\red{only practical if you are in charge of the original assistant}
\medskip

\begin{center}
\strut\green{\phantom{mathematical}\llap{Mizar} mode$\qquad\qquad\qquad$ \\
\strut mathematical mode$\qquad\qquad\qquad$ \\
\strut\phantom{mathematical}\llap{Mariusz'} mode$\qquad\qquad\qquad$}%
\medskip
\end{center}

\item[$\bullet$]
\textbf{luxurious proof assistant from scratch}

\red{does the world really need \textbf{yet another} proof assistant?}

\end{itemize}
\vfill
\end{slide}

\end{document}