\documentclass[runningheads]{llncs}
\usepackage[all]{xy}
\usepackage{latexsym}
\raggedbottom
\def\toolong{$\hspace{-3.2cm}$}
\begin{document}
\title{The formal proof sketch challenge}
\author{Freek Wiedijk}
\institute{University of Nijmegen}
\maketitle
\begin{abstract}
A {\em formal proof sketch\/} is a way to present a formal
proof in a style that is close to an informal proof, but which also is
a skeleton of the full formal proof (this makes it easy to relate the
presentation to the detailed formalization.)
Recently to us every informal proof has started to feel like a {\em challenge\/},
to write down the corresponding formal proof sketch.
We take on this challenge for the informal proof of {\em Newman's lemma\/}
from Henk Barendregt's book about $\lambda$-calculus.
The specific difficulty of that proof is its main
part,
which just is a pair of diagrams without any explanation.
\end{abstract}
\section{Introduction}
\subsection{Problem}
Often when encountering a nice piece of mathematics, we feel a strong desire
to formalize it.
This feeling probably is similar to the desire of an artist to create
a beautiful painting when he sees a beautiful woman.
Recently we introduced the notion of a
formal proof sketch \cite{wie:02}.
For us the urge to find the formal proof sketch corresponding to a specific
informal proof turns out to be
even stronger than the desire to create a formalization in some less direct
way.
In \cite{wie:02} we presented formal proof sketches for two small proofs only
(a proof of the irrationality
of $\sqrt{2}$ from Hardy \& Wright \cite{har:wri:60} and
a proof of a small lemma from linear algebra), but now every informal proof
that we encounter seems to demand
that it wants a formal proof sketch of its own.
We call this urge that makes us want to find out what
formal proof sketches shaped
after informal proofs look like, the {\em formal proof sketch challenge}.
The challenge then, is to get as close as possible to the original.
Henk Barendregt told us that he
thought that a good example for experimenting with
formal proof sketches would be the proof of Newman's lemma
(a simple lemma about confluence from the theory of abstract rewriting).
In our turn we thought that it would be interesting to investigate the
specific proof of Newman's lemma that Henk gave in his classic
textbook about $\lambda$-calculus \cite{bar:84}.
The result of this investigation is this note.
A further reason to be interested in this particular proof is that
Henk told us that he thought he remembered that
at some point he was not able to explain it to N.G.~de Bruijn.
If this indeed has happened, then apparently
the proof from \cite{bar:84} is not completely trivial.
Maybe the formal proof sketch from this paper can help making
that specific version of the proof more understandable to people
who have a formalist bend.
\subsection{Approach}
We made a formal proof sketch of
Henk's version of Newman's lemma following the same approach that
we used in \cite{wie:02}.
That is, we made a formal proof sketch using the exact syntax of the current
version of the
Mizar system, and we even tried to be `compatible' with the
big Mizar library that accompanies the Mizar system
(the `Mizar mathematical library'
or MML).
\subsection{Related Work}
The proof of Newman's lemma is very simple.
This makes it one of the basic examples for all of the major
proof checking systems,
like for instance ACL2, Coq and Isabelle.
In the Mizar mathematical library Newman's lemma is proved in article
\verb|REWRITE1| by Grzegorz Bancerek.
Diagrammatic reasoning is an active field of research.
An interesting system that implements proofs
both involving logical steps and diagrams, is
the Hyperproof system \cite{bar:etc:95} by Jon Barwise and John Etchemendy.
In \cite{bar:etc:98} they explain the philosophy behind this system.
\subsection{Contribution}
We give a formal proof sketch for an informal proof that is not primarily
textual.
We also present the full formalization that one gets by
`completing' the formal proof sketch.
Despite the non-textual nature of the original,
we show that the formal proof sketch
manages to closely follow the informal proof.
This shows that Mizar formal proof sketches are a versatile
way to present formal mathematics in an informally
acceptable way.
When discussing the relation between the diagram and the
corresponding part of the formal proof sketch,
we show that a diagram is a dynamic entity that actually
consists of a series of growing diagrams.
We explain a mechanism that a proof assistant can use
to automatically generate diagrams from a proof.
We discuss the relation between the presentation
of our formal proof sketch and the treatment
of rewriting that is in the Mizar mathematical library,
both conceptually and notationally.
We compare Henk's version of the proof to the proof of Newman's lemma
that is in the Mizar mathematical library.
\subsection{Outline}
In Section~\ref{sketch} we present both the informal proof
from \cite{bar:84} and the corresponding formal proof sketch.
In Section~\ref{diagrams} we discuss the relation between
the diagram from the original and the steps in the formal
proof sketch.
In Section~\ref{full} we present the full formalization of
the proof,
together with the statements of the lemmas that it uses.
In Section~\ref{notation} we discuss the relation between
the notation that is used in the Mizar mathematical library
and our notation.
In Section~\ref{rewrite1} we present the proof of Newman's
lemma from the Mizar mathematical library by way of another
-- this time {\em extracted\/} --
formal proof sketch.
\section{A formal proof sketch of Newman's lemma}\label{sketch}
Here is a copy of part of page 58 from \cite{bar:84}:\par
\smallskip\noindent{\hfill{\it informal proof\/}}\vspace{-\medskipamount}
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}
\noindent
3.1.25. {\sc Proposition.} {\em For notions of reduction one has
$$\mbox{\rm SN}\land\mbox{\rm WCR}\Rightarrow\mbox{\rm CR}$$}%
{\sc Proof.} By SN each term $R$-reduces to an $R$-nf. It suffices to show that this
$R$-nf is unique. Call $M$ {\em ambiguous\/} if $M$ $R$-reduces to two distinct $R$-nf's.
For such $M$ one has $M\to_R M'$ with $M'$ ambiguous (use WCR, see figure
3.3). Hence by SN ambiguous terms do not exist.
\medskip
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] &&&&
& M\ar[d] &\\
& M'\ar@{->>}[ddl]\ar@{->>}[dr] && \ar@{->>}[dl]\ar@{->>}[ddr] &&\mbox{ or }&
& M'\ar@{->>}[d] &\\
&& \ar@{->>}[d] &&&&
& \ar@{->>}[dl]\ar@{->>}[dr] &\\
M_1 && M_3 && M_2 &&
M_1 && M_2}
$$
\begin{center}
{\sc fig.}~3.3.
\end{center}
\vspace{-\medskipamount}\hfill$\Box$\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
This is a proof of the statement known as {\em Newman's lemma} \cite{new:42}.
It relates some properties of abstract `notions of reduction'
(a binary relation looked at as the abstraction of a rewrite system).
In this, the abbreviation `SN' stands for `strongly normalizing'
(which means that there is no infinite reduction sequence),
`CR' stands for the `Church-Rosser' property (which means
that reducts of a common original always can be reduced in a converging
way, i.e., to a common reduct), and `WCR' stands for `weakly Church-Rosser'
(which means that this Church-Rosser property only has to hold when the
diverging reductions are only one step long).
And here is the corresponding `formal proof sketch' (a notion which we introduced in \cite{wie:02}):
\pagebreak
\smallskip\noindent{\hfill{\it formal proof sketch\/}}\vspace{-\medskipamount}
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
\begin{quote}\footnotesize
\verb| reserve R for nf_inhabited notion_of_reduction;|\\
\verb| reserve M,M',M'',M''' for Term of R;|\\
\verb| reserve M1,M2,M3 for Nf of R;|
\medskip
\verb|theorem 3_1_25:|\\
\verb| R is SN & R is WCR implies R is CR|\\
\verb|proof|\\
\verb| assume that R is SN and R is WCR;|\\
\verb| for M ex M1 st M reduces_to M1;|\\
\verb| (for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2)|\\
\verb| implies R is CR;|\\
\verb| defpred ambiguous[Term of R] means|\\
\verb| ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;|\\
\verb| now|\\
\verb| now|\\
\verb| let M such that ambiguous[M];|\\
\verb| thus ex M' st M ---> M' & ambiguous[M']|\smallskip\\
\verb| |\hspace{-\fboxsep}\hspace{-4\fboxrule}$\!$%
\fbox{\begin{tabular}[b]{l}{\tt$\,$proof}\\
{\tt$\,$\ consider M1,M2 such that M -->> M1 \& M -->> M2 \& M1 <> M2;}\\
{\tt$\,$\ per cases;}\\
{\tt$\,$\ suppose not ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\
{\tt$\,$\ \ consider M' such that M ---> M' \& M' -->> M1;}\\
{\tt$\,$\ \ consider M'' such that M ---> M'' \& M'' -->> M2;}\\
{\tt$\,$\ \ consider M''' such that M' -->> M''' \& M'' -->> M''';}\\
{\tt$\,$\ \ consider M3 such that M''' -->> M3;}\\
{\tt$\,$\ \ take M';}\\
{\tt$\,$\ \ thus thesis;}\\
{\tt$\,$\ suppose ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\
{\tt$\,$\ \ consider M' such that M ---> M' \& M' -->> M1 \& M' -->> M2;}$\,$\\
{\tt$\,$\ \ take M';}\\
{\tt$\,$\ \ thus thesis;}\\
{\tt$\,$end;}\end{tabular}}\rlap{\tt$\;$::$\,${\it fig.$\,$3.3}}\\\strut
\verb| end;|\\
\verb| thus not ex M st ambiguous[M];|\\
\verb| end;|\\
\verb| thus thesis;|\\
\verb|end;|\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{quote}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
Note that we have used the {\em variable convention\/} here that the
variables called $M_1$, $M_2$, $M_3$, {\dots} are referring to
normal forms.
Mizar has the \verb|reserve| statement to introduce such variable conventions.
Alternatively we could have put `\verb|being| \verb|Nf| \verb|of| \verb|R|'
at each place where such a variable was introduced.
That would have made the formal proof sketch more explicit (and
therefore maybe a bit easier to follow), but also more cluttered.
The `notion of reduction' that this formal proof sketch talks about has
the attribute \verb|nf_inhabited|.
Mizar only allows non-empty
types and
we wanted to use a type \verb|Nf| \verb|of| \verb|R|
for the normal forms of \verb|R|.
Therefore we only prove the theorem for notions of reduction that have
one or more normal forms.
(In a sense that does not restrict the theorem,
because all \verb|SN| notions of reduction
are \verb|nf_inhabited|.)
One could get rid of the \verb|nf_inhabited| by not using the
\verb|Nf| \verb|of| \verb|R| type, but replacing all quantifiers
like:
\begin{quote}
\verb|for M1 being Nf of R holds |\dots
\end{quote}
by corresponding quantifiers like:
\begin{quote}
\verb|for M1 being Term of R st M1 is_nf holds |\dots
\end{quote}
The part of the proof in the box corresponds to the diagram from the original.
One gets a second, smaller, formal proof sketch of the same
original by replacing the text in the box by a single
semi-colon.
To show that this shortened formal proof sketch corresponds very
closely to the original text, we repeat the
two versions here, interleaved with each other:
\begin{quote}
{\sc Proof.}
\begin{verbatim}
proof
assume that A1: R is SN and R is WCR;
\end{verbatim}
By SN each term $R$-reduces to an $R$-nf.
\begin{verbatim}
for M ex M1 st M reduces_to M1 by A1;
\end{verbatim}
It suffices to show that this $R$-nf is unique.
\begin{verbatim}
(for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds
M1 = M2) implies R is CR;
\end{verbatim}
Call $M$ {\em ambiguous\/} if $M$ $R$-reduces to two distinct $R$-nf's.
\begin{verbatim}
defpred ambiguous[Term of R] means
ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;
\end{verbatim}
For such $M$ one has $M\to_R M'$ with $M'$ ambiguous.
\begin{verbatim}
now
now
let M such that ambiguous[M];
thus ex M' st M ---> M' & ambiguous[M'];
end;
\end{verbatim}
Hence by SN ambiguous terms do not exist.
\begin{verbatim}
thus not ex M st ambiguous[M] by A1;
end;
\end{verbatim}
$\Box$
\begin{verbatim}
thus thesis;
end;
\end{verbatim}
\end{quote}
It should be noted that we did not create this formal proof sketch
by first doing a full formalization,
and then cutting out the sketch afterward.
Instead we wrote the formal proof sketch directly, and only after-wards
completed it to a full formalization (see Section~\ref{full}).
It is one of the strengths of the Mizar language that this is possible,
and in fact even easy (the difficult part of doing a
Mizar formalization is finding the proper references to the Mizar mathematical
library.)
\section{Proofs and diagrams}\label{diagrams}
The part of the formal proof sketch that corresponds to the
diagram from the original, in fact corresponds to a {\em sequence\/}
of growing diagrams.
This means that the diagram in `fig.~3.3' is not one diagram
but a whole series.
A paper book can not show this series (at least not without using
more paper than is worth it), but an interactive proof in a
computer can.
To be able to see these `living diagrams'
might be a good reason for wanting to formalize mathematics.
Between each subsequent pair of steps in the proof there
is a `natural' diagram that shows the situation between the steps:
\begin{quote}
$$\xymatrix@=1.6em{M}\medskip$$
\begin{verbatim}
consider M1,M2 such that M -->> M1 & M -->> M2 & M1 <> M2;
\end{verbatim}
$$\xymatrix@=1.6em{& M\ar[dl]\ar[dr] & \\
M_1 && M_2}\medskip$$
\begin{verbatim}
consider M' such that M ---> M' & M' -->> M1;
\end{verbatim}
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[ddrr] && \\
& M'\ar@{->>}[dl] && & \\
M_1 && && M_2}\medskip$$
\begin{verbatim}
consider M'' such that M ---> M'' & M'' -->> M2;
\end{verbatim}
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] && \\
& M'\ar@{->>}[dl] && M''\ar@{->>}[dr] & \\
M_1 && && M_2}\medskip$$
\begin{verbatim}
consider M''' such that M' -->> M''' & M'' -->> M''';
\end{verbatim}
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] && \\
& M'\ar@{->>}[ddl]\ar@{->>}[dr] && M''\ar@{->>}[dl]\ar@{->>}[ddr] & \\
&& M''' && \\
M_1 && && M_2}\medskip$$
\begin{verbatim}
consider M3 such that M''' -->> M3;
\end{verbatim}
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] && \\
& M'\ar@{->>}[ddl]\ar@{->>}[dr] && M''\ar@{->>}[dl]\ar@{->>}[ddr] & \\
&& M'''\ar@{->>}[d] && \\
M_1 && M_3 && M_2}$$
\end{quote}
These diagrams can be generated automatically by a proof assistant
in the following way:
At every point in the proof there is a proof context (or
proof goal) consisting
of the statement that needs to be proved (what Mizar calls
the `thesis'), the {\em variables\/} that have been introduced by
\verb|let| and \verb|consider| statements, and the {\em statements\/}
in the proof that can be referred to.
Now one can select from those variables the ones that have a
certain type (in the case of the example: \verb|Term| \verb|of|
\dots) and the from those statements the statement that involve
those variables and
that have a certain shape (in the case of the example:
{\dots} \verb|--->| {\dots} and {\dots} \verb|-->>| {\dots}).
Both sets are steadily growing through a proof.
A {\em diagram\/} is a graphical representation of
both sets.
In the example it consists of a graph with the variables at
the vertices and the two kinds of predicates represented by
two kind of edges.
Of course this graph needs to be laid out in the plane,
but there exist algorithms that can do that automatically
(a nice example of an implementation
of such an algorithm \cite{gan:kou:nor:vo:93} is the \verb|dot| program
from AT\&T's \verb|graphviz| system).
Note that in a proof by contradiction the set of relevant
statements might become inconsistent.
It needs investigation how to pleasantly represent such a
situation in a diagram.
Note that the diagrams might be interactive:
instead of having the proof assistant determining the layout of the
diagram, the user might interactively drag elements of the
diagram around.
Note that the diagrams can be graphically consistent along the
series (so later diagrams are obtained by adding elements
to earlier diagrams, without moving the elements that
are already present), but they do not need to be.
Finally note that for big proofs it might be advantageous
to leave out part of the proof context from the diagram,
either under control of the algorithms generating the diagram
from the proof context or under control of the user.
In this example the diagrams represent reductions in
an abstract reduction system but the basic principles are
the same for other kinds of diagrams like geometrical
diagrams, diagrams from graph theory or
commuting diagrams from category theory.
\section{The full formalization}\label{full}
Here is the full formalization that one gets by `completing' the
formal proof sketch from Section~\ref{sketch}.
The parts that already were present in the formal proof sketch
have been underlined:
\noindent{\hfill{\it full formalization\/}}\vspace{-\medskipamount}
\noindent\rule{\hsize}{\fboxrule}\vspace{-\smallskipamount}
%Def9,Def10,Def11,Th6,Th7,Th8,Th9,SN_induction1
\begin{verse}\footnotesize
\verb| |\underbar{\tt{reserve R for nf\_inhabited notion\_of\_reduction;}}\\
\verb| |\underbar{\tt{reserve M,M',M'',M''' for Term of R;}}\\
\verb| |\underbar{\tt{reserve M1,M2,M3 for Nf of R;}}\\
\medskip
\underbar{\tt{theorem 3\_1\_25:}}\\
\verb| |\underbar{\tt{R is SN \& R is WCR implies R is CR}}\\
\underbar{\tt{proof}}\\
\verb| |\underbar{\tt{assume that}}\\
\verb|A1: |\underbar{\tt{R is SN and}}\\
\verb|A2: |\underbar{\tt{R is WCR;}}\\
\verb|A3: R is WN by A1,Th9;|\\
\verb| then |\underbar{\tt{for M ex M1 st M reduces\_to M1}}\verb| by Def10|\underbar{\tt{;}}\\
\verb|A4: |\underbar{\tt{(for M,M1,M2 st M reduces\_to M1 \& M reduces\_to M2 holds M1 = M2)}}\toolong\\
\verb| |\underbar{\tt{implies R is CR}}\\
\verb| proof|\\
\verb| assume|\\
\verb|A5: for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2;|\toolong\\
\verb| let M,M',M'';|\\
\verb| assume|\\
\verb|A6: M -->> M' & M -->> M'';|\\
\verb| consider M1 such that|\\
\verb|A7: M' -->> M1 by A3,Def10;|\\
\verb| consider M2 such that|\\
\verb|A8: M'' -->> M2 by A3,Def10;|\\
\verb| M -->> M1 & M -->> M2 by A6,A7,A8,Th6;|\\
\verb| then M' -->> M1 & M'' -->> M1 by A5,A7,A8;|\\
\verb| hence thesis;|\\
\verb| end|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{defpred ambiguous[Term of R] means}}\\
\verb| |\underbar{\tt{ex M1,M2 st \$1 reduces\_to M1 \& \$1 reduces\_to M2 \& M1 <> M2;}}\\
\verb|A9: |\underbar{\tt{now}}\\
\verb|A10: |\underbar{\tt{now}}\\
\verb| |\underbar{\tt{let M such that}}\\
\verb|A11: |\underbar{\tt{ambiguous[M];}}\\
\verb| |\underbar{\tt{thus ex M' st M ---> M' \& ambiguous[M']}}\\
\verb| |\underbar{\tt{proof}}\\
\verb| |\underbar{\tt{consider M1,M2 such that}}\\
\verb|A12: |\underbar{\tt{M -->> M1 \& M -->> M2 \& M1 <> M2}}\verb| by A11|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{per cases;}}\\
\verb| |\underbar{\tt{suppose}}\\
\verb|A13: |\underbar{\tt{not ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}}\\
\verb| M1 is_nf & M2 is_nf by Def9;|\\
\verb| then|\\
\verb|A14: M <> M1 & M <> M2 by A12,Th8;|\\
\verb| then |\underbar{\tt{consider M' such that}}\\
\verb|A15: |\underbar{\tt{M ---> M' \& M' -->> M1}}\verb| by A12,Th7|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{consider M'' such that}}\\
\verb|A16: |\underbar{\tt{M ---> M'' \& M'' -->> M2}}\verb| by A12,A14,Th7|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{consider M''' such that}}\\
\verb|A17: |\underbar{\tt{M' -->> M''' \& M'' -->> M'''}}\verb| by A2,A15,A16,Def11|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{consider M3 such that}}\\
\verb|A18: |\underbar{\tt{M''' -->> M3}}\verb| by A3,Def10|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{take M';}}\\
\verb| M' -->> M3 & M'' -->> M3 by A17,A18,Th6;|\\
\verb| then M' -->> M1 & M' -->> M3 & M1 <> M3 by A13,A15,A16;|\\
\verb| |\underbar{\tt{hence thesis}}\verb| by A15|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{suppose ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}}\\
\verb| then |\underbar{\tt{consider M' such that}}\\
\verb|A19: |\underbar{\tt{M ---> M' \& M' -->> M1 \& M' -->> M2;}}\\
\verb| |\underbar{\tt{take M';}}\\
\verb| |\underbar{\tt{thus thesis by A12,A19;}}\\
\verb| |\underbar{\tt{end;}}\\
\verb| |\underbar{\tt{end;}}\\
\verb| |\underbar{\tt{thus not ex M st ambiguous[M]}}\verb| from SN_induction1(A1,A10)|\underbar{\tt{;}}\\
\verb| |\underbar{\tt{end;}}\\
\verb| |\underbar{\tt{thus thesis}}\verb| by A4,A9|\underbar{\tt{;}}\\
\underbar{\tt{end;}}\vspace{-\medskipamount}\vspace{-\smallskipamount}
\end{verse}
\noindent\rule{\hsize}{\fboxrule}\par\medskip
\noindent
Note that the statement from the original:
\begin{quote}
{\em It suffices to show that this $R$-nf is unique.}
\end{quote}
needs a multi-line sub-proof here.
That proof corresponds to the diagram:
$$\xymatrix@=1.6em{& M\ar@{->>}[dl]\ar@{->>}[dr] & \\
M'\ar@{->>}[d] && M''\ar@{->>}[d] \\
M_1\ar@{=}[rr] && M_2}\smallskip$$
The formalization uses the following basic lemmas:
\begin{flushleft}
\verb|theorem Th6: M -->> M' & M' -->> M'' implies M -->> M'';|
\medskip
\verb|theorem Th7: M -->> M'' implies|\\
\verb| M = M'' or ex M' st M ---> M' & M' -->> M'';|
\medskip
\verb|theorem Th8: M is_nf & M -->> M' implies M = M';|
\medskip
\verb|theorem Th9: R is SN implies R is WN;|
\medskip
\verb|scheme SN_induction1 {R()->notion_of_reduction, X[set]}:|\\
\verb| for M being Term of R() holds not X[M]|\\
\verb|provided|\\
\verb| R() is SN and|\\
\verb| for M being Term of R() st X[M]|\\
\verb| ex M' being Term of R() st M ---> M' & X[M'];|
\end{flushleft}
We considered these statements general enough that their
proofs should not be part of the proof of Newman's lemma.
The last statement \verb|SN_induction1|, is equivalent to Noetherian induction:
\begin{flushleft}
\verb|scheme SN_induction {R()->notion_of_reduction, X[set]}:|\\
\verb| for M being Term of R() holds X[M]|\\
\verb|provided|\\
\verb| R() is SN and|\\
\verb| for M being Term of R() st|\\
\verb| for M' being Term of R() st M ---> M' holds X[M']|\\
\verb| holds X[M];|
\end{flushleft}
Although this looks different from \verb|SN_induction1|, it is
exactly the same
when one replaces \verb|X[M]| by \verb|not| \verb|X[M]|.
Both are higher order statements.
Mizar is a first order language, but it knows this kind of
higher order statements as {\em schemes}.
Mizar has the language of set theory, so it can state the
same thing in a first order way as well:
\begin{flushleft}
\verb|attr R is SN means|\\
\verb| for X being Subset of field R st|\\
\verb| (for M st for M' st M ---> M' holds M' in X holds M in X) holds|\\
\verb| for M holds M in X;|
\end{flushleft}
However, because Mizar has no good $\lambda$-abstraction, the
schematic form is easier to apply and therefore it is the one that we used
in the formalization.
Note that this lack of proper $\lambda$-abstraction is not
a problem for making formal proof sketches look like informal mathematics,
because in informal mathematics $\lambda$-notation is almost never used.
\section{Notation and the Mizar mathematical library}\label{notation}
The big Mizar library called MML -- Mizar mathematical library --
already contains a treatment of rewriting in article \verb|REWRITE1|.
However the notation used there is not exactly the same as the
one used in the proof from Henk's book.
Mizar has the possibility to define {\em synonyms},
so we were able to make the notation closer to the one in
the original than if we had just used the notation that
was already present in the MML.
In this table we show in the first column the notation used
in Henk's proof,
in the second column the notation for this from the MML, and
in the third column the notation that we used:
\medskip
\begin{center}
\begin{tabular}{lll}
\hline\noalign{\smallskip}
{\em Henk's book\/} & {\em MML\/} & {\em formal proof sketch\/}\\
\noalign{\vspace{0.5\smallskipamount}}\hline\noalign{\smallskip}
notion of reduction & \verb|Relation| & \verb|notion_of_reduction| \\
term & \verb|set| & \verb|Term of R| \\
$R$ is SN & \verb|R is strongly-normalizing|$\quad$ & \verb|R is SN| \\
$R$ is WCR & \verb|R is locally-confluent| & \verb|R is WCR| \\
$R$ is CR & \verb|R is confluent| & \verb|R is CR| \\
$M \to_R M'$ & \verb|[M,M'] in R| & \verb|M ---> M'| \\
$M$ $R$-reduces to $M'$$\quad$ & \verb|R reduces M,M'| & \verb|M reduces_to M'| \\
$M$ is a $R$-nf & \verb|M is_a_normal_form_wrt R| & \verb|M is_nf| \\
$M$ is ambiguous & & \verb|ambiguous[M]|\\
\noalign{\smallskip}\hline
\end{tabular}
\smallskip
\end{center}
There were two design choices for modeling
\verb|notion_of_reduction| in our formalization:
\begin{itemize}
\item
In the MML there are two types that can be used
to model an abstract reduction system.
In article \verb|RELAT_1| the type \verb|Relation| is defined
to be an arbitrary set of pairs.
This is the concept that is used in article \verb|REWRITE1|.
In article \verb|ORDERS_1| the type \verb|RelStr| (`relational structure')
is defined by:
\begin{flushleft}
\verb|definition|\\
\verb| struct(1-sorted) RelStr (#|\\
\verb| carrier -> set,|\\
\verb| InternalRel -> Relation of the carrier|\\
\verb| #);|\\
\verb|end;|
\end{flushleft}
Here one separates the carrier of the reduction structure from the
reduction relation itself.
This is more accurate when one wants to model notions of reduction,
but we wanted to reuse as much from
\verb|REWRITE1| as possible, so we chose to define \verb|notion_of_reduction|
as:
\begin{flushleft}
\verb|definition|\\
\verb| mode notion_of_reduction is non empty Relation|\\
\verb|end;|
\end{flushleft}
\item
In Mizar a predicate takes two comma-separated
lists of arguments (possibly single or maybe even empty)
on the left and the right of the relation symbol.
Using that format it is hard to imitate the $M \to_R M'$ notation
(it would become \verb|M| \verb|--->| \verb|R,M'|, which is ugly).
We chose to omit the $R$ from this notation, and have the
current reduction relation {\em inferred\/} from the type of
the terms.
In order to make this work, the type needs to be a dependent
type \verb|Term| \verb|of| \verb|R|:
\begin{flushleft}
\verb|definition let R be notion_of_reduction;|\\
\verb| mode Term of R is Element of field R;|\\
\verb|end;|
\end{flushleft}
Using this type, one defines the reduction arrow by:
\begin{flushleft}
\verb|definition let R be notion_of_reduction;|\\
\verb| let M,M' be Term of R;|\\
\verb| pred M ---> M' means [M,M'] in R;|\\
\verb|end;|
\end{flushleft}
The \verb|R| can be reconstructed from the types of the \verb|M|
and \verb|M'|, so it does not need to be part of the notation.
The choice to use dependent types (to be able to omit
the reduction relation from the notation) causes
the attributes like \verb|SN| and so on to become `non clusterable'.
This means that Mizar is not able to infer attributes by itself
using so-called 'cluster rules'.
For instance, we needed to state the fact that \verb|R| \verb|is| \verb|WN|
explicitly in our proof (statement \verb|A3|).
If the attributes had been clusterable, we also could have phrased the
statement of the theorem as a `cluster':
\begin{center}
\verb|cluster SN WCR -> CR notion_of_reduction|
\end{center}
which looks more like the statement of the original informal proof:
$$\mbox{\rm SN}\land\mbox{\rm WCR}\Rightarrow\mbox{\rm CR}$$
than what is now in the formal proof sketch.
\end{itemize}
Our decision to be compatible with the MML blocked some notational
possibilities.
The symbol \verb|term| is already used in the MML for a function,
so it can not be used for a type as well, and so we can not write
\verb|term| \verb|of| \verb|R|.
Instead we used \verb|Term| \verb|of| \verb|R|.
(Generally types are written with capital letters in Mizar anyway.)
The symbol \verb|nf| is also a used for a function,
so we can not use it
for an attribute \verb|M| \verb|is| \verb|nf|.
Instead we used \verb|M| \verb|is_nf| as a predicate synonym for this attribute.
Also we can not use it for a type \verb|nf| \verb|of| \verb|R|.
Instead this became \verb|Nf| \verb|of| \verb|R|.
\section{A formal proof sketch from the Mizar mathematical library}\label{rewrite1}
In Section~\ref{full} we developed a Mizar formalization from a formal
proof sketch.
In this section we do the reverse.
Here we {\em extract\/} a formal proof sketch from the proof of Newman's lemma
that is in the MML:
\begin{flushleft}\footnotesize
\verb| reserve R for Relation;|\\
\verb| reserve M,M',M'',M''',M'''',N,N' for set;|\\
\verb| reserve p,q for RedSequence of R;|
\medskip
\verb|definition|\\
\verb| cluster strongly-normalizing locally-confluent -> confluent Relation;|\\
\verb| coherence|\\
\verb| proof|\\
\verb| let R;|\\
\verb| assume R is strongly-normalizing;|\\
\verb| assume for M,M',M'' st [M,M'] in R & [M,M''] in R|\\
\verb| holds M',M'' are_convergent_wrt R;|\\
\verb| given N,N' such that|\\
\verb| N,N' are_divergent_wrt R & not N,N' are_convergent_wrt R;|\\
\verb| defpred is_confluent[set] means|\\
\verb| for M',M'' st R reduces $1,M' & R reduces $1,M''|\\
\verb| holds M',M'' are_convergent_wrt R;|\\
\verb| for M st for M' st [M,M'] in R & M <> M' holds is_confluent[M']|\\
\verb| holds is_confluent[M]|\\
\verb| proof|\\
\verb| let M;|\\
\verb| assume for M' st [M,M'] in R & M <> M' holds is_confluent[M'];|\\
\verb| let M',M'';|\\
\verb| assume R reduces M,M' & R reduces M,M'';|\\
\verb| consider p such that M = p.1 & M' = p.len p;|\\
\verb| consider q such that M = q.1 & M'' = q.len q;|\\
\verb| per cases;|\\
\verb| suppose len p = 1;|\\
\verb| thus M',M'' are_convergent_wrt R;|\\
\verb| suppose len q = 1;|\\
\verb| thus M',M'' are_convergent_wrt R;|\\
\verb| suppose len p <> 1 & len q <> 1;|\\
\verb| consider M''' such that R reduces p.2,M''' & R reduces q.2,M''';|\\
\verb| R reduces p.2,M';|\\
\verb| consider M'''' such that R reduces M',M'''' & R reduces M''',M'''';|\\
\verb| R reduces q.2,M'''' & R reduces q.2,M'';|\\
\verb| thus M',M'' are_convergent_wrt R;|\\
\verb| end;|\\
\verb| for M st M in field R holds is_confluent[M];|\\
\verb| thus thesis;|\\
\verb| end;|\\
\verb|end;|
\end{flushleft}
The formalization from which this has
been extracted occurs in article \verb|REWRITE1|.
It was written by
Grzegorz Bancerek.
We have renamed some variables (\verb|a|, \verb|b|,
\verb|c| $\to$ \verb|M|, \verb|M'| \verb|M''|, \verb|P| $\to$ \verb|is_confluent|) to
make this resemble the other formal proof sketch more.
The diagram that corresponds to the third `\verb|suppose|' in this
formal proof sketch is:
$$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] && \\
& p_2\ar@{->>}[dl]\ar@{->>}[dr] && q_2\ar@{->>}[dl]\ar@{->>}[dr] & \\
M'\ar@{->>}[dr] && M'''\ar@{->>}[dl] && M''\ar@{->>}[ddll] \\
& M''''\ar@{->>}[dr] & && \\
&&&& }
$$
This version of the
proof of Newman's lemma also uses Noetherian induction.
It proves that all terms are `confluent' under the assumption that
all one-step reducts are confluent already.
\section{Conclusion}
\subsection{Discussion}
The formal proof sketch from Section~\ref{sketch} is quite similar
to the original informal proof.
Here are some deviations:
\begin{itemize}
\item
The proof step which introduces the assumptions to the proof
(\verb|assume| \verb|that| \verb|R| \verb|is| \verb|SN| \verb|and|
\verb|R| \verb|is| \verb|WCR|)
and the step that states at the end that the conclusion holds (\verb|thus| \verb|thesis|)
have to be present in the formal proof sketch but are left implicit in
the informal proof.
\item
The original proof uses textual references like {\em this $R$-nf\/} and
{\em such $M$}.
In first order logic one has to quantify explicitly with the
property of the referred object to get the
same effect.
\item
The attribute \verb|nf_inhabited| that is not present in the
informal original is necessary to have
a Mizar type (which has to be non-empty)
corresponding to the notion {\em $R$-nf}.
\item
Some notation deviates from the original
to avoid conflicts with the conventions
of the Mizar mathematical library:
\verb|Term| \verb|of| \verb|R| instead of \verb|term| \verb|of| \verb|R|,
\verb|Nf| \verb|of| \verb|R| instead of \verb|nf| \verb|of| \verb|R|,
\verb|is_nf| instead of \verb|is| \verb|nf|.
\item
Mizar definitions can not be local to a proof.
Only the \verb|set|, \verb|deffunc| and \verb|defpred| constructions
are local.
These have a restricted syntax.
Therefore we had to write \verb|ambiguous[M]|, and could not
write \verb|M| \verb|is| \verb|ambiguous|.
\end{itemize}
We do not claim here that Mizar should be changed to accommodate
these differences.
We merely note them.
We do not think that the differences are that important.
(The exception might be the lack of empty types.)
\subsection{Future work}
As we stated in the introduction of this note,
every informal proof is a challenge to write the corresponding
formal proof sketch.
We would like to take on more of these challenges.
It would be nice to have an experimental proof assistant that
implements an automatic diagramming feature
as outlined in Section~\ref{diagrams}.
\paragraph{Acknowledgments.}
Thanks to Dan Synek for coining the term `formal proof sketch challenge'.
%\bibliographystyle{plain}
%\bibliography{frk}
\begin{thebibliography}{1}
\bibitem{bar:84}
H.~Barendregt.
\newblock {\em The Lambda Calculus: Its Syntax and Semantics}.
\newblock North Holland, 1984.
\bibitem{bar:etc:95}
J.~Barwise and J.~Etchemendy.
\newblock {\em Hyperproof}.
\newblock Number~42 in CSLI Lecture Notes. CSLI Publications, Stanford, 1995.
\bibitem{bar:etc:98}
Jon Barwise and John Etchemendy.
\newblock {Computers, visualization, and the nature of reasoning}.
\newblock In T.W. Bynum and James~H. Moor, editors, {\em {The Digital Phoenix:
How Computers are Changing Philosophy}}, pages 93--116. Blackwell, London,
1998.
\bibitem{gan:kou:nor:vo:93}
Emden~R. Gansner, Eleftherios Koutsofios, Stephen~C. North, and Kiem-Phong Vo.
\newblock {A Technique for Drawing Directed Graphs}.
\newblock {\em Software Engineering}, 19(3):214--230, 1993.
\bibitem{har:wri:60}
G.H. Hardy and E.M. Wright.
\newblock {\em An Introduction to the Theory of Numbers}.
\newblock Clarendon Press, Oxford, fourth edition, 1960.
\bibitem{new:42}
M.H.A. Newman.
\newblock {On theories with a combinatorial definiton of ``equivalence.''}.
\newblock {\em Ann.\ of Math.}, (2):223--243, 1942.
\bibitem{wie:02}
F.~Wiedijk.
\newblock {Formal proof sketches}.
\newblock \hfill\break URL:
\verb||, 2002.
\end{thebibliography}
\end{document}