\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,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\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{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\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 a Mizar mode for Coq?}

Freek Wiedijk \\
University of Nijmegen

Math-in-Coq meeting \\
Laboratoire de Recherche en Informatique \\
CNRS/Universit\'e Paris-Sud \\
Orsay

2003 04 24, 09:30
\end{slide}

\begin{slide}
\slidetitle{wishes}
\adviwait
\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{itemize}
\item[$\bullet$]
\textbf{predicative \texttt{Set}}
\adviwait
\item[$\bullet$]
\textbf{tactics in terms} \\
\verb|[x,y:F; H:~y=0](div x y <% Assumption %>)| \\
simulate type-correctness conditions like in PVS
\adviwait
\item[$\bullet$]
\textbf{overloading based on argument types} \\
\verb|A| \verb|/\| \verb|B| notation both for \verb|Prop| and \verb|Set|
\adviwait
\item[$\bullet$]
\textbf{uniform way to indicate labels to tactics} \\
`\notion{tactic} \verb|labeled| \notion{labels}' \\
\verb|Intros| \verb|A| \verb|B| \verb|C| would be a special case of \verb|Intros labeled A| \verb|B| \verb|C| \\
warning for labels that are still implicit
\adviwait
\item[$\bullet$]
\textbf{block structured syntax for tactic scripts} \\
\textcolor{black}{\notion{tactic}}\verb|. |\textcolor{slidered}{$\underbrace{\mbox{\textcolor{black}{\texttt{Proof.} {\dots} \texttt{Qed.} \texttt{Proof.} {\dots} \texttt{Qed.}}}}_{{\rm first\ }n - 1{\rm\ generated\ subgoals}}$} \hspace{-2em} \textcolor{slidered}{$\underbrace{\mbox{\textcolor{black}{\rlap{\phantom{\texttt{Q}}}\dots}}}_{\rm \hspace{1.4em} last\ subgoal}$}
\end{itemize}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{subject of the talk}
$$
\xymatrix@=8em@M=.6em
{\mbox{Isabelle}\ar[d]\ar@{.}[r] & \mbox{Coq} \\ 
\mbox{Isar}\adviwait\ar@{.}[r] & \mbox{\textcolor{slidered}{\LARGE ?}}\ar@{<-}[u]}
$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{a small language}
\slidetitle{a small grammar}
\vbox to 0pt{
\vspace{-\bigskipamount}
\vspace{-\smallskipamount}
\begin{tabular}{rcl}
proposition &=& $[\,$label \textbf{:}$\,]$ formula
  \vspace{-\smallskipamount} \\
statement &=& proposition justification \\
justification &=& $[\,$\textbf{by} label $\{$\textbf{,} label$\}\,]$
  \vspace{-\smallskipamount} \\
 &$|$& \textbf{proof} $\{$step \textbf{;}$\}$ $[\,$cases$\,]$ \textbf{end} \\
step &=& $[\,$\textbf{then}$\,]$ statement
  \vspace{-\smallskipamount} \\
 &$|$& \textbf{assume} proposition
 $\;|\;$ \textbf{let} variable $\{$\textbf{,} variable$\}$
  \vspace{-\smallskipamount} \\
 &$|$& \textbf{thus} statement $\;|\;$ \textbf{hence} statement
  \vspace{-\smallskipamount} \\
 &$|$& $[\,$\textbf{then}$\,]$ \textbf{consider} variable $\{$\textbf{,} variable$\}$
  \vspace{-\smallskipamount} \\
 && \quad \textbf{such} \textbf{that} proposition justification
  \vspace{-\smallskipamount} \\
 &$|$& \textbf{take} term $\{$\textbf{,} term$\}$ \\
cases &=& \textbf{per} \textbf{cases} justification \textbf{;}
  \vspace{-\smallskipamount} \\
 && \quad $\big\{$\textbf{suppose} proposition \textbf{;} $\{$step \textbf{;}$\}\big\}\hspace{-3em}$
\end{tabular}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example: infinity of primes}
\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{flushleft}
for n ex p st p is prime \& p $>$ n \\
\textbf{proof} \\
\quad \textbf{let} n$\,$\textbf{;} \\
\quad n! $>$ 0 \textbf{by} {\small NEWTON$\,$:$\,$23}$\,$\textbf{;} \textbf{then} n! $>$= 0 + 1 \textbf{by} {\small NAT\_$\,$1$\,$:$\,$38}$\,$\textbf{;} \\
\quad \textbf{then} n! + 1 $>$= 1 + 1 \textbf{by} {\small REAL\_$\,$1$\,$:$\,$55}$\,$\textbf{;} \\
\quad \textbf{then consider} p \textbf{such that} \\
A1$\,$\textbf{:}$\,$ p is prime \& p divides n! + 1 \textbf{by} {\small INT\_$\,$2$\,$:$\,$48}$\,$\textbf{;} \\
A2$\,$\textbf{:}$\,$ p $<>$ 0 \& p $>$ 1 \textbf{by} A1\textbf{,}$\,${\small INT\_$\,$2$\,$:$\,$def 5}$\,$\textbf{;} \\
\quad \textbf{take} p$\,$\textbf{;} \textbf{thus} p is prime \textbf{by} A1$\,$\textbf{;} \\
\quad \textbf{assume} p $<$= n$\,$\textbf{;} \\
\quad \textbf{then} p divides n! \textbf{by} A2\textbf{,}$\,${\small NAT\_$\,$LAT$\,$:$\,$16}$\,$\textbf{;} \\
\quad \textbf{then} p divides 1 \textbf{by} A1\textbf{,}$\,${\small NAT\_$\,$1$\,$:$\,$57}$\,$\textbf{;} \\
\quad \textbf{hence} contradiction \textbf{by} A2\textbf{,}$\,${\small NAT\_$\,$1$\,$:$\,$54}$\,$\textbf{;} \\
\textbf{end}$\,$\textbf{;}
\end{flushleft}
\vss
}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the basic Mizar proof step}
\quadskip \advirecord{b1}{A2}$\,$\textbf{:}$\,$ \advirecord{b2}{p $<>$ 0 \& p $>$ 1} $\,$\advirecord{b4}{\textbf{by}}$\,$ \advirecord{b3}{A1\textbf{,}$\;${\small INT\_$\,$2$\,$:$\,$def 5}}$\,$\textbf{;}
\adviplay{b1}\adviplay{b2}\adviplay{b3}\adviplay{b4}
\\
\adviwait
\quadskip \advirecord{a1}{\notion{label}} $\!$\textbf{:} \advirecord{a2}{\notion{formula}} \advirecord{a4}{\textbf{by}} \advirecord{a3}{\notion{references}}$\,$\textbf{;}
\adviplay{a1}\adviplay{a2}\adviplay{a3}\adviplay{a4}
%\adviwait
\adviplay[slidered]{a2}\adviplay[slidered]{b2}
\adviwait
\adviplay{a2}\adviplay{b2}
%\adviplay[slidered]{a1}\adviplay[slidered]{b1}
%\adviwait
%\adviplay{a1}\adviplay{b1}
%\adviplay[slidered]{a3}\adviplay[slidered]{b3}
%\adviwait
%\adviplay{a3}\adviplay{b3}
\medskip

Coq analogue:

\quadskip \verb|Cut| \advirecord{c1}{\notion{formula}}$\,$\verb|;| \verb|[|$\,$\verb|Intro| \advirecord{c2}{\notion{label}} \verb/|/ \verb|Auto| \verb|with| \advirecord{c3}{\notion{references}}$\,$\verb|].|
\adviplay[slidered]{a1}\adviplay[slidered]{a2}\adviplay[slidered]{a3}
\adviplay[slidered]{c1}\adviplay[slidered]{c2}\adviplay[slidered]{c3}

`cut' in the proof + automation of the easy part
\adviwait
\adviplay{a1}\adviplay{a2}\adviplay{a3}
\adviplay{c1}\adviplay{c2}\adviplay{c3}
\medskip

