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