% $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)