\textbf{by}:
`small' inference
\adviwait
\medskip

Mizar proofs: long lists of this kind of step

\textcolor{slidegreen}{many cuts\exclspace!} \\
\textcolor{slidegreen}{big contexts\exclspace!}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{then}}
generally a step refers to the previous step \\
`{\dots} \textbf{by} \notion{label of previous step}'
may be written as
`\textbf{then} {\dots}'
\adviwait
\medskip

so

\quadskip A1$\,$\textbf{:}$\,$ \notion{formula} \textbf{by} B0$\,$\textbf{;} \\
\quadskip A2$\,$\textbf{:}$\,$ \notion{other formula} \textbf{by} A1,B1$\,$\textbf{;} \\
\quadskip A3$\,$\textbf{:}$\,$ \notion{third formula} \textbf{by} A2,B2$\,$\textbf{;}

can be written as

\quadskip \notion{formula} \textbf{by} B0$\,$\textbf{;} \\
\quadskip \textbf{then} \notion{other formula} \textbf{by} B1$\,$\textbf{;} \\
\quadskip \textbf{then} A3$\,$\textbf{:}$\,$ \notion{third formula} \textbf{by} B2$\,$\textbf{;}
\vfill
\end{slide}

\begin{slide}
\slidetitle{natural deduction steps}
\begin{tabular}{lll}
& \textcolor{slidered}{Mizar} & \textcolor{slidered}{Coq}
 \vspace{-\smallskipamount}\\
$\to$-intro$\quad$ & \textbf{assume} H$\,$: \notion{formula}; & \verb|Intro| H\verb|.|
 \vspace{-\smallskipamount}\\
$\forall$-intro & \textbf{let} x; & \verb|Intro|$\,$ x\verb|.|
 \vspace{-\smallskipamount}\\
$\land$-intro & \textbf{thus} \notion{formula} \textbf{by} R; & \verb|Split;| \verb|[Auto| \verb|with| R \verb/|/ \verb|Idtac].|$\hspace{-4em}$
 \\
$\exists$-elim & \textbf{consider} x \textbf{such that} & \verb|Elim| \notion{existential}\verb|;|
 \vspace{-\smallskipamount}\\
& \quad H$\,$: \notion{formula}; & \quad \verb|Intro| x\verb|;| \verb|Intro| H\verb|.|
%& \quad H$\,$: \notion{formula}; & \quad \verb|Intros| x H\verb|.|
 \\
$\exists$-intro & \textbf{take} \notion{term}; & \verb|Exists| \notion{term}\verb|.|
 \\
$\lor$-elim & \textbf{per cases by} \notion{refs}; & \verb|Elim| \notion{disjunction}\verb|.|
 \vspace{-\smallskipamount}\\
& \quad \textbf{suppose} H1$\,$: \notion{formula}; & \quad \verb|Intro| H1\verb|.|
 \vspace{-\smallskipamount}\\
& \qquad \notion{sub-proof} & \quad \notion{sub-proof}
 \vspace{-\smallskipamount}\\
& \quad \textbf{suppose} H2$\,$: \notion{formula}; & \quad \verb|Intro| H2\verb|.|
 \vspace{-\smallskipamount}\\
& \qquad \notion{sub-proof} & \quad \notion{sub-proof}
\end{tabular}
\medskip

\textcolor{slidegreen}{all other natural deduction rules: \textbf{by}}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a small grammar (continued)}

\begin{tabular}{rcl}
step &=& {\dots} $\;|\;\;$ \textbf{set} variable \textbf{=} term \\
\advirecord{iter}{
statement &=& {\dots} $\;|\;\;$ $[\,$label \textbf{:}$\,]$ term \textbf{=} term justification \vspace{-\smallskipamount}\\
 && \phantom{{\dots} $\;|\;\;$} \quad $\{$\textbf{.=} term justification$\}$ \\}
\advirecord{thesis}{formula &=& {\dots} $\;|\;\;$ \textbf{thesis}}
\end{tabular}
\medskip

some more features of the Mizar proof language:
\begin{itemize}
\item[$\bullet$]
local definitions
\adviwait
\item[$\bullet$]
\adviplay{iter}
iterative equalities
\begin{quote}
\begin{tabular}{rrll}
$\;(x + y)^2\;$ &$\hspace{-1em}$\textbf{=}$\hspace{-1em}$& $\;(x + y)(x + y)\;$ & $\hspace{-.8em}$\textbf{by}$\,$ {\dots}
  \vspace{-\smallskipamount}\\
 &$\hspace{-1em}$\textbf{.=}$\hspace{-1em}$& $\;x(x + y) + y(x + y)\;$ & $\hspace{-.8em}$\textbf{by}$\,$ {\dots}
   \vspace{-\smallskipamount}\\
 &$\hspace{-1em}$\textbf{.=}$\hspace{-1em}$& $\;x^2 + xy + yx + y^2\;$ & $\hspace{-.8em}$\textbf{by}$\,$ {\dots}
   \vspace{-\smallskipamount}\\
 &$\hspace{-1em}$\textbf{.=}$\hspace{-1em}$& $\;x^2 +2xy + y^2\;$ & $\hspace{-.8em}$\textbf{by}$\,$ {\dots}$\,$\textbf{;}
\end{tabular}
\end{quote}
\end{itemize}
\adviwait
\adviplay{thesis}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar modes}
\slidetitle{what's a Mizar mode?}
full Mizar:
\begin{itemize}
\item[\advirecord{l1}{$\bullet$}]
\advirecord{l2}{proof language}\adviplay{l1}\adviplay{l2}
\item[$\bullet$]
foundations (first order logic, ZFC-style set theory)
\item[$\bullet$]
type system (multiple types, sub-typing, `adjectives', structures)
\item[$\bullet$]
automation (powerful type inference, very fast inference checking)
\item[$\bullet$]
expression syntax (heavy overloading, flexible operator syntax)
\end{itemize}
\adviwait
\medskip

