% $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{<http://www.cs.kun.nl/~freek/mmode/mmode.tar.gz>}.
\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<n->(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set
  n : nat
  IH : (before n P)
  A4 : O<n
  pp : nat
  A5 : (primediv pp n)
  x : nat
  A7 : O<pp/\$x[x]pp=n
  A8 : pp[x]x=n
  A9 : n=pp[x]x
  A10 : x=O
  A11 : x[x]pp=O
  _ : x[x]pp=n
  ============================
   O=n

subgoal 2 is:
 FF
subgoal 3 is:
 O<x
subgoal 4 is:
 (EX L:ListN|(allprimes L)/\$n=(Prod L))
subgoal 5 is:
 ((prime n)\$/~(prime n))\$/(P n)
\end{alltt}
\noindent
Although these proofs do not \emph{look} like Coq tactic scripts,
they \emph{are}.

\subsection{Coq equivalents of MMode tactics}

There are various ways to explain the meaning of the MMode steps.
In Section~\ref{implem} we will discuss them
in detail, but first for brevity we will just \emph{list} the MMode steps
and list how the same effect is obtained using traditional Coq tactics:
\begin{center}
\begin{tabular}{lp{23.5em}}
\key{by} & tactics like \key{Auto}/\key{EAuto}, \key{Prolog} and \key{Intuition} \\
\key{Let\_} & \key{Intro} \\
\key{Assume} & \key{Intro} \\
\key{Have}/\key{Then} & \key{Cut}/\key{Assert} \\
\key{Claim} & \key{Cut}/\key{Assert} \\
\key{Thus}/\key{Hence}$\qquad$ & \key{Exact}, possibly preceded by a \key{Split} of a conjunction in the goal \\
\key{Consider} & \key{Elim}, of an existential statement \\
\key{Take} & \key{Exists} \\
\notion{cases} & \key{Elim}, of a disjunction \\
\key{Show\_} & this does nothing (it just uses \key{Change} to verify the current goal)
\end{tabular}
\end{center}
\noindent
This table is not exact,\footnote{
In particular \key{by} is more general than the tactics mentioned here;
see Section~\ref{by} below for a precise description.
}
it just is meant to give a rough idea of what
the various MMode constructions are for.

Note that this table is very similar to the list of Mizar Light tactics in
\cite{wie:01}.
The differences are that here there is a distinction between
\key{Have} and \key{Claim} (both are equivalent to the tactic `\texttt{A}' in \cite{wie:01}),
and that in \cite{wie:01} there is no equivalent of \key{Show\_}.

\subsection{MMode steps and natural deduction}
\label{natded}

In this report, the MMode language will only be described in terms
of the Coq system.
However it is possible to give a more system independent account
of the MMode language.
Most of the semantics of this language is system (and even logic)
independent.

The only feature of MMode that does not have a `natural' meaning
is the \key{by} tactic.
Apart from that the language is just natural deduction and makes
sense for any logic that has the
connectives $\neg$, $\to$, $\land$, $\lor$, $\forall$ and $\exists$.

In this report we will not describe the meaning of the MMode language
in a system independent way (for such an account
of a language similar to MMode, see \cite{wie:00:1}).  We will just list
the correspondence between the natural deduction rules
for the logical connectives and the corresponding MMode
constructions:

\begin{center}
\begin{tabular}{clcl}
$\bot$ & elimination &$\quad$& \quad (\key{by}) \\
$\neg$ & introduction && \key{Assume} \\
$\neg$ & elimination && \quad (\key{by}) \\
$\to$ & introduction && \key{Assume} \\
$\to$ & elimination && \quad (\key{by}) \\
$\land$ & introduction && \key{Thus}/\key{Hence} \\
$\land$ & elimination && \quad (\key{by}) \\
$\lor$ & introduction && \quad (\key{by}) \\
$\lor$ & elimination && \notion{cases} \\
$\forall$ & introduction && \key{Let\_} \\
$\forall$ & elimination && \quad (\key{by}) \\
$\exists$ & introduction && \key{Take} \\
$\exists$ & elimination && \key{Consider}
\end{tabular}
\end{center}

\noindent
An entry of `(\key{by})` in this table means that the \key{by}
justification is used to reason using this rule.
For instance application of the rule of $\to$-elimination would be written
like:
\begin{quote}
\begin{alltt}
  ..............
  Have P->Q (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<d
  ............
  ============================
   n<d/\n=d[x]zero[+]n

subgoal 2 is:
 n<d\/(P n)

Euclid < Thus (n<d) [by A2].  
2 subgoals
  .............
  d : nat
  n : nat
  A2 : n<d
  .............
  ============================
   n=d[x]zero[+]n

subgoal 2 is:
 n<d\/(P n)

Euclid < Thus (n=d[x]zero[+]n) [by times_com].  
1 subgoal
  ...........
  d : nat
  n : nat
  ...........
  ============================
   n<d\/(P n)

\end{verbatim}

We can only prove one formula at a time. The formulas have to proved
in the same order as they are in a conjunction statement.

\subsection{Consider}

\qkey{Consider} \notion{var} \qkey{such} \qkey{that} 
\notion{bound-formula} [ \punct{(} \notion{label} \punct{)} ] \\
\{ \qkey{and} 
\notion{bound-formula} [ \punct{(} \notion{label} \punct{)} ] \} 
{} [ \punct{[} \notion{tactic} \punct{]} ] \punct{.}
\medskip

This tactic eliminates the existential quantifier. There are
four kinds of existential statements with one predicate in Coq:

\begin{verbatim}
{x:A | (P x)}
{x:A & (P x)}
(EX x | (P x))
(EXT x | (P x))
\end{verbatim}

depending on the types of \texttt{A} and \texttt{P}. As 
the argument \notion{var} we put a witness, as the argument
\notion{bound-propositions} the lambda term \texttt{[x:A](P x)}, 
as the argument \notion{label}
the name we want to give for the hypothesis \texttt{(P x)},
 and as the argument \notion{justification} a tactic that proves 
the existential statement we want to eliminate.
The tactic adds `\notion{var}\texttt{:A}' and 
`\notion{label}\texttt{: (P} \textit{var}\texttt{)}' to the local context.

For example,

\begin{alltt}

  ............
  P := [n:nat]O<n->(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace
  A10: O<x
  A12 : (P x)
  ............
  ============================
   (EX L:ListN|(allprimes L)/\$n=(Prod L))

Coq < Consider LL such that
                 [LL:ListN] (allprimes LL)/\$x=(Prod LL) (A13) [by A12,A10].\negspace
  
  ............
  P := [n:nat]O<n->(EX L:ListN|(allprimes L)/\$n=(Prod L)) : nat->Set\negspace
  A10: O<x
  A12 : (P x)
  ............
  LL : ListN
  A13 : (allprimes LL)/\$x=(Prod LL)
  ============================
   (EX L:ListN|(allprimes L)/\$n=(Prod L))

\end{alltt}


We use \key{Consider} in an analogous way in order to eliminate
the existential statements with two predicates. There are four
kinds of these statements in Coq:

\begin{verbatim}
 (EX x | P(x) & Q(x))
 (EXT x | P(x) & Q(x))
 {x:A | (P x) & (Q x)}
 {x:A & (P x) & (Q x)}
\end{verbatim}

To eliminate it, we apply:

\begin{verbatim}
Consider x such that [x:A](P x) (H1) and [x:A](Q x) (H2) [tactic]
\end{verbatim}

It adds `\texttt{x:A}', `\texttt{H1 : (P x)}', `\texttt{H2 : (Q x)}' 
to the local context. The \texttt{tactic} justifies the existential statement
we want to eliminate.

There are two more kinds existential statements in the C-CoRN library. We apply
\key{Consider} to eliminate them in the same way.

\vspace{0.5cm}

\paragraph{The implementation:}\

\vspace{0.5cm}

First the right existential statement is formed from the argument 
\notion{bound-proposi\-tions}. Then \key{Cut} is called with this statement
as an argument. To the first subgoal the following tactics are applied:

\begin{itemize}
\item
\key{Intro} in order to add an existential statement to the local context

\item
\key{Elim} in order to eliminate this existential statement

\item
\key{Intro} in order to add the variable \notion{var} and
a predicate to the local context.
\end{itemize}

To the second one, the tactic \notion{tactic} is applied.

We tried to implement \key{Consider} as a tactic of grammar:

\vspace{0.5cm}

\qkey{Consider} \notion{var} \qkey{being} \notion{type} 
\qkey{such} \qkey{that} \notion{formula} \notion{label} 
[ \punct{[} \notion{tactic} \punct{]} ] \punct{.}

\vspace{0.5cm}

where as the \notion{formula} we would put the application
of the \notion{var} to a predicate. For example,
instead of typing:

\begin{verbatim}
Consider x such that [x:A](P x) [tactic].
\end{verbatim}

we would type

\begin{verbatim}
Consider x being A such that (P x) [tactic].
\end{verbatim}

This solution is more elegant. But we did not manage to implement it
because we cannot use `\texttt{(P x)}' as an argument. The variable
\texttt{x} is not yet in the context when we call 
\key{Consider} and Coq does not accept the formula \texttt{(P x)}
(does not know what to apply to the predicate \texttt{P}).

\subsection{Take}

\qkey{Take} \notion{term} \qkey{and} \qkey{prove} 
\notion{formula} \{ \qkey{and} \notion{formula} \} \punct{.}
\medskip

This tactic is applicable to a goal that is an existential statement
or a disjunction statement that includes an existential statement.
As the argument \notion{term} we put an object that satisfies the predicate 
of the existential statement. As the argument \notion{formula} we put 
the application of the object to that predicate. The goal is reduced 
to the \notion{formula}. 

\textit{Example 1}

\begin{verbatim}
1 subgoal
  
  .........
  n : nat
  .........
  ============================
   (EX r:nat|r<d/\n=d[x]zero[+]r)

Euclid < Take n and prove (n<d/\n=d[x]zero[+]n). 
1 subgoal
  
  ...........
  n : nat
  ...........
  ============================
   n<d/\n=d[x]zero[+]n

\end{verbatim}

\textit{Example 2}

\begin{verbatim}
1 subgoal
  ..................
  ============================
   X =c A\/(EXT A'|X==A' u {x}/\A' =c A)

Included_Add < Take (X-{x}) 
               and prove (X==(X-{x}) u {x}/\(X-{x}) =c A). 

1 subgoal
  ..................
  ============================
   X==(X-{x}) u {x}/\(X-{x}) =c A

\end{verbatim}

The order that we put two \notion{formula}-arguments, must be the same as
the order of the corresponding predicates in the existential statement. 

\vspace{0.5cm}

\paragraph{The implementation:}\

\vspace{0.5cm}

\key{Take} performs 3 steps.

\begin{itemize}

\item
First it tries to apply \key{Red}. Therefore the user can also apply
\key{Take} to a goal which is not an explicit existential statement.

\item
Then the tactic `\key{Apply} \notion{term1} \key{with} \notion{term2}'
is applied. As the \notion{term1} the constructors of the existential 
statements are used. The tactic is applied repeatedly until it succeeds.
Every time
another constructor is put. As \notion{term2} the \notion{formula} is put.

\item
At the end `\key{Change} \notion{formula}' is applied. It is to check
whether the user put the right argument for \notion{formula}
\end{itemize}

It is possible to apply \key{Take} to a disjunction statement that includes
an existential statement. In that case \key{Take} is applied one after 
another to every formula in this disjunction until it comes to this 
existential formula. If there is more than one existential statement
in a goal then it depends on the parameter \notion{formula} to which 
existential statement \key{Take} will be applied successfully.

For example, the goal is a disjunction of the form:

\begin{alltt}
A1 \$/ A2 \$/ ... \$/ (EX x:T | (P x)) \$/ (EX x:T | (Q x)) \$/ ... \$/ An\negspace
\end{alltt}

Then
`\texttt{Take} \notion{var} \texttt{and prove (P} \notion{var} \texttt{)}'
will succeed on applying to\hfill\break\mbox{\texttt{(EX x:T | (P x))}} and
`\texttt{Take} \notion{var} \texttt{and prove (Q} \notion{var} \texttt{)}'
will succeed on applying to \mbox{\texttt{(EX x:T | (Q x))}} 

\subsection{proving by cases}

\begin{flushleft}
\qkey{First} \qkey{case} \notion{formula}  
[ \punct{(} \notion{label} \punct{)} ] \punct{.} \\
\notion{proof} \\
\{ \qkey{Next} \qkey{case} \notion{formula} [ \punct{(} \notion{label} 
\punct{)} ] \punct{.} \notion{proof} \} \\
 \qkey{End\_cases} [ \punct{[} \notion{tactic} \punct{]} ]
 \punct{.}
\end{flushleft}


We start to prove by cases with the tactic \key{First case}. This tactic adds
\notion{formula} to the local context with the label \notion{label}.
It also generates another subgoal
that is a disjunction statement of the \notion{formula} and the first subgoal.
For example:

\begin{alltt}

  P := [n:nat]O<n->(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<n->(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<n->(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<n->(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<n->(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<n)->(EX L:ListN |((allprimes L)/\$(n=(Prod L)))).
Proof.
  LetTac P :=[n:nat](O<n)->(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)<pp)/\$(s[x]pp)=n)) (A4).
    Claim  (x<n)/\$((O)<x) (A11).
      Have (pp[x]x)=n (A9) [by times_com, A4]. 
      Then n=(pp[x]x) (A7).
      Have (prime pp) [by A5].
      Then  one<pp.
    Hence (x<n) [by A7, A6, propprod_propfact].
      Claim (~x=O).
        Assume (x = O) (A8).
        Have (O = (x [x] pp)) [by A8].
               _= n [by A9, times_com].
        Then (O < O) [by A6]. 
        Hence thesis [by not_lt_zero].
      End_claim.
    Hence ((O) < x) [by neq_zero_imp_gt_zero].
    End_claim.
    Then (P x) (A12) [by A10].
    Have ((O)<x)  [by A11]. 
    Then consider LL such that 
      [LL:ListN] (allprimes LL)/\$x=(Prod LL) (A13) [by A12].
    Have (prime pp) [by A5].
    Then (allprimes (cons pp LL)) (A14) [by A13].
    Have (n = (x [x] pp)) (A15) [by A4, eq_sym].
           _= (Prod (cons pp LL))  [by A13, times_com].
    Take (cons pp LL) and prove 
          ((allprimes (cons pp LL))/\$n=(Prod (cons pp LL))).
  Thus thesis [by A14, A15].
  End_cases [by prime_dec].
End_claim.
Show_ (n:nat)(P n).
Thus thesis [by A16,cv_ind].
Qed.
\end{alltt}

\subsection{Example of a CMode proof}

The third one is a proof of the Fundamental Theorem of Algebra.
The original proof comes from the C-CoRN library.
In two places there is
\texttt{Let\char`\_\ f be (cs\char`\_crr (cpoly\char`\_cring CC))} instead of
\texttt{Let\char`\_\ f be (cpoly\char`\_cring CC)}. The reason was that 
\texttt{Change (cpoly\char`\_cring CC) in f}, which is called by \key{Let\_}
after \texttt{Intro f} (see~\ref{mlet}), fails because it does not
insert the relevant coercion.

Another thing is that in one of the last steps of the proof
the label \textit{Hrecn}, that is not present in the proof script, is used
as a reference. This label refers to the induction hypothesis:

\begin{verbatim}
  Hrecn : (f:(cpoly_cring CC))
           (degree_le n f)->(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<n)->(EX L:ListN |((allprimes L)/\$(n=(Prod L)))).
Proof. 
  LetTac  P :=[n:nat](O<n)->(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)<n).
      We have [by A1]

               (allprimes (cons n nil)) (A2).

      Also 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))).     
      Then we are done [by A2 , A3].
    Case 2 ~(prime n).
      Assume ((O) < n) (A4). 
      Have  (HPD n) [by nat_HPD].
      Now choose pp such that 

              ([pp:nat] (primediv pp n)) (A5).

      Then (pp [|] n). 
      Now  choose x such that 

               ([s:nat](((O)<pp)/\$(s[x]pp)=n)) (A7). 

      Claim  (x<n)/\$((O)<x) (A8).
        First we have (pp[x]x)=n (A8) [by times_com , A7]. 
        So n=(pp[x]x) (A9). 
        We have (prime pp) [by A5].
        Then  one<pp.
        Hence (x<n) [by A9 ,  A4  , propprod_propfact].

        Secondly claim (~x=O).
          Indeed assume (x = O) (A10).

          Claim O=n.
            So ((x [x] pp)=O) (A11) [by A10].
            Also ((x[x]pp)=n) [by A8 , times_com].
          Hence we have our claim [by A11].
        Then (O < O) [by A4].

        Hence claim done [by not_lt_zero].
      Hence ((O) < x) [by neq_zero_imp_gt_zero].

      Now [by A8, IH] we have 

               (P x) (A12).

      Then [by A8]

               (EX L:ListN |((allprimes L)/\$(x=(Prod L)))) (A13).

      Now choose LL such that 
   
              [LL:ListN] (allprimes LL)/\$x=(Prod LL) (A14).

      We have (prime pp) [by A5].
      Also  (allprimes (cons pp LL)) (A15) [by A14]. 
      We have 

               ((Prod LL)[x]pp)=(pp[x](Prod LL)) [by times_com].

      Hence [by A14] again (x[x]pp) = (pp[x](Prod LL)) (A17).
      We have (n = (x [x] pp)) [by A7 , eq_sym]. 
      Therefore [by A17]  (n=(Prod (cons pp LL))) (A16).
      Finally take (cons pp LL) 
            and prove (allprimes (cons pp LL))/\$n=(Prod (cons pp LL)).     
    So we are done [by A15, A16]. 
  End_cases [by prime_dec].
Qed.
\end{alltt}


\section{Conclusion} % first version: Freek

\subsection{Discussion}

The MMode system is a rather complete Mizar mode for Coq:
it emulates all Mizar proof steps.
However, currently it is just a prototype.
It has just been developed enough to process the five example proofs.
We would expect that for the next few proofs it will still need to be
extended significantly.
For instance, the \key{by} tactic only has been implemented
for at most three references (in the real Mizar system there are
\key{by} justifications with tens of references).
This shows that at the moment the system is just a proof of concept.

We will now compare the efficiency of MMode proofs as
compared to `old style' Coq proofs:

\begin{itemize}
\item
Our MMode proofs are approximately twice as long as the corresponding Coq
proofs.
There are two reasons for this.
The Coq proof does not contain the statements of the proof states,
while the MMode proof does.
Also, the MMode proof text is indented
so it contains much more whitespace.

Surprisingly, the MMode version of a Mizar proof is longer too.
The MMode version of \url{min_abs} is about three times as long
as the Mizar original.
The main reason for this is that the C-CoRN notation used in the
Coq version of the Mizar statements is much clumsier
than the original Mizar notation.

\item
Our MMode proofs take approximately three times as much time
to check as the corresponding Coq proofs.
This is all caused by the fact that we generate the justifications
with the \key{by} tactic.
The proofs where the justifications have been `expanded'
(in \url{other/expanded_by/}) are only
slightly slower than the originals.

The use of \key{by} slows checking for two reasons.
First, it takes time for it to find the proof.
Second, the proof it finds generally is less efficient than a proof
found manually.

\emph{Bold claim:}
We expect that there is room for improvement in the performance
of \key{by}.
The current version in MMode is really just a first experimental version.

\item
The MMode proof terms are less than twice as large as the corresponding
Coq proof terms.
(We looked at the size of the \url{.vo} files to judge the size of
the proof terms.)

This difference is even less when considering the $\beta$-normal forms
of the proof terms.
MMode proofs contain many more cuts than traditional Coq proofs.
This is one of the main reasons for the increase in the size of the proof terms.

Another reason, again, is that \key{by} will not always find as efficient a
proof as a human will.

\end{itemize}
\noindent
All in all we can summarize that using MMode probably imposes a performance
penalty -- both in space and time -- of about a factor of two.
We expect that when we develop MMode, there will be some space for improvement,
mainly in the time dimension.
However we do not expect that MMode proofs will ever be as small and fast as
old style Coq proofs.

This can be compared to writing programs in assembly
versus using a high level language like C.
In assembly a program will be faster and will use less resources.
However, this is not always a good reason to program in assembly.

\subsection{Future work}

Most importantly, the MMode system needs to be turned into more
than a prototype.
For this, two things are essential:

\begin{itemize}
\item
MMode needs to be ported to the latest versions of Coq and C-CoRN
(at the time of writing this report, the latest version of Coq is still
version 7.4 but C-CoRN already has been modified to work with a more recent
`CVS version' of Coq).

\item
MMode needs to be used for a significant `proof development', a
formalization of a non-trivial piece of mathematics.

\end{itemize}

\noindent
Then, there are some issues of a more theoretical character:

\begin{itemize}
\item
The current version of MMode is very Coq specific.
It would be nice to give a more system independent and more theoretically
oriented description of the meaning of the MMode steps.

\item
It is an interesting question whether the given implementation of \key{by}
in MMode is \emph{complete}.
The question then, is whether it is possible to prove any Coq theorem
when only using the MMode tactics (where only variables are used
for the references after the \key{by} tactic).

\end{itemize}

\noindent
The syntax of MMode is currently rather restricted, mainly due to our decision
only to use Coq's \texttt{Grammar} rules to implement it.
There is room for improvement here:

\begin{itemize}
\item
The tactics in the Appendix on page~\pageref{appendix} only give a small
sub-language of the syntax from Section~\ref{mmodegrammar} on page~\pageref{mmodegrammar}.
Many more instances of the steps in this grammar
should be implemented as tactics.
For instance there should be \key{by} tactics with more than
three arguments, \key{Let\_} tactics that
bind more than two variables, and so on.

Alternatively we might look into having a MMode parser that is not just
built using \texttt{Grammar} rules.
If we do this, the MMode system will be harder to install and it will not work in
all Coq environments anymore.
But on the other hand, the full grammar from Section~\ref{mmodegrammar} might
be available then.
Also the keywords \key{Let\_} and \key{Show\_} would not need an underscore
anymore, but could just be \key{Let} and \key{Show}.

\item
There should be more serious investigation of synonyms for MMode steps,
as described in Section~\ref{synon}.
It might be interesting to take an existing mathematical text (Henk
Barendregt calls this `best mathematical style'), and
collect statistics on what wordings are actually used for the various kinds of
MMode steps.

\item
Combinations of MMode tactics could be given syntax of their
own.
For instance Mizar's \key{Given} ($=$ \key{Assume} $+$ \key{Consider})
or \key{Let} \key{\dots} \key{such} \key{that} ($=$ \key{Let} $+$ \key{Assume})
could be implemented.
Another possibility might be to implement an \key{Otherwise} tactic:
the step \key{Otherwise} $P$ then would be an abbreviation of \key{Assume} \url{~}\emph{thesis}\texttt{;} \key{Then} $P$.

\end{itemize}

\noindent
The tactics of MMode also can use improvements:

\begin{itemize}
\item
When using the Sketch variant of MMode, the error messages
for steps that have not been sufficiently justified just appear in the
contexts.
This means that when compiling a file with \texttt{coqc} there will
be no feedback about those errors.
Currently it is not possible to produce appropriate error messages
without going to the ML level in the implementation of the tactics
(we decided we did not want to do this).
In the next version of Coq having proper error messages in the Sketch mode
probably will be possible without programming on the ML level.

\item
The \key{by} tactic in its current form probably is (a) too weak
and (b) too inefficient.
It should be refined to find a proof faster, find more efficient
proofs and find proofs in more cases.
(It is not clear to us whether going to the ML level for the implementation
of the \key{by} tactic would help with this.)

\item
It would be useful if \key{by} could print the proof it finds.
(This is similar to the \key{Info} tactical of Coq.)

\item
The \key{by} tactic currently does two things.
It builds a restricted context that just contains the arguments
of the tactic.
Then it searches for a proof in this context with \key{GAuto}.
Separating these two parts might make it possible to substitute
other automated proof tactics for \key{GAuto} but keep the property
that only the arguments of the tactic can be used by it.

\item
The \key{by} tactic currently only takes references and tactics.
It would be useful to extend this with \key{Hints} classes.

\item
The `trick' of \key{End\_claim} to have the same subgoal twice
(to `remember' what subproof one is working on) might be modified.
For instance the second subgoal could be different, to make it
more obvious that this is just a reminder of a subproof that needs
to be closed, instead of a statement that really needs a proof
of itself.

\end{itemize}

\noindent
Finally an interesting topic is to investigate whether it
is possible to automatically convert an existing `old style'
Coq proof script into an MMode proof.
Of course we do not think that this would be a better way of getting
MMode proofs than
writing them directly.
However, it might be interesting to see whether one could use
MMode as a `proof presentation language' for existing `legacy' Coq proofs.
This would be closely related to the work on generating proof presentations
from Coq tactic proof scripts by Fr\'ed\'erique Guilhot, Hanane Naciri and Lo{\"\i}c Pottier (they do not have a publication about it yet).

Related to this is the question whether it is possible to support the
writing of MMode proofs with some automation.
For instance, most MMode proofs start with a couple of \key{Let\_} and \key{Assume}
steps that really are determined by the statement that one is proving.
In traditional Coq proofs one only needs to write \key{Intros} for this.
It should be possible to have a command that inserts
these \key{Let\_} and \key{Assume} steps automatically into the proof text.
Henk Barendregt calls this kind of automatic support for the writing of
MMode proofs
\emph{luxury} MMode.

A naive way to translate a traditional proof script into an MMode proof is to convert the Coq \emph{proof term} that
is constructed by the proof script
to an MMode proof, but we do not think this is the best way.
A better approach probably is to `merge' all subgoals that the
tactic script goes through into an MMode proof skeleton.
Probably that would give an MMode proof of which not all the
justifications can be done by \key{by},
but it would be a good starting point for a human to produce
a working MMode proof.

\paragraph{Acknowledgments.}

We especially would like to thank Henk Barendregt for his enthusiasm for what
he calls `mathmode'.
Thanks also to Dan Synek and Iris Loeb
for their comments on draft versions of this document.
Further thanks for all the help we got from
Lu{\'\i}s Cruz-Filipe,
Herman Geuvers,
Milad Niqui,
Bas Spitters and
Jasper Stein.
Finally many thanks to Hugo Herbelin who showed us how to get Coq to do what
we wanted it to do.

The first author of this report was financed as a young researcher
under European Community contract nr.~HPRN-CT-2000-00102, in the
thematic network CALCULEMUS, Systems for Integrated Computation and Deduction.


\bibliographystyle{plain}
\bibliography{mmode}


\appendix
\section{The implemented MMode tactics}
\label{appendix}

We now list all MMode tactics that have been implemented thus far.
These tactics give a sub-language of the proof language of the
grammar on page~\pageref{mmodegrammar} in Section~\ref{mmodegrammar}.

\subsection{\key{by}}

\begin{flushleft}
\qkey{by} \notion{ref} \\
\qkey{by} \notion{ref} \punct{,} \notion{ref} \\
\qkey{by} \notion{ref} \punct{,} \notion{ref} \punct{,} \notion{ref}
\end{flushleft}

\begin{flushleft}
\setbox0=\hbox{\qkey{by} \notion{ref} \punct{,} \notion{ref} \punct{,} \notion{ref}}
\strut\rlap{\qkey{by} \notion{ref}}\hspace{\wd0} \qkey{with} \notion{tactic} \\
\strut\rlap{\qkey{by} \notion{ref} \punct{,} \notion{ref}}\hspace{\wd0} \qkey{with} \notion{tactic} \\
{\unhcopy0} \qkey{with} \notion{tactic}
\end{flushleft}

\subsection{\key{Let\_}/\key{Assume}}

\begin{flushleft}
\setbox0=\hbox{\qkey{Let\_} \notion{var} \punct{,} \notion{var}}
\strut\rlap{\qkey{Let\_} \notion{var}}\hspace{\wd0} \qkey{be} \notion{type} \\
{\unhcopy0} \qkey{be} \notion{type} \\
{\unhcopy0} \qkey{be} \notion{type} \qkey{and} \notion{var} \qkey{be} \notion{type} \\
\strut\rlap{\qkey{Let\_} \notion{var}}\hspace{\wd0} \qkey{be} \notion{type} \rlap{\punct{,}}\phantom{\qkey{and}} \notion{var} \qkey{be} \notion{type}
\end{flushleft}

\begin{flushleft}
\setbox0=\hbox{\qkey{Assume} \notion{formula} \punct{(} \notion{label} \punct{)}}
\qkey{Assume} \notion{formula} \\
\strut\rlap{\qkey{Assume} \notion{formula}}\hspace{\wd0} \qkey{and} \notion{formula} \\
{\unhcopy0} \\
{\unhcopy0} \qkey{and} \notion{formula}
\end{flushleft}

\subsection{\key{Have}/\key{Then}}

\begin{flushleft}
\setbox0=\hbox{\qkey{Have} \notion{formula} \punct{(} \notion{label} \punct{)}}
\strut\rlap{\qkey{Have} \notion{formula}}\hspace{\wd0} \punct{[} \notion{tactic} \punct{]} \\
{\unhcopy0} \punct{[} \notion{tactic} \punct{]} \\
\strut\qkey{Have} \notion{formula} \\
{\unhcopy0}
\end{flushleft}

\begin{flushleft}
\setbox0=\hbox{\qkey{Then} \notion{formula} \punct{(} \notion{label} \punct{)}}
\strut\rlap{\qkey{Then} \notion{formula}}\hspace{\wd0} \punct{[} \notion{tactic} \punct{]} \\
{\unhcopy0} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Then} \notion{formula} \\
{\unhcopy0}
\end{flushleft}

\subsection{Iteration}

\begin{flushleft}
\strut\phantom{\qkey{Thus}} \phantom{\punct{\char`\_[=]}}\llap{\punct{\char`\_=}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\strut\phantom{\qkey{Thus}} \rlap{\punct{=\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\strut\phantom{\qkey{Thus}} \punct{\char`\_[=]} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\strut\phantom{\qkey{Thus}} \rlap{\punct{[=]\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\strut\phantom{\qkey{Thus}} \punct{\char`\_[=]} \notion{term} \\
\strut\phantom{\qkey{Thus}} \rlap{\punct{[=]\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term} \\
\qkey{Thus} \phantom{\punct{\char`\_[=]}}\llap{\punct{\char`\_=}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Thus} \rlap{\punct{=\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Thus} \rlap{\punct{\char`\_[=]}}\phantom{\punct{\char`\_[=]}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Thus} \rlap{\punct{[=]\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Thus} \rlap{\punct{\char`\_[=]}}\phantom{\punct{\char`\_[=]}} \notion{term} \\
\qkey{Thus} \rlap{\punct{[=]\char`\_}}\phantom{\punct{\char`\_[=]}} \notion{term}
\end{flushleft}

\subsection{\key{Claim}/\key{Thus}}

\begin{flushleft}
\qkey{Claim} \notion{formula} \\
\qkey{Claim} \notion{formula} \punct{(} \notion{label} \punct{)} \\
\qkey{End\_claim}
\end{flushleft}

\begin{flushleft}
\strut\rlap{\qkey{Thus}}\phantom{\qkey{Hence}} \rlap{\qkey{thesis}}\phantom{\notion{formula}} \punct{[} \notion{tactic} \punct{]} \\
\strut\qkey{Hence} \rlap{\qkey{thesis}}\phantom{\notion{formula}} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Hence} \qkey{thesis}
\end{flushleft}

\begin{flushleft}
\strut\rlap{\qkey{Thus}}\phantom{\qkey{Hence}} \notion{formula} \punct{[} \notion{tactic} \punct{]} \\
\qkey{Hence} \notion{formula} \punct{[} \notion{tactic} \punct{]}
\end{flushleft}

\subsection{\key{Consider}}

\begin{flushleft}
\strut\phantom{\qkey{Then}} \qkey{Consider} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \phantom{\punct{(} \notion{label} \punct{)}} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
\strut\phantom{\qkey{Then}} \qkey{Consider} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \phantom{\punct{(} \notion{label} \punct{)}} \\
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \\
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \phantom{\punct{(} \notion{label} \punct{)}} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
\end{flushleft}

\begin{flushleft}
\strut\phantom{\qkey{Then}} \qkey{Consider} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \\
\strut\phantom{\qkey{Then} \qkey{Consider} \notion{var} \qkey{such} \qkey{that}}\llap{\qkey{and}} \notion{bound-formula} \phantom{\punct{(} \notion{label} \punct{)}} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
%\medskip
\strut\phantom{\qkey{Then}} \qkey{Consider} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)}\\
\strut\phantom{\qkey{Then} \qkey{Consider} \notion{var} \qkey{such} \qkey{that}}\llap{\qkey{and}} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \rlap{\punct{[} \notion{tactic} \punct{]}} \\
%\medskip
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)}\\
\strut\phantom{\qkey{Then} \qkey{Consider} \notion{var} \qkey{such} \qkey{that}}\llap{\qkey{and}} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \\
%\medskip
\qkey{Then} \rlap{\qkey{consider}}\phantom{\qkey{Consider}} \notion{var} \qkey{such} \qkey{that} \notion{bound-formula} \punct{(} \notion{label} \punct{)}\\
\strut\phantom{\qkey{Then} \qkey{Consider} \notion{var} \qkey{such} \qkey{that}}\llap{\qkey{and}} \notion{bound-formula} \punct{(} \notion{label} \punct{)} \rlap{\punct{[} \notion{tactic} \punct{]}}
\end{flushleft}

\subsection{\key{Take}}

\begin{flushleft}
\qkey{Take} \notion{term} \qkey{and} \qkey{prove} \notion{formula} \\
\qkey{Take} \notion{term} \qkey{and} \qkey{prove} \notion{formula} \qkey{and} \notion{formula}
\end{flushleft}

\subsection{Per cases}

\begin{flushleft}
\strut\rlap{\qkey{First}}\phantom{\qkey{Next}} \qkey{case} \notion{formula} \punct{(} \notion{label} \punct{)} \\
\strut\rlap{\qkey{First}}\phantom{\qkey{Next}} \qkey{case} \notion{formula} \\
\qkey{Next} \qkey{case} \notion{formula} \punct{(} \notion{label} \punct{)} \\
\qkey{Next} \qkey{case} \notion{formula} \\
\qkey{End\_cases} \punct{[} \notion{tactic} \punct{]}
\end{flushleft}

\subsection{\key{Show\_}}

\begin{flushleft}
\qkey{Show\_} \notion{formula}
\end{flushleft}

\end{document}
