% $Id: mmode.tex,v 1.72 2004/03/09 15:30:04 freek Exp $ \documentclass[runningheads]{llncs} \usepackage{alltt,url} \raggedbottom \def\key#1{\textbf{#1}} \def\qkey#1{`\key{#1}'} \def\notion#1{\emph{#1}} \def\punct#1{`\texttt{#1}'} \def\cut{\penalty100} \def\negspace{$\hspace{-1.64cm}$} % 1.63 is too little \def\${\char`\\} \begin{document} \title{MMode \\ A Mizar Mode for the proof assistant Coq} \titlerunning{A Mizar Mode for the proof assistant Coq} \author{Mariusz Giero\inst{2,1} \and Freek Wiedijk\inst{1}} \institute{Department of Computer Science, University of Nijmegen,\\ Toernooiveld 1, 6525 ED Nijmegen, The Netherlands \and Department of Logic, Informatics and Philosophy of Science,\\ University of Bia{\l}ystok, Plac Uniwersytecki 1, 15-420 Bia{\l}ystok, Poland} \maketitle \begin{abstract} We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics can be used with any interface of Coq, and they can be freely mixed with the normal Coq tactics. The system described in this report can be downloaded on the web at \url{}. \end{abstract} \section{Introduction} % first version: Freek \subsection{The goal: a declarative proof language for Coq} Computers have made it practical to encode non-trivial mathematics in such a way that the correctness of the proofs can be automatically verified. However, this kind of encoded proof -- the way the encoder works with it -- currently does not resemble the mathematics that we know from journals and textbooks. Instead it looks like source code in a programming language. The proof languages of the proof assistants (programs to verify the correctness of encoded mathematics) come in two flavors. On the one hand there are the \emph{procedural} proof languages. These are the languages of the systems based on the architecture of the LCF system \cite{gor:mil:wad:79}. Examples of procedural provers are Coq \cite{coq:02}, NuPRL \cite{con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86}, HOL \cite{gor:mel:93,har:00}, Isabelle \cite{nip:pau:wen:02} and PVS \cite{owr:rus:sha:92}. In such a system a proof generally works its way backward, from the end of the proof to the beginning, and consists of a sequence of \emph{tactics}, which are commands that transform a proof state. On the other hand there are the \emph{declarative} proof languages. In a declarative system a proof is a sequence of statements, and proceeds from the beginning of the proof to the end. The steps in such a proof generally are bridged by some kind of automation built into the system. The declarative provers differ according to how much automation the system offers. On the one hand there are the fully \emph{automated theorem provers} like ACL2 \cite{kau:man:moo:00} and Theorema \cite{buc:jeb:kri:mar:vas:97}. Here a mathematical development is a linear list of lemmas, and the system tries to prove each lemma from the previous ones. On the other hand there are systems like Automath \cite{ned:geu:vri:94} and Agda \cite{coq:00}. These have no automation at all, but support \emph{natural deduction} style declarative proof with a hierarchical block structure. In the middle of this spectrum there is Mizar \cite{muz:93,wie:99:1}. Here a proof has a natural deduction style block structure, but the steps in the proof are also inferred from earlier ones using automation. The notions of procedural and declarative prover are not very sharp.\footnote{ Once again, the differences are: (a) in a procedural prover proofs generally run backward from the goal to the assumptions, while in a declarative prover they run mostly forward from the assumptions to the goal, and (b) in a procedural prover the proof scripts generally do not contain the statements that occur in the proof states, while in a declarative prover they do. } Maybe the terms do not mean much more than `the proofs look similar to Coq and HOL proof scripts' and `the proofs look like Mizar proofs'. If one thinks in terms of natural deduction proofs, the difference is largely the amount of `cuts' in proofs for the system: in a procedural prover a proof generally contains at most a few cuts, while in a declarative prover proofs contain a cut for almost every proof step. Also, the adjectives `procedural' and `declarative' really apply to the proof \emph{language} used to write proofs for the system. Maybe we should not speak about procedural/declarative \emph{provers}, but just of procedural/declarative \emph{proofs}. It is generally agreed that a declarative proof is more similar to the informal mathematical proofs from journals and textbooks than a tactics proof for a procedural system. For this reason some systems have put a declarative proof language on top of their procedural base. Generally this declarative proof language resembles the language of the Mizar system. The first to experiment with such a \emph{Mizar mode} was John Harrison, who built one on top of his HOL Light system \cite{har:00}. The main procedural system for which a Mizar-like proof language has become the accepted way of writing proofs is Isabelle, for which Markus Wenzel developed the Isar proof language \cite{wen:99}. We think that the Coq system should follow the example of Isabelle. This report describes a prototype declarative proof language for the Coq system. One goal for this language is that it should be closely integrated with the `old style' Coq proof language. In particular all the automation of the Coq system should be available in the language in a natural way. Another goal is that it should be easy for people to experiment with our language. Originally we called our prototype language `Mizar mode', but then Henk Barendregt proposed the name `mathematical mode', to stress the fact that the language should resemble the look of informal mathematics. Eventually both names were abbreviated to `MMode' which is the current name of our system. (A third reading of MMode is `Mariusz' mode'.) \medskip \noindent Note that our system can \emph{not} be used to automatically import Mizar proofs into Coq. We only imitated the \emph{proof language} of Mizar for Coq, the logical foundations beneath the two systems still are completely different. \subsection{Approach} We decided to implement the MMode language in the spirit of Mizar Light \cite{wie:01}. This is another experimental Mizar mode for the HOL Light system. The main difference with the Mizar mode by John Harrison is that there is no separate parser. Instead the system just consists of a collection of `Mizar tactics'. These tactics can be freely interleaved with the already existing tactics of the system. If one just uses these Mizar tactics, the proof closely resembles a declarative proof in the Mizar language. We had two models for the MMode language. On the one hand there was the Mizar language. The Mizar language has a large grammar, but the \emph{proof fragment} (the part of the grammar that is directly related to proof steps, so what one gets if one leaves out the grammar rules that are related to other things like term/formula syntax or the type system) actually is rather small. On the other hand there were Henk Barendregt's ideas about what a declarative language should look like \cite{bar:02}. Since the Mizar language is much further developed than Henk's ideas, we decided to start by implementing the proof fragment of the Mizar language. Later we extended this to get closer to Henk's ideas as well (this will be described in Section \ref{synon}). The part of Mizar that we took as a model for the MMode language is given by the following context free grammar\footnote{ In this grammar we have used the following customary abbreviations: [\notion{notion}] means zero or one occurrences of \notion{notion}, \{\notion{notion}\} means zero or more repetitions of \notion{notion}, and (\notion{notion}$_1$$\;|\;$\notion{notion}$_2$) means a choice between \notion{notion}$_1$ and \notion{notion}$_2$. }: \label{mizgrammar} \begin{quote} \notion{typing} := \notion{var} \{ \punct{,} \notion{var} \} [ ( \qkey{be} $|$ \qkey{being} ) \notion{type} ] \\ \notion{typings} := \notion{typing} \{ \punct{,} \notion{typing} \} \end{quote} \begin{quote} \notion{proposition} := [ \notion{label} \punct{:} ] ( \notion{formula} $|$ \qkey{thesis} ) \\ \notion{propositions} := \notion{proposition} \{ \qkey{and} \notion{proposition} \} \end{quote} \begin{quote} \notion{simple-justification} := [ \qkey{by} \notion{label} \{ \punct{,} \notion{label} \} ] \\ \notion{proof} := \qkey{proof} \{ \notion{step} \} [ \notion{cases} ] \qkey{end} \\ \notion{justification} := \notion{simple-justification} $|$ \notion{proof} \end{quote} \begin{quote} \notion{statement} := \\ \strut\quad \notion{propositions} \notion{justification} \\ \strut\rlap{$|$}\quad [ \notion{label} \punct{:} ] \notion{term} \punct{=} \notion{term} \notion{justification} \{ \punct{.=} \notion{term} \notion{justification} \} \end{quote} \begin{quote} \notion{step} := \\ \strut\quad \qkey{let} \notion{typings} \punct{;} \\ \strut\rlap{$|$}\quad \qkey{assume} \notion{propositions} \punct{;} \\ \strut\rlap{$|$}\quad [ \qkey{then} ] \notion{statement} \punct{;} \\ \strut\rlap{$|$}\quad ( \qkey{thus} $|$ \qkey{hence} ) \notion{statement} \punct{;} \\ \strut\rlap{$|$}\quad [ \qkey{then} ] \qkey{consider} \notion{typings} \qkey{such} \qkey{that} \\ \strut\quad\quad \notion{propositions} \notion{justification} \punct{;} \\ \strut\rlap{$|$}\quad \qkey{take} \notion{term} ( \punct{,} \notion{term} ) \punct{;} \\ \strut\rlap{$|$}\quad \qkey{set} \notion{var} \punct{=} \notion{term} \punct{;} \end{quote} \begin{quote} \notion{cases} := \\ \strut\quad \qkey{per} \qkey{cases} \notion{justification} \punct{;} \\ \strut\quad \{ \qkey{suppose} \notion{propositions} \punct{;} \{ \notion{step} \} \} \end{quote} \noindent For an explanation of the meanings of the various constructions in this grammar, see \cite{wie:99:1}. This grammar is almost the full proof fragment of Mizar. However, there are a few differences; \begin{itemize} \item This grammar is more orthogonal than the real Mizar syntax. For instance in this grammar a \key{proof} can be used everywhere where a \key{by} can be used. In the real Mizar various steps (like \key{consider} and \key{per cases}) can only be proved with a \key{by} justification. Also in this grammar a \key{then} can be used at any point, while in the real Mizar a \key{then} is forbidden after a \key{consider} step. %For these reasons this grammar is somewhat more expressive than the real %Mizar proof language. \item In this grammar some abbreviated steps from the real Mizar have been omitted. For instance there is no \key{given} (a combination of \key{assume} and \key{consider}) and there is no \key{let} \key{\dots} \key{such that} (a combination of \key{let} and \key{assume}). These abbreviations can be trivially expanded, so their omission does not restrict the expressivity of the language. \item The Mizar steps related to the Mizar type system like \key{reconsider} have been omitted. They make no sense in a system like Coq in which types are unique. \item A few other Mizar constructions have not been included either. For instance \key{deffunc} and \key{defpred} are not in this grammar. (In a higher order system like Coq these are special cases of \key{set}.) The \key{case} variation of the \key{suppose} step in a \key{per cases} construction has also been omitted for simplicity. \end{itemize} \noindent All these differences are minor and therefore this language fragment should \emph{not} be interpreted as being less powerful than the full proof language of the Mizar system. We wanted the threshold for experimenting with the MMode to be as low as possible. For this reason we took the following design decisions: \begin{enumerate} \item \emph{We did not want a separate parser for our language. All syntax was implemented through Coq's \emph{\texttt{Grammar}} rules.} This choice makes it possible to use the MMode system in any Coq interface that accepts user-defined tactics with a syntax given by \texttt{Grammar} rules. By this choice we hoped to minimize the need for users to switch to a different interface to be able to use our system. In particular the MMode language works fine with the Proof General interface of Coq. This choice caused some complications. One was that the keywords \key{Let} and \key{Show} already were used by the original Coq language, and could not be used by MMode. Therefore MMode uses the keywords \key{Let\_} and \key{Show\_}, with an underscore at the end. Another problem was that we wanted the justification of a step to be an arbitrary Coq tactic. However in Coq 7.4 tactics cannot have tactics as an argument. Hugo Herbelin kindly showed us how to patch Coq 7.4 to allow this. However, this means that one needs to patch Coq to be able to try our system. We discuss this in more detail in Section \ref{system}. \medskip \item \emph{We did not want tactics implemented on the ML level. All tactics in the MMode language were implemented using David Delahaye's ${\cal L}_{\rm tac}$ language.} In the C-CoRN project \cite{cru:03} we had one tactic (called \texttt{Rational}) that was implemented in ML. For this reason to be able to use the C-CoRN library with the native version of Coq, people had to build a C-CoRN specific Coq image. This should be trivial, but in practice this often was causing problems. For the MMode language we wanted to avoid this complication. This choice slowed us down quite a bit. Often ${\cal L}_{\rm tac}$ behaved erratically and even if it behaved properly the error messages were not very informative. \end{enumerate} \noindent These two design choices might be changed for a later version of the system. For the moment we consider MMode to be a prototype that shows what is possible. For this reason we wanted it to be as easy as possible for people to try our system. If people happen to like it, a later version might depart more from the standard Coq environment. We did not develop the MMode system systematically. Instead we took some existing Coq and Mizar proofs, and tried to fit them into a Coq version of the Mizar fragment that we showed earlier. We just implemented the MMode tactics that were needed to make these example proofs work. The example proofs are shown in Section \ref{examples} and fall into three categories: \begin{description} \item[Translations of Coq proofs that just use the basic Coq tactics,] for examples that are easy to understand. Among these were proofs by Henk Barendregt from his development of the Fundamental Theorem of Arithmetic; \item[Translations of Coq proofs that use a complicated library.] In our case this was the C-CoRN library. We included this kind of proof to show that our approach also works with non-trivial tactics; \item[Translations of Mizar proofs,] to show the similarity of the MMode version to the original Mizar version. \end{description} \subsection{Related Work} Our goal is to extend Coq to a system that can be used in a declarative way. Most proof assistants are procedural: only a few systems are declarative. The main declarative system is Mizar. Other declarative systems in the style of Mizar are Don Syme's DECLARE \cite{sym:99} and Vincent Zammit's SPL \cite{zam:99}. Mizar modes for procedural systems are not common either. The Mizar modes for HOL are currently just experiments. However, the Isar language for Isabelle \cite{wen:99} has become a success. It is now the official input language for the Isabelle system. Our MMode language differs in an important respect from Isar (for a comparison of Mizar and Isar, see \cite{wen:wie:02}). In Isar the declarative and procedural parts of the system both have a proof state of their own, called the static and dynamic proof states. However, in MMode we follow the approach from the Mizar modes for HOL, where the proof state that is used by the normal tactics of the system is also used for the declarative proofs. We think that this is more elegant and simple. \subsection{Contribution} We have created a system for writing declarative proofs with Coq. We have reimplemented most features of the proof language of the Mizar system. The system is not a separate layer on top of Coq, but is written in such a way that proofs can freely mix old style Coq tactics and declarative proof steps. Also, the system can be used in any reasonable Coq interface. \subsection{Outline} This report is organized as follows. In Section \ref{system} we describe the organization and installation of our system. In Section \ref{language} we present the MMode proof language. In Section \ref{by} we describe the inference automation (the \key{by} tactic) that we developed for the MMode system. In Section \ref{implem} we give a detailed account of each of the MMode tactics. In Section \ref{examples} we discuss the example proofs that we used to develop the MMode system. Finally, in Section \ref{synon} we describe the extension to the MMode syntax for Henk Barendregt's proofs. In this report we assume familiarity with the Coq system. Basic knowledge of the Mizar proof language also helps. For an introduction to Mizar-style proof read the introduction to the MMode language in Section~\ref{mmodeintro} on page~\pageref{mmodeintro}. \section{The MMode system} % first version: Freek \label{system} We now describe the organization of the MMode distribution. If you do not want to experiment with MMode but just want to read about it, you can skip this section. The MMode system has four variants: \begin{description} \item[MMode.] This is the basic version of the system, which does not need anything besides the standard Coq library. To use it one needs to add one line: \begin{center} \verb|Require MMode.| \end{center} at the beginning of the Coq file. \item[CMode.] This is the version of the system to be used with the C-CoRN library from Nijmegen \cite{cru:03}. It knows about the C-CoRN equality \verb|[=]| and about the C-CoRN equational reasoning tactics \verb|Algebra| and \verb|Rational|. Also, it knows about the C-CoRN type for computational propositions which is called \verb|CProp|. To use the CMode variant of MMode, one adds the line: \begin{center} \verb|Require CMode.| \end{center} at the beginning of one's Coq file. \item[HMode.] This is a version of the system to be used with Henk Barendregt's files in which he proved the Fundamental Theorem of Arithmetic. The reason that this needs a special version of MMode, is that Henk does not use the normal Leibniz equality of Coq, but defines his own equality. Also he has his own types for propositions called \verb|prop| and \verb|cprop|. To use the HMode variant of MMode, one adds the line: \begin{center} \verb|Require HMode.| \end{center} at the beginning of one's Coq file. \item[HMode with synonyms.] The HMode version of MMode has a variant where many synonyms have been added for the MMode steps, to make proofs look more like normal mathematical text. See Section~\ref{synon} for a description of these synonyms. To use the HMode variant of MMode with the synonyms, one adds the line: \begin{center} \verb|Require HMode_synon.| \end{center} at the beginning of one's Coq file. \end{description} \noindent Normally MMode will stop processing a proof at the first error. This is the normal behavior of Coq, but it differs from the behavior of Mizar which uses error recovery to continue checking after errors. If one uses the \key{Sketch} option of MMode, it will behave like Mizar in this respect: in that case justification errors will not be fatal. See Section~\ref{missing} for a description of this feature. To use the Sketch option of MMode, one adds the line: \begin{center} \verb|Require Sketch.| \end{center} at the beginning of one's Coq file. One does not need to have the MMode files next to the Coq files that make use of them. If the MMode files have been properly installed Coq will be able to find the relevant \verb|.vo| files automatically in the Coq library directory. If the MMode files have not been installed, but are used from their source directory, one needs to add the flag \begin{center} \verb|-R |\notion{$\langle$directory that holds the \emph{MMode} \emph{\texttt{.vo}} files$\rangle$}\verb| Coq.mmode| \end{center} to the Coq commands. To install the MMode system, one needs to perform the following six steps: \begin{enumerate} \item Get the MMode distribution file from \begin{center} \url{http://www.cs.kun.nl/~freek/mmode/mmode.tar.gz} \end{center} \item Unpack the \verb|mmode.tar.gz| file to a directory \verb|mmode|: \begin{flushleft} \verb/zcat mmode.tar.gz | tar xf -/ \\ \verb|cd mmode| \end{flushleft} \item Patch the Coq source and recompile Coq (see below for an explanation of why this is necessary): \begin{flushleft} \verb|patch -d |\notion{$\langle$your Coq source directory$\rangle$}\verb|/tactics < mmode.patch| \\ \verb|cd |\notion{$\langle$your Coq source directory$\rangle$} \\ \verb|make world| \\ \verb|make install| \\ \verb|cd -| \end{flushleft} \item The next steps has three variants. Choose one of them: \begin{enumerate} \item Edit the \verb|Makefile| according to whether or not you have C-CoRN (follow the instructions at the start of the file). \item If you have C-CoRN but do not want to edit the \verb|Makefile|, create a link called \verb|algebra| in the \verb|mmode| directory that points to your C-CoRN directory: \medskip \begin{flushleft} \verb|ln -s |\notion{$\langle$your \emph{C-CoRN} directory$\rangle$}\verb| algebra| \end{flushleft} \medskip \item If you do not have C-CoRN, but want to try it, unpack the file \url{algebra.tar.gz} and compile it: \medskip \begin{flushleft} \verb/zcat algebra.tar.gz | tar xf -/ \\ \verb|cd algebra| \\ \verb|make| \\ \verb|cd ..| \end{flushleft} \medskip The file \verb|algebra.tar.gz| contains the part of C-CoRN that is used by the C-CoRN examples. \end{enumerate} In case you choose 4(a) or 4(b), be aware that you need to have a version of C-CoRN that works with Coq 7.4. (The most recent version of C-CoRN does not work with Coq 7.4 anymore.) \item Type: \begin{flushleft} \verb|make| \end{flushleft} This will compile the MMode files and the examples. \item Type: \begin{flushleft} \verb|make install| \end{flushleft} This will copy the MMode \verb|.vo| files to the library directory of Coq. (It will use the command \verb|coqc| \verb|-where| to find out where this is.) It also will copy Henk's files that are needed for the HMode. \end{enumerate} \noindent As step 3 of the installation, Coq 7.4 needs to be `patched'. This is needed to be able to process the \verb|Grammar| rules in the MMode files. Two lines in the Coq source file \verb|tacinterp.ml| will be changed. This will allow the \verb|Grammar| rules to define syntax for tactics that take tactics as arguments.\footnote{ To understand why MMode has tactics that take tactics as arguments, consider the MMode step: \begin{quote} \texttt{Have (3)=(plus (3) (0)) [by plus\char`\_n\char`\_O].} \end{quote} \noindent The subgoal \texttt{(3)=(plus} \texttt{(3)} \texttt{(0))} will be solved by the tactic `\texttt{by} \texttt{plus\char`\_n\char`\_O}'. Both the full `\texttt{Have} \texttt{\dots}' step itself, as well as the `\texttt{by} \texttt{plus\char`\_n\char`\_O}' argument to the \texttt{Have} tactic are Coq tactics. This also means that the same step could have used a different Coq tactic for its justification. For instance it could have been: \begin{quote} \texttt{Have (3)=(plus (3) (0)) [Omega].} \end{quote} } \emph{The only change will be that slightly more \emph{\texttt{Grammar}} rules will be accepted by Coq: anything that worked with Coq 7.4 will keep working in exactly the same way as it worked before.} So one can patch Coq without any fear for compatibility problems. The MMode distribution contains the following files: \begin{center} \begin{tabular}{lp{22em}} \verb|mmode.patch| & patch to allow Coq 7.4 to process the MMode files \\ \noalign{\medskip} \verb|src/| & source files of the MMode tactics \\ \verb|other/henk/| & Coq files needed for the HMode \\ \verb|algebra.tar.gz| & relevant part of the C-CoRN files for the CMode \\ \noalign{\medskip} \verb|examples/| & examples of MMode proofs \\ \noalign{\medskip} \verb|other/originals/| & the original versions from which the examples have been derived \\ \verb|other/expanded_by/|$\quad$ & the examples where the \key{by} justifications have been expanded to more common Coq tactics \\ \noalign{\medskip} \verb|README| & an ASCII file similar to this section \\ \verb|paper/| & {\LaTeX} source of this report \end{tabular} \end{center} \noindent Apart from files for the four variants of MMode, the \verb|src| directory also contains a file called `\verb|BMode.v|' (the `basic' part of MMode). This is the common part of MMode, CMode and HMode. It is not meant to be used by itself. \section{The MMode proof language} % first version: Freek \label{language} \subsection{MMode syntax} In this section we will describe the proof language of the MMode system. The description will be from the point of view of a MMode user. For a more detailed description, which also discusses the implementation of the MMode tactics, see the next sections. The MMode proof language is given by the following grammar. The MMode tactics do \emph{not} implement this language completely. For a list of the actual steps that one can use in the current MMode system, see the Appendix on page \pageref{appendix}. However, in this section we will describe the MMode language as if it were fully implemented: \label{mmodegrammar} \begin{flushleft} \notion{typing} := \notion{var} \{ \punct{,} \notion{var} \} \qkey{be} \notion{type} \\ \notion{typings} := \notion{typing} \{ ( \punct{,} $|$ \qkey{and} ) \notion{typing} \} \end{flushleft} \begin{flushleft} \notion{bound-formula} := \\ \strut\quad \punct{[} \notion{var} \punct{:} \notion{type} \punct{]} \notion{formula} \\ \strut\rlap{$|$}\quad \punct{(} \notion{bound-formula} \punct{)} \end{flushleft} \begin{flushleft} \notion{proposition} := \notion{formula} [ \punct{(} \notion{label} \punct{)} ] \\ \notion{propositions} := \notion{proposition} \{ \qkey{and} \notion{proposition} \} \end{flushleft} \begin{flushleft} \notion{bound-proposition} := \notion{bound-formula} [ \punct{(} \notion{label} \punct{)} ] \\ \notion{bound-propositions} := \notion{bound-proposition} \{ \qkey{and} \notion{bound-proposition} \} \end{flushleft} \begin{flushleft} \notion{justification} := \\ \strut\quad [ \punct{[} \qkey{by} \notion{ref} \{ \punct{,} \notion{ref} \} [ \qkey{with} \notion{Coq-tactic} ] \punct{]} ] \\ \strut\rlap{$|$}\quad \phantom{[} \punct{[} \notion{Coq-tactic} \punct{]} \\ \end{flushleft} \begin{flushleft} \notion{step} := \\ \strut\quad \qkey{Let\_} \notion{typings} \punct{.} \\ \strut\rlap{$|$}\quad \qkey{Assume} \notion{propositions} \punct{.} \\ \strut\rlap{$|$}\quad ( \qkey{Have} $|$ \qkey{Then} ) \notion{proposition} \notion{justification} \punct{.} \\ \strut\quad \{ [ \qkey{Thus} ] ( \punct{\char`\_=} $|$ \punct{\char`\_[=]} $|$ \punct{=\char`\_} $|$ \punct{[=]\char`\_} ) \notion{term} \notion{justification} \punct{.} \} \\ \strut\rlap{$|$}\quad \qkey{Claim} \notion{proposition} \punct{.} \\ \strut\quad \quad \notion{proof} \\ \strut\quad \qkey{End\_claim} \punct{.} \\ \strut\rlap{$|$}\quad ( \qkey{Thus} $|$ \qkey{Hence} ) ( \notion{formula} $|$ \qkey{thesis} ) \notion{justification} \punct{.} \\ \strut\rlap{$|$}\quad ( \qkey{Consider} $|$ \qkey{Then} \qkey{consider} ) \notion{var} \qkey{such} \qkey{that} \notion{bound-propositions} \\ \strut\quad \quad \notion{justification} \punct{.} \\ \strut\rlap{$|$}\quad \qkey{Take} \notion{term} \qkey{and} \qkey{prove} \notion{formula} \{ \qkey{and} \notion{formula} \} \punct{.} \\ \strut\rlap{$|$}\quad \qkey{Show\_} \notion{formula} \punct{.} \\ \strut\rlap{$|$}\quad \notion{Coq-tactic} \punct{.} \end{flushleft} \begin{flushleft} \notion{cases} := \\ \strut\quad \qkey{First} \qkey{case} \notion{proposition} \punct{.} \notion{proof} \{ \qkey{Next} \qkey{case} \notion{proposition} \punct{.} \notion{proof} \} \\ \strut\quad \qkey{End\_cases} \notion{justification} \punct{.} \end{flushleft} \begin{flushleft} \notion{proof} := \{ \notion{step} \} [ \notion{cases} ] \end{flushleft} \noindent In this grammar the notions \notion{var}, \notion{term}, \notion{type}, \notion{formula}, \notion{label}, \notion{ref} and \notion{Coq-tactic} are taken to be primitive. These notions are inherited from Coq. The notions \notion{var} and \notion{label} are Coq identifiers, the notions \notion{term}, \notion{type}, \notion{formula} and \notion{ref} are Coq terms, and the notion \notion{Coq-tactic} is for Coq tactics. In comparison to the Mizar proof grammar on page \pageref{mizgrammar}, the most important differences in this grammar are: \begin{itemize} \item The MMode grammar has a special step called \key{Show\_}, to state the current goal. This does not do anything (maybe this is the reason that Mizar does not have an equivalent step), it just documents the proof obligation in the proof. \item In the MMode grammar, justifications are only `\key{by}' justifications and not multi-step subproofs. To have subproofs one uses a special tactic called \key{Claim}. In contrast to this, in the grammar on page \pageref{mizgrammar} a subproof can be used in exactly the same places as where a \key{by} justification can be used. (The real Mizar is in between these two extremes: in Mizar subproofs are not allowed in \emph{all} justifications, but there is not a special keyword for them either.) \item In MMode one can have arbitrary Coq proof terms after the \key{by}. In Mizar one can only put labels there. \item There is no step in MMode that corresponds to Mizar's abbreviation step called `\key{set}'. In Coq there already exists the tactic \key{LetTac} for this. \item There are some other small differences between Mizar and MMode. In Mizar the keyword \key{thesis} can be used anywhere to represent the current goal, while in MMode it only can be used after \key{Thus} or \key{Hence}. In Mizar the formula after a \key{Thus} or \key{Hence} can have a label, in MMode it can not. In Mizar after a \key{take} step there is no statement of what the thesis/goal has become, in MMode there is (so the MMode `\key{Take}' is a combination of the Mizar \key{take} and the MMode \key{Show\_}). In Mizar the justification in a proof by cases (`\key{per} \key{cases}') is at the start of the cases, in MMode it is at end (for only then it is known what the cases are). \end{itemize} \noindent All these differences are minor. The MMode grammar is very close to the Mizar proof grammar from page~\pageref{mizgrammar}, and it therefore is justified to call MMode a `Mizar mode'. Both MMode steps and MMode justifications can be arbitrary Coq tactics. Therefore it is possible to freely mix `traditional style' Coq tactics and MMode steps. For instance one might decide to do a proof by induction by just running Coq's \key{Induction} tactic, and then handle the cases that this tactic generates using MMode. \subsection{A brief introduction to MMode proofs} \label{mmodeintro} We now will go through a Coq session, to explain the basics of MMode proofs. We start by typing: \begin{alltt} Require Le. Check le_trans_S. \end{alltt} \noindent Coq will answer: \begin{alltt} le_trans_S : (n,m:nat)(le (S n) m)->(le n m) \end{alltt} \noindent Apparently the Coq lemma \texttt{le\char`\_trans\char`\_S} states that for all natural numbers $n$ and $m$ holds that if $n + 1 \le m$ then also $n \le m$. We now will prove the equivalent statement for \texttt{lt} in various ways. This is of course completely trivial, but it will show the relation between the Coq way of doing proofs and MMode style proofs. First, here is a low level Coq proof: \begin{alltt} Lemma lt_trans_S_coq_simple : (n,m:nat)(lt (S n) m)->(lt n m). Proof. Intros n m A1. Change (le (S n) m). Apply le_trans_S. Exact A1. Qed. \end{alltt} \noindent Of course the proof can be done automatically as well: \begin{alltt} Lemma lt_trans_S_coq_auto : (n,m:nat)(lt (S n) m)->(lt n m). Proof. Auto with arith. Qed. \end{alltt} (In the \texttt{Arith} library of Coq all lemmas like this are proved in this style.) We will now prove the same statement using MMode. Again we start in a very basic way: \begin{alltt} Lemma lt_trans_S_mmode_simple : (n,m:nat)(lt (S n) m)->(lt n m). Proof. Let_ n,m be nat. Assume (lt (S n) m) (A1). Have (le (S (S n)) m) (A2) [by A1]. Have (le (S n) m) (A3) [by A2,le_trans_S]. Thus (lt n m) [by A3]. Qed. \end{alltt} Before we go through this line by line, note that this proof uses four kinds of steps: \key{Let\_}, \key{Assume}, \key{Have} and \key{Thus}. These steps correspond in Coq to the tactics \key{Intro}, \key{Intro}, \key{Cut}/\key{Assert} and \key{Exact}. (Of course there are more MMode tactics than just these.\footnote{ Also \key{Thus} does more than \key{Exact}, because it can split conjunctions: it corresponds to the natural deduction rule of $\land$-introduction. } Below we will list them, and relate them to Coq tactics, and also to the natural deduction rules of first order logic.) Note that there is no step that corresponds to \key{Apply}. The role of \key{Apply} is taken by the \key{by} justification. Now let us look at this example proof in detail. Each line contains a \notion{formula} that it will introduce to the context, it also contains a \notion{label} between round brackets, and most of the lines contain a \notion{justification} between square brackets. We can execute the proof step by step. After all, each step is just a completely ordinary Coq tactic: \smallskip \begin{alltt}\footnotesize ============================ (n,m:nat)(lt (S n) m)->(lt n m) lt_trans_S_mmode_simple < Let_ n,m be nat. 1 subgoal n : nat m : nat ============================ (lt (S n) m)->(lt n m) lt_trans_S_mmode_simple < Assume (lt (S n) m) (A1). 1 subgoal n : nat m : nat A1 : (lt (S n) m) ============================ (lt n m) lt_trans_S_mmode_simple < Have (le (S (S n)) m) (A2) [by A1]. 1 subgoal n : nat m : nat A1 : (lt (S n) m) A2 : (le (S (S n)) m) ============================ (lt n m) lt_trans_S_mmode_simple < Have (le (S n) m) (A3) [by A2,le_trans_S]. 1 subgoal n : nat m : nat A1 : (lt (S n) m) A2 : (le (S (S n)) m) A3 : (le (S n) m) ============================ (lt n m) lt_trans_S_mmode_simple < Thus (lt n m) [by A3]. Subtree proved! \end{alltt} \noindent This example session shows the relation between the formulas and labels in the MMode steps, and how these steps affect Coq's proof state. Most of the references in this proof are to the label of the previous proof step. This is so common in Mizar-like proofs, that there is a special abbreviation for this. If one writes \key{Then} instead of \key{Have} or \key{Hence} instead of \key{Thus}, there is an implicit reference to the previous proof step. Another abbreviation is that the statement in the final step can be abbreviated as \key{thesis}. Together this leads to a low level MMode proof of our example in a for Mizar more customary style: \begin{alltt} Lemma lt_trans_S_mmode_abbrev : (n,m:nat)(lt (S n) m)->(lt n m). Proof. Let_ n,m be nat. Assume (lt (S n) m). Then (le (S (S n)) m). Then (le (S n) m) [by le_trans_S]. Hence thesis. Qed. \end{alltt} \noindent So in MMode labels are only necessary when the reference is to a step that is not the previous one. In MMode the \key{by} tactic has a similar power to the \key{Auto} tactic of Coq. Therefore, we do not need to prove this statement in this low level manner, but instead can just write: \begin{alltt} Lemma lt_trans_S_mmode_by : (n,m:nat)(lt (S n) m)->(lt n m). Proof. Thus thesis [by le_trans_S]. Qed. \end{alltt} \noindent This completes our brief introduction to MMode proofs. \medskip \noindent For less trivial MMode proofs see the examples in Sections~\ref{examples} and~\ref{synon}. Realize that even in the example with synonyms starting on page~\pageref{synonexample} (which looks like a `presentation' of a proof) the text still can be executed one tactic at a time. For instance after the line: \begin{quote} \begin{alltt} Also ((x[x]pp)=n) [by A8 , times_com]. \end{alltt} \end{quote} the goal state of Coq will look like: \begin{alltt}\footnotesize P := [n:nat]O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set n : nat IH : (before n P) A4 : OQ (A1) [by \dots]. Have P (A2) [by \dots]. .............. Have Q [\underbar{by A1,A2}]. .............. \end{alltt} \end{quote} \noindent The six entries in this table marked `(\key{by})' are a lower bound on the power of the \key{by} tactic. The \key{by} of the Mizar system and the \key{by} of MMode satisfy this bound. Both of these \key{by} tactics have the property that they include these six natural deduction rules. \section{By} \label{by} The MMode language (and other declarative proof languages like Mizar and Isar) combines two aspects: \begin{itemize} \item natural deduction proofs in a block structured language; \item \emph{automation} of inferences for forward reasoning. \end{itemize} \noindent The set of tactics that are used for the first will be explained in detail in Section~\ref{implem}. In this section we will discuss the \key{by} tactic, which in the MMode system is the implementation of automated forward reasoning. Most steps in both the Mizar and the MMode systems generate a \emph{proof obligation} that has to be proved by a \emph{justification}. For instance the MMode step \begin{quote} \verb|Consider m such that [m:nat] n=(plus m (1)) [|\notion{tactic}\verb|].| \end{quote} has as proof obligation \begin{quote} \verb/(EX m:nat | n=(plus m (1)))/ \end{quote} This is the statement that \notion{tactic} should completely prove. In the Mizar system there is only one `tactic' that is used to prove justifications like this, which is called \key{by}.\footnote{ This is not completely true. Mizar proof steps sometimes use the \key{from} justification as well, which is a very weak second order prover. Here we will ignore this, and just talk about `\key{by}'. } This prover has the following three properties: \begin{enumerate} \item It is \emph{very fast}. Either it almost immediately succeeds in proving the proof obligation or it almost immediately fails. So in both cases it returns the answer in a very short time. On modern hardware Mizar can prove thousands of \key{by} justifications in seconds. \item It is \emph{complete}, in the sense that anything that can be proved in the logic of the underlying system can be proved using the combination of natural deduction steps and \key{by}. For Mizar this is easy to establish, cf.~the discussion in Section~\ref{natded}. The MMode \key{by} preferably also should be complete for the Coq logic. We conjecture that for the current implementation this is the case, but we do not have a proof of this yet. \item It is sufficiently \emph{powerful}, in the sense that the \key{by} prover can establish inferences that a human user considers to be trivial. The justifications that the Mizar \key{by} proves are in the Mizar literature called \emph{obvious} inferences. \end{enumerate} \noindent Note that there is a tension between property 1 and property 3. As MMode is a Mizar mode, we have been looking for a `natural' implementation of a \key{by} prover for the Coq system. We have gone through three approaches: \begin{itemize} \item Coq already has automated proof search tactics: \key{Auto}, \key{EAuto}, \key{Prolog}, \key{Intuition} and \key{Jp} (`JProver'). As a first approximation, it seems natural to just use one of those tactics as the Coq version of \key{by}. In particular \key{Intuition} seems the natural choice for a Coq version of `obviousness'. However, in practice this does not come close enough to the `completeness' and `powerful' requirements of \key{by}. Often a Coq proof will need tactics like \key{Induction} or \key{Inversion} to proceed naturally. This kind of reasoning will not be captured by one of the already automated search tactics of Coq. \medskip \item For a second attempt at a Coq \key{by} we reasoned as follows: Most Coq tactics can be run either with no arguments, or with a Coq term for an argument. Coq proofs mostly are a linear list of such zero- or one-argument tactic invocations. We want \key{by} to search for short proofs of this shape. This method generalizes the \key{Auto} tactic, which searches for short proofs that \emph{only} use the \key{Intro} and \key{Apply} tactics. Therefore we called our attempt \key{GAuto} (`Generalized Auto'). The \key{Auto} tactic tries to prove the goal by applying the \key{Apply} tactic to: \begin{enumerate} \item items from \emph{hints} databases; \item items from the context. \end{enumerate} The idea of \key{GAuto} was to modify this, by dropping the hints sets (so this makes the tactic weaker), but to use other tactics apart from \key{Apply} (this makes the tactic stronger). So apart from \key{Apply}, the \key{GAuto} tactic will recursively try to apply tactics like \key{Absurd}, \key{Rewrite} \texttt{->}, \key{Rewrite} \texttt{<-}, \key{Elim}, \key{Induction} and \key{Inversion} to variables from the context. Also \key{GAuto} will try tactics without arguments other than \key{Intro}, like \key{Split}, \key{Simpl} and \key{Red}. One often observes that when people start learning Coq they manage to do proofs without any real understanding, by just trying tactics until the goal is solved. This approach to Coq proof finding is what \key{GAuto} is automating. \medskip \noindent As an experiment we also put `normal' Coq tactic scripts as justifications in the MMode examples. These variant proofs can be found in the directory \url{other/expanded_by/} of the MMode distribution. For instance, the proof of \url{nat_factorizes} will work with the following justifications: \medskip \begin{quote} \begin{alltt}\footnotesize Simpl; Apply conj; [ Apply A1 | Apply trivial] Simpl; Rewrite -> times_com; Apply refl_equal Apply conj; [Apply A2 | Apply A3] Apply nat_HPD Red in A5; Elim A5; Intro; Intro B1; Exact B1 Exact _ Elim A4; Intro; Intro B2; Rewrite <- B2; Apply times_com Rewrite A9; Apply refl_equal Red in A5; Elim A5; Intro B3; Intro; Exact B3 Red in _; Elim _; Intro B4; Intro; Exact B4 EApply propprod_propfact; [Apply A7 | Apply A6 | Exact _] Rewrite A8; Simpl; Apply refl_equal Rewrite <- A9; Apply times_com Rewrite <- _ in A6; Exact A6 Elim not_lt_zero with O; Exact _ Apply neq_zero_imp_gt_zero; Exact _ Apply A10; Elim A11; Intro B5; Intro; Exact B5 Elim A11; Intro; Intro B6; Exact B6 Apply A12; Exact _ Elim A5; Intro B7; Intro; Exact B7 Split; [Exact _ | Elim A13; Intro B8; Intro; Exact B8] Elim A4; Intro; Intro B9; Apply eq_sym; Exact B9 Elim A13; Intro; Intro B10; Rewrite B10; Simpl; Apply times_com Split; [Exact A14 | Exact A15] Apply prime_dec Apply cv_ind; Exact A16 \end{alltt} \end{quote} \medskip (In these proof scripts `\texttt{\char`\_}' is the label used by MMode for an unlabeled formula that was put in the context by the previous proof step.) The same justifications using the \key{by} tactic are: \medskip \begin{quote} \begin{alltt}\footnotesize by A1 by refl_equal, times_com by A2, A3 by nat_HPD by A5 by _ by times_com, A4 by A9 by A5 by _ by _, A7, A6, propprod_propfact by A8 by A9, times_com by _, A6 by _, not_lt_zero by _, neq_zero_imp_gt_zero by A11, A10 by A11 by _, A12 by A5 by _, A13 by A4, eq_sym by A13, times_com by A14, A15 by prime_dec by A16, cv_ind \end{alltt} \end{quote} \medskip (Of course in MMode proofs the label `\texttt{\char`\_}' is not actually written. Instead the \key{Then} keyword is used for this.) \medskip \noindent Coq's \key{Auto} tactic tries to use everything that is in the context. However, the \key{by} tactic only uses its arguments.\footnote{ There are two reasons for this: (1) efficiency and (2) to make the `flow of reasoning' in the proof apparent. It might be interesting to experiment with a version of MMode where \key{by} is allowed to use everything from the context (instead of just its arguments). That way the proofs will probably check much slower, but also much less references to `local' labels will be needed. } To accomplish this, \key{by} first replaces the context with a context that just contains variables corresponding to the arguments. It does this by calling \key{Generalize} for all its arguments, then clearing the context, and finally putting them in the context again by calling \texttt{Try} \texttt{Intros}. For instance, in the example proof from Section~\ref{mmodeintro}, when justifying the step: \begin{flushleft} \begin{alltt} Have (le (S n) m) (A3) [by A2,le_trans_S]. \end{alltt} \end{flushleft} \noindent at the start of the justification the context looks like \begin{flushleft} \begin{alltt}\footnotesize n : nat m : nat A1 : (lt (S n) m) A2 : (le (S (S n)) m) ============================ (le (S n) m) \end{alltt} \end{flushleft} \noindent After \begin{flushleft} \begin{alltt} Generalize A2; Generalize le_trans_S \end{alltt} \end{flushleft} \noindent the goal becomes \begin{flushleft} \begin{alltt}\footnotesize n : nat m : nat A1 : (lt (S n) m) A2 : (le (S (S n)) m) ============================ ((n,m:nat)(le (S n) m)->(le n m))->(le (S (S n)) m)->(le (S n) m) \end{alltt} \end{flushleft} \noindent Then the context is cleared, so the goal becomes \begin{flushleft} \begin{alltt}\footnotesize n : nat m : nat ============================ ((n,m:nat)(le (S n) m)->(le n m))->(le (S (S n)) m)->(le (S n) m) \end{alltt} \end{flushleft} \noindent and then after \begin{flushleft} \begin{alltt} Try Intros. \end{alltt} \end{flushleft} \noindent the goal becomes \begin{flushleft} \begin{alltt}\footnotesize n : nat m : nat H : (n,m:nat)(le (S n) m)->(le n m) A2 : (le (S (S n)) m) ============================ (le (S n) m) \end{alltt} \end{flushleft} \noindent Only then \key{GAuto} is run. \medskip \item The actual implementation of \key{by} that is currently in MMode is \emph{in between} the two previous approaches. Basically it implements the previous method, but it does not recursively look for arbitrary proof scripts up to a certain length. Instead it only tries all the relevant Coq tactics for \emph{one} step. Before and after this one step it uses the automation of Coq. The two automated tactics that it uses there are \begin{flushleft} \begin{alltt} Intuition EAuto Prolog [] 9 \end{alltt} \end{flushleft} \noindent The tactics that it tries between these calls to \key{Intuition} or \key{Prolog} are \def\notionterm{\textrm{\notion{term}}} \begin{flushleft} \begin{alltt} Elim \notionterm Rewrite -> \notionterm Rewrite <- \notionterm Absurd \notionterm Red in \notionterm Rewrite \notionterm in \notionterm Rewrite <- \notionterm in \notionterm \end{alltt} \end{flushleft} \noindent (This list works for the example proofs. Possibly it needs to be extended when more experience with MMode is gained.) Apart from the tactics in this list, the \key{by} tactic can be given an extra tactic after the keyword \key{with}. It will then try this tactic as well. \end{itemize} \section{Implementation of the tactics} % first version: Mariusz \label{implem} We will now describe the `natural deduction' MMode tactics. For each tactic we will describe its effect on the proof state, when it is appropriate to use it, and how it has been implemented. \subsection{Let\_/Assume} \newlength{\oldparindent} \setlength{\oldparindent}{\parindent} \setlength{\parindent}{0cm} \label{mlet} \qkey{Let\_} \notion{var} \{ \punct{,} \notion{var} \} \qkey{be} \notion{type} \{ ( \punct{,} $|$ \qkey{and} ) \notion{var} \{ \punct{,} \notion{var} \} \qkey{be} \notion{type} \} \punct{.} \qkey{Assume} \notion{formula} [ \punct{(} \notion{label} \punct{)} ] \punct{.} \medskip The \key{Let\_} tactic applies to a goal which is a dependent product `\texttt{(x:U)T}'. \begin{verbatim} Let_ x be U \end{verbatim} puts `\texttt{x:U}' in the local context and the new subgoal becomes `\texttt{T}'. The \key{Assume} tactic applies to a goal which is a non-dependent product\hfill\break\mbox{`\texttt{T1 -> T2}'}. \begin{verbatim} Assume T1 (H1) \end{verbatim} puts `\texttt{H1:T1}' in the local context. If instead of `\texttt{Assume T1 (H1)}' we apply \begin{verbatim} Assume T1 \end{verbatim} then `\texttt{\char`\_:T1}' is put in the local context. In both cases the new subgoal\hfill\break\mbox{becomes `\texttt{T2}'}. We can use both tactics with a list of arguments. For example, if a goal is of the shape \begin{verbatim} (x,y:U1;z:U2)T1 -> T2 -> T3 \end{verbatim} we can then apply \begin{verbatim} Let_ x,y be U1 and z be U2. Assume T1 (H1) and T2. \end{verbatim} to add \texttt{x},\texttt{y},\texttt{z},\texttt{T1},\texttt{T2} to the local context and we get \texttt{T3} as the new subgoal. \key{Let\_} and \key{Assume} are also applicable to goals of which the head is a defined constant. For example: \begin{verbatim} Coq < Lemma example: (Included U A B). 1 subgoal U : Type A : (Ensemble U) B : (Ensemble U) ============================ (Included U A B) example < Let_ x be U. 1 subgoal U : Type A : (Ensemble U) B : (Ensemble U) x : U ============================ (In U A x)->(In U B x) \end{verbatim} where the definition of \texttt{Included} is \begin{verbatim} Definition Included : Ensemble -> Ensemble -> Prop := [B, C: Ensemble] (x: U) (In B x) -> (In C x). \end{verbatim} \vspace{0.5cm} \paragraph{The implementation:}\ The tactics \key{Let\_} and \key{Assume} are defined with 3 tactics: \begin{itemize} \item \key{Match Context With} which enables the user apply \key{Let\_} only to dependent products and \key{Assume} only to non-dependent products; \item \key{Intro} which adds a variable or an assumption to the local context; \item \key{Change} which checks the correctness of arguments, i.e., whether what the user typed corresponds to the goal. In the case of \key{Let\_}, this is the type of a variable, in the case of \key{Assume}, this is the assumption. \end{itemize} \subsection{Have} \label{have} \qkey{Have} \notion{formula} [ \punct{(} \notion{label} \punct{)} ] [ \punct{[} \notion{tactic} \punct{]} ] \punct{.} \medskip The tactic is applicable to any goal. It adds the hypothesis \notion{formula} to the local context with a name \notion{label}. The tactic \notion{tactic} is to prove this hypothesis. For example: \begin{verbatim} 1 subgoal ................... H : (In U A x) H0 : (Included U A B) ................... ============================ True example < Have (In U B x) (H2) [by H, H0]. 1 subgoal ................ H : (In U A x) H0 : (Included U A B) ................ H2 : (In U B x) ============================ True \end{verbatim} \vspace{0.5cm} \paragraph{The implementation:}\ \vspace{0.5cm} \key{Have} applies \key{Cut} \notion{formula}. Then it applies \key{Intro} to the first subgoal and \notion{tactic} to the second one. \subsection{Iterated equality} [ \qkey{Thus} ] ( \punct{\char`\_=} $|$ \punct{\char`\_[=]} $|$ \punct{=\char`\_} $|$ \punct{[=]\char`\_} ) \notion{term} [ \punct{[} \notion{tactic} \punct{]} ] \punct{.} \medskip In mathematics one often writes chains of equalities, like for example:\footnote{In the second step this uses that $n - d = dq + r$.} $$n = (n - d) + d = dq + r + d = d (q + 1) + r$$ MMode (like Mizar) has the possibility to write this kind of `iterated equalities'. In MMode this example becomes (the lines are taken from the HMode example called \url{euclid.v}): \begin{center} \verb| Have n = ((n-,d)[+]d) [by ge_imp_mon_plus_eq, A5].| \\ \verb| _= (d[x]q[+]r[+]d) [by A8]. | \\ \verb| _= (d[x](S q)[+]r) [by compute]. | \end{center} Note that this one iterated equality turns into three MMode tactics, of which the first is \key{Have} and the other two are \punct{\char`\_=}. \vspace{0.5cm} In order to do an iterated equality first we apply the \key{Have} tactic to add an initial equality to the local context. Then the tactic \texttt{\char`\_=} or \texttt{=\char`\_} replaces the right hand side or left hand side of the equality, respectively with \notion{term}. The \notion{tactic} is to prove the equality of the \notion{term} and the expression we want to replace. We apply `\key{Thus} \texttt{\char`\_=}' or `\key{Thus} \texttt{=\char`\_}' if a goal and the last hypothesis in the local context are equalities. Suppose that a goal is the equality `\texttt{a = c}', and `\texttt{a = b}' is the last hypothesis in the local context. Then to prove the goal we apply \mbox{`\texttt{Thus \char`\_= c [tactic]}'} , where as the argument \texttt{tactic} we need to put a tactic that solves `\texttt{b = c}'. The tactics \punct{\char`\_[=]}, \punct{[=]\char`\_} were defined to do iterative equalities in C-CoRN. They work in an analogous way to \punct{\char`\_=} and \punct{=\char`\_}, respectively. \vspace{0.5cm} \paragraph{The implementation:}\ \vspace{0.5cm} We explain how the tactic \punct{\char`\_=} works. The tactic \punct{=\char`\_} is defined in an analogous way. Suppose that the last hypothesis in the local context is the equality \texttt{a = b} and we apply \texttt{\char`\_= c [tactic]}. Then, the following steps are performed: \begin{itemize} \item \texttt{Cut (a = c)} \item The equality \texttt{a = c} is added to the local context of the first subgoal by \key{Intro}. The equality \texttt{a = b} is removed from that context. \item The theorem about transitivity of equality is applied to the second goal. This generates two subgoals: \texttt{a = b} and \texttt{b = c}. As the last hypothesis in the context is \texttt{a = b}, the first subgoal is solved by \key{Exact}. The second one is solved by the argument \texttt{tactic}. \end{itemize} \subsection{Claim} \label{claim} \qkey{Claim} \notion{formula} [ \punct{(} \notion{label} \punct{)} ] \punct{.} \\ \quad \notion{proof} \\ \qkey{End\_claim} \punct{.} \medskip It adds, like \key{Have}, the hypothesis \notion{formula} with the name \notion{label} to the local context. The \notion{proof} is a proof of this hypothesis. Suppose that the goal is the formula \texttt{G} and we need the formula \texttt{A} to prove it. Then we can apply \texttt{Claim A (H1)}. \begin{verbatim} 1 subgoal ... ============= G Claim A (H1). 3 subgoals ... ============= A A G \end{verbatim} It will generate \texttt{A} as a subgoal twice. After having proved the first subgoal, the formula \texttt{A} will be added to the local context. Then we need to apply \key{End\_claim} tactic that will prove the second one\footnote{After having proved \texttt{A}, it will be added to the local context with a label generated by Coq. After applying \key{End\_claim} the right label (the label we put as an argument of \key{Claim}) will be assigned to \texttt{A}.} \begin{verbatim} 2 subgoals ... H1:A ============= A G End_claim. 1 subgoal ... H1:A ============= G \end{verbatim} Therefore we have \texttt{A} in the local context and we continue the proof of \texttt{G}. The reason why the \notion{formula} is generated as a subgoal twice is to improve the readability of a proof script. \key{End\_claim} indicates the end of the proof of the \notion{formula} in the proof script. \subsection{Thus thesis} \qkey{Thus} \qkey{thesis} \punct{[} \notion{tactic} \punct{]} \punct{.} \medskip The tactic is applicable to any goal. We use this tactic to finish a proof, i.e., to do the last step. As the argument \notion{tactic} we put a tactic that proves the goal. Example: \begin{verbatim} ............... A8 : x0 E X A10 : ~x0 E X ............... ============================ x0 E A Included_Add < Thus thesis [by A8,A10]. Subtree proved! \end{verbatim} %\subsubsection{} \bigskip \qkey{Thus} \notion{formula} \punct{[} \notion{tactic} \punct{]} \punct{.} \medskip The tactic is applicable to a goal that is a conjunction. As the argument \notion{formula} we put a formula that is a part of the conjunction and as the argument \notion{tactic} a tactic to prove this formula. Then the goal is reduced to a conjunction without this formula. Example: \begin{verbatim} ............ d : nat n : nat A2 : n(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace A10: O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace A10: O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace n : nat ============================ (P n) nat_factorizes < First case (prime n) (A1). P := [n:nat]O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace n : nat A1 : (prime n) ============================ (P n) subgoal 2 is: (prime n)\$/(P n) \end{alltt} What kind of disjunction is generated depends on the types of the first subgoal and the \notion{formula}. After having proved the first case, we have as a goal the disjunction statement of the first case formula and the goal formula. In our example it will be: \begin{verbatim} (prime n)\/(P n) \end{verbatim} We consider the next case with the tactic \key{Next case}. It adds the argument \notion{formula} to the local context. The first goal is again the goal which we prove by cases and the second one the disjunction statement formed with the first case formula, the next case formula and the goal formula. For example: \begin{alltt} P := [n:nat]O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace n : nat .............. ============================ (prime n)\$/(P n) nat_factorizes < Next case ~(prime n) (A1). P := [n:nat]O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace n : nat .............. A1 : ~(prime n) ============================ (P n) subgoal 2 is: ((prime n)\$/~(prime n))\$/(P n) \end{alltt} To consider next cases, we apply \key{Next case}. Every time it adds \notion{formula}. The first subgoal becomes the goal that we prove by cases. The second one is a disjunction that is enlarged by \notion{formula}. For example, if we considered four cases \texttt{A}, \texttt{B}, \texttt{C}, \texttt{D} then the second subgoal would be `\texttt{(A \$/ B \$/ C \$/ D) \$/ goal}'. Note that the outermost disjunction is associated to the left. After all the cases are done, the goal is a disjunction statement generated by the tactics \key{First case} and \key{Next case}. We apply \key{End\_cases} to prove it. First \key{End\_cases} applies \key{Left}. Since the disjunction is associated to the left, the current goal becomes a disjunction of all cases that we considered. Then the tactic \notion{tactic} is applied. In other words the \notion{tactic} is to justify that we could split the proof into cases. In our example there are two cases. After the second one is done, we have: \begin{alltt} P := [n:nat]O(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace n : nat .............. ============================ ((prime n)\$/~(prime n))\$/(P n) \end{alltt} We finish the proof by applying \texttt{End\char`\_cases [by prime\char`\_dec]}. First, the goal is reduced to \begin{verbatim} ((prime n)\/~(prime n)) \end{verbatim} by the \key{Left} tactic and then it is proved by the tactic \texttt{by prime\char`\_dec}, where \texttt{prime\char`\_dec} states: \begin{verbatim} prime_dec : (n:nat)(prime n)\/~(prime n) \end{verbatim} \vspace{0.5cm} \paragraph{The implementation:}\ \vspace{0.5cm} The solution that we justify the proof `by cases' after considering all cases was implemented in order to be able to use the \key{by} tactic for it. One cannot use \key{by} at the beginning because there is nothing to be justified then, because the cases we want to consider are not listed yet. Another solution can be to define a tactic that does not use \key{by}. For example: \begin{verbatim} Tactic Definition per_cases_by argument_lemma arg1 arg2 ... := Elim argument_lemma with arg1 arg2 .... \end{verbatim} where as the argument \texttt{argument\char`\_lemmma} we would put the identifier of the theorem that justifies the proof by cases and as \texttt{arg1}, \texttt{arg2}, etc. the values for dependent premises of this theorem. But then there is a problem with the number of these premises which varies and the order we should put them in. One more solution might be that instead of \key{Elim with} we use \key{Elim} and then as an argument for \key{Elim} we would put the application of the theorem to these values. We think that the implemented solution is more elegant and is also closer to the Mizar solution. There are a few kinds of the disjunction statements in Coq depending what the types of the formulas in the given statement are. In order to form the right kind of disjunction the type of the argument \notion{formula} in the tactics \key{First case} and \key{Next case} and the type of a goal is checked. We had to define separate tactics in CMode and HMode because in C-CoRN and Henk Barendregt's files new types are introduced: \texttt{CProp} and \texttt{cprop}. \subsection{Show\_} \qkey{Show\_} \notion{formula} \punct{.} \medskip The tactic is a synonym of the tactic \key{Change}. It was defined to improve the readability of a proof script. We use it if we want to indicate in the proof script what the current goal is. As the argument \notion{formula} we put the current goal. Example: \begin{verbatim} 1 subgoal ============================ (n:nat)~n=(S n) n_Sn < Proof. n_Sn < Induction n. 2 subgoals n : nat ============================ ~(0)=(1) subgoal 2 is: (n0:nat)~n0=(S n0)->~(S n0)=(S (S n0)) n_Sn < Show_ (~(0)=(1)). 2 subgoals n : nat ============================ ~(0)=(1) subgoal 2 is: (n0:nat)~n0=(S n0)->~(S n0)=(S (S n0)) \end{verbatim} The proof script looks like: \begin{verbatim} .............. Induction n. Show_ ~(0)=(1). .............. \end{verbatim} Therefore, we have information that after the application of \key{Induction} the goal is `\texttt{\~{}(0)=(1)}'. \subsection{Then} The tactics: \key{Then}, \key{Then consider}, \key{Hence thesis} are variants of the tactics \key{Have}, \key{Consider}, \key{Thus thesis}, respectively. The difference is that if we put as the argument \notion{tactic} the \key{by} tactic then the \key{by} takes as an argument also the last hypothesis in the local context. For details about \key{by} see section~\ref{by}. Example: \begin{verbatim} 2 subgoals ............... A8 : x0 E X A11 : x0 E (A u {x}) _ : ~x0 E X ============================ x0 E A subgoal 2 is: (x0 E A\/x==x0)\/x0 E A Included_Add < Hence thesis [by A8]. 1 subgoal ................ A8 : x0 E X A11 : x0 E (A u {x}) ============================ (x0 E A\/x==x0)\/x0 E A \end{verbatim} The \key{by} tactic took as the arguments the hypotheses `\texttt{A8}' and `\texttt{\char`\_}'. \vspace{0.5cm} \paragraph{The implementation:}\ \vspace{0.5cm} The tactics with variant `\key{Then}' apply their mother tactics with the tactic \key{LINK} as an argument. The tactic \key{LINK} calls \key{Generalize} for the last hypothesis in the local context. Suppose that we have the following context with \texttt{G} as a goal: \begin{verbatim} H1: P ... _: P -> Q ============ G \end{verbatim} When we apply `\texttt{Then Q [by H1]}', the formula \texttt{Q} will be generated as the second goal. Then \key{LINK} will be applied to this subgoal. It will call \texttt{Generalize \char`\_}. Next \key{by} will call \texttt{Generalize H1}, clear context and call \texttt{Try Intros}. Therefore in the context we will have the formula \texttt{P -> Q} (the last hypothesis in the context when we called \key{Then}) and the formula \texttt{P} (put as an argument for \key{by}). \subsection{Dealing with labels} \label{labels} The tactics: \key{Assume}, \key{Have}, \key{Claim}, \key{Consider}, \key{First case} and \key{Next case} have an optional argument called \notion{label}. This is to give a name for the hypotheses which we can add to the context with these tactics. Example: \begin{verbatim} .................. ============================ X =c (A u {x})->X =c A\/(EXT A'|X==A' u {x}/\A' =c A) Included_Add < Assume (X =c (A u {x})) (A1). 1 subgoal ................... A1 : X =c (A u {x}) ============================ X =c A\/(EXT A'|X==A' u {x}/\A' =c A) \end{verbatim} All the hypotheses in the context must have names. So if one does not specify what name we want to assign to a hypothesis, Coq generates it automatically. Then in the context we have a hypothesis that has a name that is not present in the proof script. While proving the user rather looks at the context and the goals generated by Coq than at the proof script. So it may happen that the user uses such a name as a reference for the \key{by} tactic and that makes the proof script unreadable. To avoid this, the hypothesis is added to the local context with the name `\texttt{\char`\_}' if the user does not put the argument \notion{label}. Example: \begin{verbatim} .................. ============================ X =c (A u {x})->X =c A\/(EXT A'|X==A' u {x}/\A' =c A) Included_Add < Assume (X =c (A u {x})). 1 subgoal ................... _ : X =c (A u {x}) ============================ X =c A\/(EXT A'|X==A' u {x}/\A' =c A) \end{verbatim} and the user is aware that such a hypothesis is not labeled in their proof script. Coq does not allow to have the hypotheses with the same names. If the user does not give a name for another hypothesis, the previous one is removed and the new one gets a name `\texttt{\char`\_}'. If we want to check whether such and such hypothesis was introduced we can look into the proof script. \subsection{Sketch mode} \label{missing} When we formalize mathematics we often want to prove some facts later, in order to be able to first work on the main proof. In Coq we can use the \key{Cut} tactic or declare these facts as axioms. In Mizar mode we implemented another solution. It requires to declare \texttt{Require Sketch}. Then we can add to the local context a hypothesis without justification. Above this hypothesis an error message is generated. Example: \begin{verbatim} 1 subgoal H : P->Q ============================ Q example < Have P (H1). 1 subgoal H : P->Q error : inference_not_accepted H1 : P ============================ Q \end{verbatim} So we have \texttt{P} in the local context and we can continue our proof. The error message is also generated when we do not put enough justification. This feature we can use with the tactics: \key{Have}, \key{Consider}, \punct{=\char`\_}, \punct{\char`\_=}, \key{Then}, \key{Then consider}. We can only have one error message in the local context. If another unjustified hypothesis is added to the local context then the error message, referring to the previous one, will be removed and the error message will be generated above this hypothesis. The continuation of the previous example: \begin{verbatim} 1 subgoal H : P->Q error : inference_not_accepted H1 : P ============================ Q example < Have R (H2). 1 subgoal H : P->Q H1: P error : inference_not_accepted H2 : R ============================ Q \end{verbatim} The error message for the hypothesis \texttt{H1} has been removed and the new error message refers to the hypothesis \texttt{H2}. To find the unjustified hypotheses in the local context we need to comment `\texttt{Require Sketch}' then Coq will stop checking at the first error. One can also check whether a proof consists of the unjustified hypotheses by searching the proof term for \texttt{missing\char`\_proof\char`\_of}. For example, in the proof below we added the formula \texttt{(In U X x)} without justification. \begin{verbatim} x : U H : (In U (Intersection U X Y) x) ============================ (In U (Union U X Y) x) example < Have (In U X x). 1 subgoal x : U H : (In U (Intersection U X Y) x) error : inference_not_accepted _ : (In U X x) ============================ (In U (Union U X Y) x) example < Hence thesis [by Union_introl]. Subtree proved! \end{verbatim} In the proof term, we can see that the `axiom' \texttt{missing\char`\_proof\char`\_of} was applied to add the formula \texttt{(In U X x)} to the local context: \begin{verbatim} example = [x:U; _:(In U (Intersection U X Y) x)] [H0:=(missing_proof_of (In U X x))] [H1:=[_:(In U X x)](Union_introl U X Y x _)](H1 H0) : (Included U (Intersection U X Y) (Union U X Y)) \end{verbatim} A little different situation is when we use tactics: \key{Thus thesis}, \key{Thus thesis}, \key{Hence thesis}, `\key{Thus \texttt{\char`\_=}}', `\key{Thus \texttt{=\char`\_}}'. If our justification is not enough or we do not put any justification, then the error message replaces the current goal. In order to continue the proof we need to apply the tactic \key{cp}. \begin{verbatim} H : P H0 : P->Q ============================ Q subgoal 2 is: True test < Thus thesis [by H]. 2 subgoals H : P H0 : P->Q ============================ inference_not_accepted subgoal 2 is: True test < cp. 1 subgoal H : P H0 : P->Q ============================ True \end{verbatim} \vspace{0.5cm} \paragraph{The implementation:}\ \vspace{0.5cm} To `solve' a goal the following axiom is applied: \begin{verbatim} Axiom missing_proof_of : incomplete. Definition incomplete := (A:Type)A. \end{verbatim} Before `solving' the goal the tactic \key{Intro} adds to the local context the `hypothesis' \texttt{inference\char`\_not\char`\_accepted} with the label \texttt{error}. The type\hfill\break\texttt{inference\char`\_not\char`\_accepted} is defined as follows: \begin{verbatim} Definition inference_not_accepted := True. \end{verbatim} \section{Examples} % first version: Mariusz \label{examples} We present four proofs in Mizar Mode language. \subsection{Example from the Coq library} The first one is on a fact from the set theory. Standard Coq symbols were replaced by other ones to make the proof closer to mathematical text. \begin{itemize} \item `\texttt{E}' denotes a predicate of being an element (\texttt{In}) of a set (\texttt{Ensemble}) \item `\texttt{=c}' denotes inclusion relation between two sets (\texttt{Included}) \item `\texttt{\char`\{\ \char`\}}' denotes a set containing only one element (\texttt{Singleton}) \item `\texttt{u}' denotes union of two sets (\texttt{Add}) \item `\texttt{-}' denotes subtraction of two sets (\texttt{Subtract}) \end{itemize} \begingroup \def\{{\char`\{} \def\}{\char`\}} \begin{alltt}\footnotesize Lemma Included_Add: (X, A: (Ensemble U))(x:U) (X =c (A u \{x\})) -> (X =c A) \$/ (EXT A' | X == A' u \{x\} /\$ (A' =c A)). Proof. Let_ X,A be (Ensemble U) and x be U. Assume (X =c (A u \{x\})) (A1). First case (x E X) (A3). Take (X-\{x\}) and prove (X==(X-\{x\}) u \{x\}/\$(X-\{x\}) =c A). Have (X =c (X - \{x\} u \{x\})) (A4) [by add_soustr_2,A3]. Have ((X - \{x\}) u \{x\} =c X) [by add_soustr_1, A3]. Hence (X == ((X - \{x\}) u \{x\})) [by Dbl_Inc_Eq, A4]. Let_ x0 be U. Assume (x0 E (X - \{x\})). Then ((x0 E X) /\$ (~x == x0)) (A6) [by Subtract_inv]. Then (x0 E (A u \{x\})) (A10) [by A1]. First case (x0 E A). Hence thesis. Next case (x == x0). Hence thesis [by A6]. End_cases [by Add_inv, A10]. Next case (~(x E X)) (A7). Claim (X =c A). Let_ x0 be U. Assume (x0 E X) (A8). Then (x0 E (A u \{x\})) (A11) [by A1]. First case (x0 E A). Hence thesis. Next case (x == x0). Then (~(x0 E X)) [by A7]. Hence thesis [by A8]. End_cases [by Add_inv,A11]. End_claim. Hence thesis. End_cases [by classic]. Qed. \end{alltt} \endgroup The original proof comes from the Coq standard library: \begin{alltt}\footnotesize Lemma Included_Add: (X, A: (Ensemble U)) (x: U) (Included U X (Add U A x)) -> (Included U X A) \$/ (EXT A' | X == (Add U A' x) /\$ (Included U A' A)). Proof. Intros X A x H'0; Try Assumption. Elim (classic (In U X x)). Intro H'1; Right; Try Assumption. Exists (Subtract U X x). Split; Auto with sets. Red in H'0. Red. Intros x0 H'2; Try Assumption. LApply (Subtract_inv U X x x0); Auto with sets. Intro H'3; Elim H'3; Intros K K'; Clear H'3. LApply (H'0 x0); Auto with sets. Intro H'3; Try Assumption. LApply (Add_inv U A x x0); Auto with sets. Intro H'4; Elim H'4; [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. Elim K'; Auto with sets. Intro H'1; Left; Try Assumption. Red in H'0. Red. Intros x0 H'2; Try Assumption. LApply (H'0 x0); Auto with sets. Intro H'3; Try Assumption. LApply (Add_inv U A x x0); Auto with sets. Intro H'4; Elim H'4; [Intro H'5; Try Exact H'5; Clear H'4 | Intro H'5; Clear H'4]. Absurd (In U X x0); Auto with sets. Rewrite <- H'5; Auto with sets. Qed. \end{alltt} \subsection{Example of a HMode proof} The second one is on the fact from the number theory that every natural number can be factorized into a product of primes. The original proof was taken from Henk Barendregt's files. \begin{alltt}\footnotesize Lemma nat_factorizes : (n:nat)(O(EX L:ListN |((allprimes L)/\$(n=(Prod L)))). Proof. LetTac P :=[n:nat](O(EX L:ListN |((allprimes L)/\$(n=(Prod L)))). Claim ((n:nat)(before n P) -> (P n)) (A16). Let_ n be nat. Assume (before n P) (A10). First case (prime n) (A1). Assume ((O) < n). Have (allprimes (cons n nil)) (A2) [by A1]. Have n=(Prod (cons n nil)) (A3) [by refl_equal, times_com]. Take (cons n nil) and prove ((allprimes (cons n nil))/\$n=(Prod (cons n nil))). Thus thesis [by A2, A3]. Next case ~(prime n). Assume ((O) < n) (A6). Consider pp such that ([pp:nat](primediv pp n)) (A5) [by nat_HPD]. Then (pp [|] n). Then consider x such that ([s:nat] (((O)(nonConst CC f)->{z:CC | f!z[=]Zero} \end{verbatim} The problem is that \texttt{Induction n} adds this hypothesis to the context automatically and we can not make any indication of it in the proof script. \begin{alltt}\footnotesize Lemma fta' : (n:nat)(f:(cpoly_cring CC)) (degree_le n f) -> (nonConst ? f) -> {z:CC | f!z [=] Zero}. Proof. Let_ n be nat. Induction n. Show_ (f:(cpoly_cring CC)) (degree_le (O) f)->(nonConst CC f)->{z:CC | f!z[=]Zero}. Let_ f be (cs_crr (cpoly_cring CC)). Assume (degree_le O f) (A0) and (nonConst CC f). Then consider n such that ([n:nat](lt (O) n)) (A2) and ([n:nat]((nth_coeff n f)[#]Zero)) (A3). Have ((nth_coeff n f) [=] Zero) [by A2, A0]. Then (Not (nth_coeff n f)[#]Zero) [by eq_imp_not_ap]. Hence thesis [by A3]. Show_ ((f:(cpoly_cring CC)) (degree_le (S n) f)->(nonConst CC f)->{z:CC | f!z[=]Zero}). Let_ f be (cs_crr (cpoly_cring CC)). Assume (degree_le (S n) f) (A1) and (nonConst CC f). Then consider m' such that ([m':nat] (lt (0) m')) (A4) and ([m':nat]((nth_coeff m' f)[#]Zero)) (A5). Then f[#]Zero [by nth_coeff_ap_zero_imp]. Then consider c such that ([c:CC](f!c[#]Zero)) [by poly_apzero_CC]. Then consider a such that ([a:CC]({b:CC & {g:cpoly_cring CC | (degree_le n g) | (f[=] ((_C_ a)[*]_X_[+] (_C_ b))[*]g)}})) [by FTA_1', A1]. Then consider b such that ([b:CC]({g:cpoly_cring CC | (degree_le n g) | (f[=] ((_C_ a)[*]_X_[+](_C_ b))[*] g)})). Then consider g such that ([g:(cpoly_cring CC) ](degree_le n g)) (A6) and ([g:(cpoly_cring CC)](f[=]((_C_ a)[*]_X_[+](_C_ b))[*]g)) (A7). First case ({m:nat | (S m)=m'}). Then consider m such that ([m:nat](S m)=m') (A8). Have (nth_coeff (S m) f) [=] (nth_coeff (S m) ((_C_ a)[*]_X_[+](_C_ b))[*]g) (A9). _[=] a[*](nth_coeff m g)[+]b[*](nth_coeff (S m) g). Have ((nth_coeff (S m) f)[#] Zero) [by A8,A5]. Then (a[*](nth_coeff m g)[+]b[*](nth_coeff (S m) g) [#] Zero) (A10) [by A9,ap_well_def_lft_unfolded]. First case (a[*](nth_coeff m g)[#]Zero). Then (a [#] Zero) (H6') [by cring_mult_ap_zero]. Have f!([--]b[/]a[//]H6') [=] (((_C_ a)[*]_X_[+](_C_ b))[*]g)!([--]b[/]a[//]H6') (A11). _[=] ((_C_ a)[*]_X_[+](_C_ b))!([--]b[/]a[//]H6')[*]g!([--]b[/]a[//]H6').\negspace _[=] (((_C_ a)[*]_X_)!([--]b[/]a[//]H6')[+] (_C_ b)!([--]b[/]a[//]H6'))[*] g!([--]b[/]a[//]H6'). _[=] ((_C_ a)!([--]b[/]a[//]H6')[*]_X_!([--]b[/]a[//]H6')[+]b)[*]\negspace g!([--]b[/]a[//]H6'). _[=] (a[*]([--]b[/]a[//]H6')[+]b)[*]g!([--]b[/]a[//]H6') _[=] (Zero::CC). Take ([--]b[/]a[//]H6') and prove (f!([--]b[/]a[//]H6')[=]Zero). Thus thesis [by A11]. Next case (b[*](nth_coeff (S m) g)[#]Zero) (A12). Claim (nonConst CC g). Have (lt (0) (S m)) (A13) [by A4 , A8]. Have (nth_coeff (S m) g)[#]Zero (A14) [by cring_mult_ap_zero_op, A12]. Take (S m) and prove (lt (O) (S m)) and ((nth_coeff (S m) g)[#]Zero).\negspace Thus thesis [by A13]. Thus thesis [by A14]. End_claim. Then consider z such that ([z:CC](g!z[=]Zero)) [by Hrecn, A6]. Have f!z [=] (((_C_ a)[*]_X_[+](_C_ b))[*]g)!z (A15). _[=] ((_C_ a)[*]_X_[+](_C_ b))!z[*]g!z. _[=] (((_C_ a)[*]_X_[+](_C_ b))!z)[*]Zero. _[=] (Zero::CC) . Take z and prove (f!z[=]Zero). Thus thesis [by A15]. End_cases [by cg_add_ap_zero, A10]. Next case (O) = m'. Then (lt (O) (O)) [by A4]. Hence thesis [by lt_n_n]. End_cases [by O_or_S]. Qed. \end{alltt} \subsection{Example from the Mizar library} The fourth one is a proof on the equality of the minimum of two real numbers and the absolute value of the subtraction of these numbers. Likewise in the above proof of FTA theorem the tactic \texttt{Let\char`\_\ x,y be IR} cannot be used because of coercion. The original proof was taken from Mizar library and is presented below MMode proof. \begin{alltt}\footnotesize Lemma min_abs: (x,y:IR) (Min x y) [=] (x [+] y [-] (AbsIR (x [-] y))) [/] Two [//] (two_ap_zero IR). Proof. Let_ x,y be (cs_crr IR). First case (x [<=] y) (H). Have (Min x y) [=] x [by eq_symmetric_unfolded, leEq_imp_Min_is_lft,H].\negspace _[=] ((x [+] x)[/](Two::IR)[//](two_ap_zero IR)). _[=] ((x[+]y)[-](y[-]x))[/](Two::IR)[//](two_ap_zero IR).\negspace _[=] ((x[+]y)[-]((Max x y)[-]x))[/](Two::IR)[//](two_ap_zero IR) \negspace [by H,leEq_imp_Max_is_rht; Auto 6 with algebra_r algebra algebra_c algebra_s].\negspace _[=] ((x[+]y)[-]((Max x y)[-](Min x y)))[/](Two::IR)[//]\negspace (two_ap_zero IR) [by H,leEq_imp_Min_is_lft; Auto 6 with algebra_r algebra algebra_c algebra_s].\negspace Thus _[=] ((x[+]y)[-](AbsIR (x[-]y)))[/](Two::IR)[//](two_ap_zero IR)\negspace [by eq_symmetric_unfolded, Abs_Max;Algebra]. Next case y[<=]x (H1). Have (Min x y) [=] (Min y x) [by Min_comm]. _[=] y [by eq_symmetric_unfolded, leEq_imp_Min_is_lft, H1; \negspace Algebra]. _[=] ((Two [*] y))[/](Two::IR)[//](two_ap_zero IR) . _[=] ((x[+]y)[-](x[-]y))[/](Two::IR)[//](two_ap_zero IR).\negspace _[=] ((x[+]y)[-](x[-](Min y x)))[/](Two::IR)[//](two_ap_zero IR)\negspace [by eq_symmetric_unfolded, leEq_imp_Min_is_lft, H1;\negspace Auto 6 with algebra_r algebra algebra_c algebra_s].\negspace _[=] ((x[+]y)[-]((Max y x)[-](Min y x)))[/](Two::IR)[//]\negspace (two_ap_zero IR) [by eq_symmetric_unfolded, leEq_imp_Max_is_rht, H1;\negspace Auto 6 with algebra_r algebra algebra_c algebra_s].\negspace _[=] ((x[+]y)[-]((Max x y)[-](Min y x)))[/](Two::IR)[//]\negspace (two_ap_zero IR) [by Max_comm;Algebra]. _[=] ((x[+]y)[-]((Max x y)[-](Min x y)))[/](Two::IR)[//]\negspace (two_ap_zero IR) [by Min_comm;Algebra]. Thus _[=] ((x[+]y)[-](AbsIR (x[-]y)))[/](Two::IR)[//](two_ap_zero IR)\negspace [by eq_symmetric_unfolded, Abs_Max;Algebra].\negspace End_cases [by LeEq_dec]. Qed. \end{alltt} The Mizar proof: \begin{alltt}\footnotesize theorem Th34: min(x,y) = (x + y - abs(x - y)) / 2 proof now per cases; suppose A1: x <= y; then 0 <= y - x by Th12; then A2: 0 <= -(x-y) by XCMPLX_1:143; thus min(x,y) = x by A1,Def1 .= (x+x)/2 by XCMPLX_1:65 .= (((x+y)-y)+x)/2 by XCMPLX_1:26 .= ((x+y)- (y - x))/2 by XCMPLX_1:37 .= ((x+y)- -(x - y))/2 by XCMPLX_1:143 .= ((x+y)-abs(-(x - y)))/2 by A2,ABSVALUE:def 1 .= ((x+y)-abs(x - y))/2 by ABSVALUE:17; suppose A3: y <= x; then A4: 0 <= x - y by Th12; thus min(x,y) = y by A3,Def1 .= (y+y)/2 by XCMPLX_1:65 .= (x+y-x+y)/2 by XCMPLX_1:26 .= ((x+y)- (x - y))/2 by XCMPLX_1:37 .= ((x+y)-abs(x-y))/2 by A4,ABSVALUE:def 1; end; hence thesis; end; \end{alltt} \section{Synonyms} % first version: Mariusz \label{synon} One of the main aims of our Mizar mode is to improve readability of Coq proofs. To make them look closer to mathematical text MMode was equipped with some synonyms of the basic tactics described in Section~\ref{implem}. They are available if we put the declaration \texttt{Require HMode\char`\_synon.} Here is the list of all synonyms. The \textit{tactic} argument is either \key{by} or a Coq tactic and has to be put in square brackets, the \textit{label} argument has to be put in round brackets. The only exception is the synonym \key{The ... is ...} for the \key{Assume} tactic, where \textit{label} has to be put in square brackets. In this list square brackets mean an optional argument. \begin{itemize} \item \key{Assume} \notion{formula} [\notion{label}] \notion{tactic}. Synonyms: \begin{itemize} \item \key{Now assume} \notion{formula}. \item \key{The} \notion{label} \key{is} \notion{formula}. \item \key{Indeed assume} \notion{formula label}. \end{itemize} \item \key{Have} \notion{formula} [\notion{label}] \notion{tactic}. \begin{itemize} \item \key{We have} \notion{formula} \notion{tactic}. \item \key{Secondly we have} \notion{formula} \notion{tactic} . \item \key{We have} \notion{tactic} \notion{formula} \notion{label}. \item \key{First we have} \notion{formula} \notion{label} \notion{tactic}. \item \key{Now} \notion{formula} \notion{label} \notion{tactic}. \item \key{Now} \notion{tactic} \key{we have} \notion{formula} \notion{label}. \end{itemize} \item \key{Then} \notion{formula} [\notion{label}] [\notion{tactic}]. \begin{itemize} \item \key{Also} \notion{formula} [\notion{label}] \notion{tactic}. \item \key{So} \notion{formula} \notion{label} [\notion{tactic}]. \item \key{Then} \notion{tactic} \notion{formula} \notion{label}. \item \key{Hence} \notion{tactic} \key{again} \notion{formula} \notion{label}. \item \key{Therefore} \notion{tactic} \notion{formula} \notion{label}. \end{itemize} \item \key{Thus thesis} \notion{tactic}. \begin{itemize} \item \key{Done} \notion{tactic}. \item \key{Then we are done} \notion{tactic}. \end{itemize} \item \key{Thus} \notion{formula} \notion{tactic}. \begin{itemize} \item \key{Done} \notion{formula} \notion{tactic}. \item \key{Firstly} \notion{formula} \notion{tactic}. \end{itemize} \item \key{Hence thesis} \notion{tactic}. \begin{itemize} \item \key{Hence done} \notion{tactic}. \item \key{Hence we have our claim} \notion{tactic}. \item \key{Hence claim done} \notion{tactic}. \item \key{So we are done} \notion{tactic}. \end{itemize} \item \key{Show\_} \notion{formula}. \begin{itemize} \item \key{We need to prove} \notion{formula}. \item \key{Finally we need to prove} \notion{formula}. \end{itemize} \item \key{Claim} \notion{formula}. \begin{itemize} \item \key{Secondly claim} \notion{formula}. \end{itemize} \item \key{Take} \notion{variable} \key{and prove} \notion{formula}. \begin{itemize} \item \key{Finally take} \notion{variable} \key{and prove} \notion{formula}. \end{itemize} \item \key{Then consider} \notion{variable} \key{such that} \notion{formula} \notion{label}. \begin{itemize} \item \key{Now choose} \notion{variable} \key{such that} \notion{formula} \notion{label}. \end{itemize} \item \key{First case} \notion{formula} [\notion{label}]. \begin{itemize} \item \key{Case 1} \notion{formula} [\notion{label}]. \end{itemize} \item \key{Next case} \notion{formula} [\notion{label}]. \begin{itemize} \item \key{Case 2} \notion{formula} [\notion{label}]. \end{itemize} \item \key{Apply} \notion{term}. \begin{itemize} \item \key{We apply} \notion{term}. \end{itemize} \item \key{Idtac}. \begin{itemize} \item \key{So we have proved} \notion{label}. \item \key{Secondly}. \end{itemize} \end{itemize} The definition of the tactic \key{Claim} in the \texttt{HMode\char`\_synon} is different from the definition of the \key{Claim} in the \texttt{MMode}. In the \texttt{MMode} the \key{Claim} requires to apply the tactic \key{End\_claim} after we have finished the proof (see~\ref{claim}) while in the \texttt{HMode\char`\_synon} it does not. The \key{End\_claim} is to indicate in the proof script the end of the `claim' proof. In the \texttt{HMode\char`\_synon} we do not need such a tactic. We have tactics like \key{Hence claim done} which realize two things. We can do the last step in the `claim' proof (in the MMode we use the \key{Thus thesis}) and the tactic indicates in the proof script the end of the `claim' proof (the \key{Thus thesis} is not so meaningful). \setlength{\parindent}{\oldparindent} The version of Mizar mode with synonyms is so far only an experiment. The above list was prepared to play with two proofs. The one is presented below, it is again the proof that every natural number can be factorized into a product of primes, and the second one, the proof of the Quotient-Remainder theorem, is available in the directory examples (\texttt{euclid\char`\_synon.v}). We are aware that the list should be enlarged and to the existing synonyms options like label should be added to make the version fully functional. \label{synonexample} \begin{alltt}\footnotesize Lemma nat_factorizes : (n:nat)(O(EX L:ListN |((allprimes L)/\$(n=(Prod L)))). Proof. LetTac P :=[n:nat](O(EX L:ListN |((allprimes L)/\$(n=(Prod L)))). We apply (cv_ind P). We need to prove ((n:nat)(before n P) -> (P n)). Let_ n be nat. The [IH] is (before n P). Case 1 (prime n) (A1). Now assume ((O)