\adviplay[slidegreen]{l2}
\textcolor{slidegreen}{Mizar mode: \textbf{only} the proof language on top of another system}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar modes}
various systems that isolate the Mizar proof language from Mizar:
\begin{center}
\begin{tabular}{rl}
Andrzej Trybulec: & baby Mizar ($=$ Mizar MSE) \\
\adviwait
John Harrison: & Mizar mode for HOL Light \\
\adviwait
Markus Wenzel: & \advirecord{isar}{Isar for Isabelle}\adviplay{isar} \\
\adviwait
Freek Wiedijk: & Mizar Light for HOL Light \\
\adviwait
Henk Barendregt: & `math mode' for Coq
  \vspace{-\smallskipamount} \\
(Bas Spitters: & partial implementation using ${\cal L}_{\rm tac}$ language)
\end{tabular}
\end{center}
\adviwait
\medskip

\adviplay[slidered]{isar}
\textcolor{slidered}{only one serious system}
\vfill
\end{slide}

\begin{slide}
\slidetitle{keywords}
\vbox to 0pt{
\vspace{-\bigskipamount}
\vspace{-\smallskipamount}
\begin{tabular}{lll}
\textcolor{slidered}{Mizar} & \textcolor{slidered}{Isar} & \textcolor{slidered}{`math mode'} \vspace{-\smallskipamount}\\
\notion{label}: & \notion{label}: & \textcolor{slidegray}{doesn't exist} \vspace{-\smallskipamount}\\
by & from, using & by \vspace{-\smallskipamount}\\
then & then, with & Then \vspace{-\smallskipamount}\\
proof/end & proof/qed & Proof/QED \vspace{-\smallskipamount}\\
\textcolor{slidegray}{no keyword} & have & Then \vspace{-\smallskipamount}\\
thus & show & Then \vspace{-\smallskipamount}\\
hence & then show & Then \vspace{-\smallskipamount}\\
assume & assume & Assume/Towards \vspace{-\smallskipamount}\\
let & fix & Let \vspace{-\smallskipamount}\\
consider/such that$\quad$ & obtain/where$\quad$ & There exists/such that, Pick$\hspace{-2em}$ \vspace{-\smallskipamount}\\
take & \textcolor{slidegray}{doesn't exist} & Take \vspace{-\smallskipamount}\\
per cases/suppose & next assume & Case \vspace{-\smallskipamount}\\
set & let, def & \textcolor{slidegray}{doesn't exist} \vspace{-\smallskipamount}\\
% .= & {\dots} = & \textcolor{slidegray}{doesn't exist} \vspace{-\smallskipamount}\\
thesis & ?thesis & \textcolor{slidegray}{doesn't exist}
\end{tabular}
\vss}
\vfill
\end{slide}

\begin{slide}
\slidetitle{synonyms}
keywords $\longleftrightarrow$ meaning
\begin{itemize}
\item[$\bullet$]
mature languages (Mizar, Isar): one-to-one

\item[$\bullet$]
Henk's `math mode': many-to-one
\end{itemize}
\medskip
\adviwait

\textcolor{slidered}{`math mode' synonyms}

\textbf{Then} = \textbf{We have} = \textbf{It follows that} = \textbf{Hence} = \textbf{Moreover} = \textbf{Again}

\textbf{Towards} = \textbf{Suffices} = \textbf{In order to show} = \textbf{We must show}

\textbf{Let} = \textbf{Given}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar Light}
\slidetitle{experiment}
$$
\xymatrix@=8em@M=.6em
{\mbox{Isabelle}\ar[d]\ar@{.}[r] & \mbox{HOL Light} \\ 
\mbox{Isar}\adviwait\ar@{.}[r] & \mbox{\textcolor{slidered}{Mizar Light\advirecord{ii}{\rlap{ II}}}}\ar@{<-}[u]}
$$
%\adviwait
%\adviplay[slidered]{ii}
\vfill
\end{slide}

\begin{slide}
\slidetitle{mixing procedural and declarative proof}
\begin{itemize}
\item[$\bullet$]
John's Mizar mode for HOL Light \& Isar for Isabelle:  \\
separate language on top of original system

\item[$\bullet$]
Mizar Light: \\
freely interleaving `old style' tactics and Mizar style proof
\end{itemize}
\adviwait
\bigskip

just define 8 new tactics in the system:
\textcolor{slidered}{`Mizar tactics'} \\
%\adviwait
`imitate' a Mizar proof in a tactic script
%
%(explains Mizar-style proof in the context of LCF-style provers)
\adviwait
\bigskip

HOL/Mizar Light: a `proof' is just an ML program \\
%
\textcolor{slidegreen}{no special parser on top of the ML interpreter} \\
%restricts syntax
\medskip
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar Light tactic types}
HOL ML types:
\begin{quote}
term, thm, tactic
\end{quote}

Mizar Light tactics:
\def\textttx#1{\rlap{\texttt{#1}}\phantom{\texttt{PER\char`_CASES}} }
\begin{quote}
\strut\textttx{BY} : string list $\to$ thm list $\to$ tactic \\
\textttx{HAVE} : string $\times$ term $\to$ tactic $\to$ tactic \\
\textttx{ASSUME} : string $\times$ term $\to$ tactic \\
\textttx{LET} : term list $\to$ tactic \\
\textttx{THUS} : string $\times$ term $\to$ tactic $\to$ tactic \\
\textttx{CONSIDER} : term list $\to$ (string $\times$ term) list $\to$ tactic $\to$ tactic$\hspace{-2em}$ \\
\textttx{TAKE} : term list $\to$ tactic \\
\textttx{PER\char`_CASES} : tactic $\to$ ((string $\times$ term) $\times$ tactic) list $\to$ tactic
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar Light II}
Mizar Light: \textcolor{slidegreen}{it's all about concepts}
\begin{center}\small
\textcolor{slidered}{\texttt{CONSIDER [`a:A`] ["A1",`\char`~(P:A->bool) a`] (BY ["A0"][]) THEN}} \\
\end{center}
important features missing: no `then'
\adviwait
\medskip

Mizar Light II: \textcolor{slidegreen}{more practical version}
\begin{center}
\textcolor{slidered}{\texttt{so consider ["a:A"] st "\char`~P a" at 1;}} \\
\end{center}
\adviwait
but: ML types of the tactics less meaningful \\
\phantom{but: }\verb|step| type instead of \verb|tactic| type
\adviwait

but: some renamings to fit ML syntax \\
\phantom{but: }\begin{tabular}{lcl}
\notion{label}$\,$\textbf{:} &$\rightarrow$& \verb|at| \notion{label} \vspace{-\smallskipamount}\\
\textbf{then} &$\rightarrow$& \verb|so| \vspace{-\smallskipamount}\\
\textbf{let} &$\rightarrow$& \verb|fix| \vspace{-\smallskipamount}\\
\textbf{such that} &$\rightarrow$& \verb|st| %\vspace{-\smallskipamount}\\
%\textbf{.=} &$\rightarrow$& \verb|...| \verb|=|
\vspace{-2em}
\end{tabular}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{translating a Coq proof to Mizar Light II}
Lu\'{\i}s Cruz-Filipe: Fundamental Theorem of Calculus

one of his lemmas translated into Mizar Light
\adviwait
\medskip

lemma: `\verb|Barrow|'s rule'
$$g' = f \;\Rightarrow\; \int_a^b f(x) \; dx = g(b) - g(a)$$
\begin{center}
\textcolor{slidered}{derivative g f $\;\Rightarrow\;$ integral a b f = g b -- g a}
\end{center}
\adviwait
\medskip

first order version \\
\adviwait
proved from functional version: \verb|FTC2|
$$g' = f \;\Rightarrow\; \Big(\int f\Big) - g = c$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{the Coq version}
\begin{flushleft}\footnotesize
\verb|Theorem |\advirecord{b1}{\texttt{Barrow}}\adviplay[slidered]{b1}\verb| : (a,b:IR)(iprop J a)->(iprop J b)->| \\
\verb|  (H:(Continuous_I (Min_leEq_Max a b) |\advirecord{f1}{\texttt{F}}\adviplay{f1}\verb|))(Ha,Hb:?)| \\
\verb|  (Integral H)[=](G0[@]b (G0_inc b Hb))[-](G0[@]a (G0_inc a Ha)).| \\
\adviwait
\verb|Intros.| \\
\verb|Elim |\advirecord{h1}{\texttt{FTC2}}\adviplay[slidered]{h1}\verb|; Intros c Hc.| \\
\verb|Inversion_clear Hc.| \\
\verb|Inversion_clear H2.| \\
\verb|RStepr ((G0[@]b (G0_inc b Hb))[+]c)[-]((G0[@]a (G0_inc a Ha))[+]c).| \\
\verb|Apply eq_transitive_unfolded with (|\advirecord{f2}{\texttt{G}}\adviplay{f2}\verb|[@]b Hb)[-](|\advirecord{f3}{\texttt{G}}\adviplay{f3}\verb|[@]a Ha).| \\
\verb|Unfold G; Simpl.| \\
\verb|Cut (x,y,z:IR)|\advirecord{w1}{\texttt{(z[=]x[+]y)->(y[=]z[-]x)}}\adviplay{w1}\verb|; Intros.| \\
\verb|Apply H2.| \\
\verb|Apply |\advirecord{x1}{\texttt{Integral\char`_plus\char`_Integral}}\adviplay{x1}\verb| with (Min3_leEq_Max3 x0 b a).| \\
\verb|Apply |\advirecord{x2}{\texttt{included\char`_imp\char`_Continuous}}\adviplay{x2}\verb| with J.| \\
\verb|Auto.| \\
\verb|Apply |\advirecord{x3}{\texttt{included3\char`_interval}}\adviplay{x3}\verb|; Auto.|
\verb|Apply eq_symmetric_unfolded.| \\
\verb|RStepr (x[+]y)[-]x; Algebra.| \\
\verb|Cut (x,y,z:IR)|\advirecord{w2}{\texttt{(x[-]y[=]z)->(x[=]y[+]z)}}\adviplay{w2}\verb|; Intros.|
\end{flushleft}
\vspace{-2em}
\vfill
\adviwait
\adviplay{b1}
\adviplay{h1}
%\adviplay[slidered]{f1}\adviplay[slidered]{f2}\adviplay[slidered]{f3}
%\adviwait
%\adviplay{f1}\adviplay{f2}\adviplay{f3}
\adviplay[slidered]{x1}\adviplay[slidered]{x2}\adviplay[slidered]{x3}
\adviwait
\adviplay{x1}\adviplay{x2}\adviplay{x3}
\adviplay[slidered]{w1}\adviplay[slidered]{w2}
\end{slide}

\begin{slide}
\slidetitle{the Coq version (continued)}
\begin{flushleft}\footnotesize
\verb|Opaque G.| \\
\verb|Cut (x:IR)(iprop J x)->(Hx,Hx':?)(G[@]x Hx)[-](G0[@]x Hx')[=]c; Intros.| \\
\verb|Apply cg_minus_wd; Apply H2; Auto.| \\
\verb|Simpl in H3.| \\
\verb|EApply eq_transitive_unfolded.| \\
\verb|2: Apply H3 with Hx:=(Hx,Hx').| \\
\advirecord{v1}{\texttt{Algebra}}\adviplay{v1}\verb|.| \\
\verb|Auto.| \\
\verb|Auto.| \\
\advirecord{v2}{\texttt{RStep}}\adviplay{v2}\verb| y[+](x[-]y).| \\
\advirecord{v3}{\texttt{Algebra}}\adviplay{v3}\verb|.| \\
\verb|Qed.|
\end{flushleft}
\adviwait
\adviplay[slidered]{v1}\adviplay[slidered]{v2}\adviplay[slidered]{v3}
\vfill
\end{slide}

\def\textttg#1{\textcolor{slidegray}{\texttt{#1}}}
\def\textttr#1{\textcolor{slidered}{\texttt{#1}}}

\begin{slide}
\slidetitle{the Mizar Light version}
\begin{flushleft}\footnotesize
\verb|let |\advirecord{b2}{\texttt{Barrow}}\adviplay[slidered]{b2}\verb| = theorem| \\
\verb|  "!J f g0 a b.| \\
\verb|     interval J /\ Continuous J f /\ Derivative J g0 f /\ a IN J /\ b IN J|$\hspace{-2em}$ \\
\verb|     ==> (integral' a b f = g0 b - g0 a)"| \\
\adviwait
\adviplay{b2}
\verb| [fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];|$\hspace{-3em}$ \\
\verb|  assume "interval J"|\textttg{\ at 0}\verb|;| \\
\verb|  assume "Continuous J f"|\textttg{\ at 1}\verb|;| \\
\verb|  assume "Derivative J g0 f"|\textttg{\ at 2}\verb|;| \\
\verb|  assume "a IN J /\ b IN J"|\textttg{\ at 3}\verb|;| \\
\adviwait
\verb|  consider ["x0:real"] st "x0 IN J"|\textttg{\ at 4 from [3]}\verb|;| \\
%\adviwait
\verb|  |\textttg{so}\verb| consider ["c:real"] st| \\
\verb|    "|\advirecord{s1}{\texttt{Feq J (Fprim f x0 - g0) (Fconst c)}}\adviplay{s1}\verb|"|\textttg{\ at 5 from [0;2] by [}\advirecord{h2}{\texttt{FTC2}}\adviplay[slidered]{h2}\textttg{]}\verb|;| \\
\adviwait
\adviplay{h2}
\adviplay[slidered]{s1}
\verb|  |\texttt{have}\verb| "|\advirecord{s2}{\texttt{!x.\ x IN J ==> (integral' x0 x f = g0 x + c)}}\adviplay[slidered]{s2}\verb|"|\textttg{\ at 6} \\
\verb|  proof| \\
\verb|   [fix ["x:real"];| \\
\verb|    assume "x IN J";| \\
\verb|    |\textttg{so}\verb| |\texttt{have}\verb| "(Fprim f x0 - g0) x = c"|\textttg{\ from [5] by [Feq; Fconst]}\verb|;| \\
\verb|    |\textttg{so}\verb| |\texttt{have}\verb| "integral' x0 x f - g0 x = c"|\textttg{\ by [Fminus; Fprim]}\verb|;|
\end{flushleft}
\vspace{-2em}
\vfill
%\adviwait
%\adviplay{s1}\adviplay{s2}
\end{slide}

\begin{slide}
\slidetitle{the Mizar Light version (continued)}
\begin{flushleft}\footnotesize
\verb|    |\texttt{hence}\verb| thesis|\textttg{\ by [}\advirecord{z1}{\texttt{ARITH\char`_CONV `(x - y = z) ==> (x = y + z)`}}\adviplay[slidegray]{z1}\textttg{]}\verb|];| \\
\verb|  |\texttt{have}\verb| "compact (x0 MIN b MIN a) (x0 MAX b MAX a) SUBSET J"| \\
\textttg{\ \ \ \ from [0;3;4] by [}\advirecord{y1}{\texttt{included3\char`_interval}}\adviplay[slidegray]{y1}\textttg{]}\verb|;| \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "continuous_I (x0 MIN b MIN a) (x0 MAX b MAX a) f"| \\
\textttg{\ \ \ \ from [1] by [}\advirecord{y2}{\texttt{included\char`_imp\char`_Continuous}}\adviplay[slidegray]{y2}\textttg{]}\verb|;| \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "integral' x0 b f = integral' x0 a f + integral' a b f"| \\
\textttg{\ \ \ \ by [}\advirecord{y3}{\texttt{Integral\char`_plus\char`_Integral}}\adviplay[slidegray]{y3}\textttg{]}\verb|;| \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "integral' a b f = integral' x0 b f - integral' x0 a f"| \\
\textttg{\ \ \ \ by [}\advirecord{z2}{\texttt{ARITH\char`_CONV `(z = x + y) ==> (y = z - x)`}}\adviplay[slidegray]{z2}\textttg{]}\verb|;| \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "... = (g0 b + c) - (g0 a + c)"|\textttg{\ from [3;6]}\verb|;| \\
\verb|  |\texttt{hence}\verb| "... = g0 b - g0 a"|\advirecord{z3}{\texttt{\ using K ARITH\char`_TAC using REWRITE\char`_TAC}}\adviplay[slidegray]{z3}\verb|];;|
\end{flushleft}
\adviwait
\adviplay[slidered]{y1}\adviplay[slidered]{y2}\adviplay[slidered]{y3}
\adviwait
\adviplay[slidegray]{y1}\adviplay[slidegray]{y2}\adviplay[slidegray]{y3}
\adviplay[slidered]{z1}\adviplay[slidered]{z2}\adviplay[slidered]{z3}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a formal proof sketch}
\begin{flushleft}\footnotesize
\verb|current_prover := sketch_prover;;|
\end{flushleft}
\begin{flushleft}\footnotesize
\verb|let Barrow = theorem| \\
\verb|  "!J f g0 a b.| \\
\verb|     interval J /\ Continuous J f /\ Derivative J g0 f /\ a IN J /\ b IN J|$\hspace{-2em}$ \\
\verb|     ==> (integral' a b f = g0 b - g0 a)"| \\
\verb| [fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];|$\hspace{-3em}$ \\
\verb|  assume "interval J; assume "Continuous J f"; assume "Derivative J g0 f";|$\hspace{-2em}$ \\
\verb|  assume "a IN J /\ b IN J";| \\
\advirecord{extra}{\texttt{\ \ consider ["x0:real"] st "x0 IN J";}}\adviplay{extra} \\
\verb|  consider ["c:real"] st "Feq J (Fprim f x0 - g0) (Fconst c)";| \\
\verb|  have "!x. x IN J ==> (integral' x0 x f = g0 x + c)";| \\
%\verb|  have "compact (x0 MIN b MIN a) (x0 MAX b MAX a) SUBSET J";| \\
%\verb|  have "continuous_I (x0 MIN b MIN a) (x0 MAX b MAX a) f";| \\
\verb|  have "integral' x0 b f = integral' x0 a f + integral' a b f";| \\
\verb|  have "integral' a b f = integral' x0 b f - integral' x0 a f";| \\
\verb|  have "... = (g0 b + c) - (g0 a + c)";| \\
\verb|  thus "... = g0 b - g0 a"];;|
\end{flushleft}
\adviwait
\adviplay[slidered]{extra}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a shorter proof (formal proof sketch)}
\begin{flushleft}\footnotesize
\verb|current_prover := sketch_prover;;|
\end{flushleft}
\begin{flushleft}\footnotesize
\verb|let Barrow = theorem| \\
\verb|  "!J f g0 a b.| \\
\verb|     interval J /\ Derivative J g0 f /\ a IN J /\ b IN J| \\
\verb|     ==> (integral' a b f = g0 b - g0 a)"| \\
\verb| [fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];|$\hspace{-3em}$ \\
\verb|  assume "interval J"; assume "Derivative J g0 f";| \\
\verb|  assume "a IN J /\ b IN J";| \\
\verb|  consider ["c:real"] st "Feq J (Fprim f a - g0) (Fconst c)";| \\
\verb|  have "!x. x IN J ==> (integral' a x f - g0 x = c)";| \\
\verb|  have "integral' a a f = &0";| \\
\verb|  have "c = --g0 a";| \\
\verb|  have "integral' a b f - g0 b = c";| \\
\verb|  thus "integral' a b f = g0 b - g0 a"];;|
\end{flushleft}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a shorter proof (full proof)}
\begin{flushleft}\footnotesize
\verb|let Barrow = theorem| \\
\verb|  "!J f g0 a b.| \\
\verb|     interval J /\ Derivative J g0 f /\ a IN J /\ b IN J| \\
\verb|     ==> (integral' a b f = g0 b - g0 a)"| \\
\verb| [fix ["J:real->bool"; "f:real->real"; "g0:real->real"; "a:real"; "b:real"];|$\hspace{-3em}$ \\
\verb|  assume "interval J"|\textttg{\ at 0}\verb|;| \\
\verb|  assume "Derivative J g0 f"|\textttg{\ at 1}\verb|;| \\
\verb|  assume "a IN J /\ b IN J"|\textttg{\ at 2}\verb|;| \\
\verb|  |\textttg{so}\verb| consider ["c:real"] st| \\
\verb|    "Feq J (Fprim f a - g0) (Fconst c)"|\textttg{\ from [0;1] by [}\textttg{FTC2}\textttg{]}\verb|;| \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "!x. x IN J ==> (integral' a x f - g0 x = c)"|\textttg{\ at 4} \\
\textttg{\ \ \ \ using (REWRITE\char`_TAC o map (REWRITE\char`_RULE[Feq; Fconst; Fminus; Fprim]))}\verb|;|$\hspace{-2em}$ \\
\verb|  |\texttt{have}\verb| "integral' a a f = &0"|\textttg{\ by [INTEGRAL'; INTEGRAL\char`_NULL; REAL\char`_LE\char`_REFL]}\verb|;|$\hspace{-2em}$ \\
\verb|  |\textttg{so}\verb| |\texttt{have}\verb| "c = --g0 a"|\textttg{\ at 6 from [2;4] by [ARITH\char`_CONV `\char`&0 - x = --x`]}\verb|;| \\
\verb|  |\texttt{have}\verb| "integral' a b f - g0 b = c"|\textttg{ from [2;4]}\verb|;| \\
\verb|  |\texttt{hence}\verb| thesis|\textttg{\ from [6] by [ARITH\char`_CONV `(--y = w - x) ==> (w = x - y)`]}\verb|];;|$\hspace{-2em}$
\end{flushleft}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{implementing a Mizar mode}
\slidetitle{the easy part}
implementing the `natural deduction' behavior of the steps \\
Mizar Light \& Bas' `math mode' show: this is easy
\adviwait
\medskip

support for writing steps in a Mizar mode? \\
Mizar steps need much more typing
\begin{center}
\begin{tabular}{ccc}
\verb|Intro.| &$\;\to\;$&
\textbf{assume} \notion{label}: \notion{formula}$\,$\textbf{;}
\end{tabular}
\end{center}

menu items to generate proof text: \textcolor{slidegreen}{interactive mode}
\adviwait
\medskip

but: having `meta-scripts' to generate proof text is a bad idea \\
\textcolor{slidered}{the file that the user interacts with} should be understandable!
\vfill
\end{slide}

\begin{slide}
\slidetitle{the hard part}
Mizar's \textbf{by} tactic: not clear how to map it to Coq \\
\adviwait
possibility:
\begin{itemize}
\item[$\bullet$]
put all statements referred to in a hint class \verb|H|
\item[$\bullet$]
solve sub-goal for the statement using:
\textcolor{slidered}{\texttt{Intuition}$\,$ \texttt{Auto}$\,$ \texttt{with}$\,$ \texttt{H}}
\end{itemize}
\adviwait
\medskip

%but!
%this won't be powerful enough \\
\textcolor{slidegreen}{how to write a `Mizar style' proof that uses other tactics?} \\
%\adviwait
\verb|Elim|?
%\adviwait
\verb|Induction|?
%\adviwait
\verb|Inversion|?
%\adviwait
\verb|Omega|?
%\adviwait
\verb|Field|?
%\adviwait
own tactics?
\adviwait
\medskip

approach in Mizar Light:
%(similar approach in Isar)
\begin{center}
{\dots} \textbf{using} \notion{tactic}$\,$\textbf{;}
\end{center}
\adviwait
my experience with this in practice: I don't like it \\
I want to think about the proof, not about why a tactic doesn't work!
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{working in an incomplete proof text}
Mizar style of working: \\
one often has to reprocess the whole proof when a change is made
\adviwait
\medskip

\begin{tabular}{rl}
\textcolor{slidegreen}{Proof General}: & split between correct text and unprocessed text \\
\textcolor{slidegreen}{Mizar}: & everything is checked everywhere all the time
\end{tabular}
\adviwait
\medskip

working \textcolor{slidered}{behind} errors
\adviwait

%\begin{itemize}
%\item[$\bullet$]
%most important class of errors: reasoning errors \\
%%\adviwait
explicit formulas make error recovery possible \\
%\adviwait
(like adding temporary axioms manually)
%\adviwait
%\item[$\bullet$]
%also (less important): type errors, syntax errors
%\end{itemize}
\adviwait
\bigskip

\begin{center}
\textbf{Mizar demo}
\adviwait
\adviembed{/home/freek/talks/mathincoq/mizdemo/run}
\end{center}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{conclusion}
\slidetitle{what needs to be done?}
\textcolor{slidered}{someone} should do a proper Mizar mode for Coq
\begin{itemize}
\item[$\bullet$]
no significant change of the Coq system will be needed
%\adviwait
\item[$\bullet$]
\textcolor{slidegreen}{the problem of an appropriate \textbf{by} for Coq will need to be solved first}
%\textcolor{slidegreen}{appropriate \textbf{by} for Coq?}
%\adviwait
%\smallskip
%
%properties of Mizar's \textbf{by} tactic:
%\begin{itemize}
%\item
%\textbf{complete}
%
%(prove anything with sufficiently many steps)
%%\adviwait
%
%\item
%\textbf{efficient}
%
%(if it fails, it fails fast)
%\end{itemize}
%\adviwait
%
%\textcolor{slidegreen}{important properties?}
\end{itemize}
\vfill
\end{slide}

\end{document}