1 files changed, 291 insertions, 0 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
new file mode 100755
index 000000000..c9bc4e4d9
--- /dev/null
+++ b/doc/RefMan-pro.tex
@@ -0,0 +1,291 @@
+\chapter{Proof handling}
+\index{Proof editing}
+\label{Proof-handling}
+
+In \Coq's proof editing mode all top-level commands documented in 
+chapter \ref{Vernacular-commands} remain available
+and the user has access to specialized commands dealing with proof
+development pragmas documented in this section. He can also use some
+other specialized commands called {\em tactics}.  They are the very
+tools allowing the user to deal with logical reasoning. They are
+documented in chapter \ref{Tactics}.\\ 
+When switching in editing proof mode, the prompt
+\index{Prompt} 
+{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
+declared name of the theorem currently edited.
+
+At each stage of a proof development, one has a list of goals to
+prove. Initially, the list consists only in the theorem itself. After
+having applied some tactics, the list of goals contains the subgoals
+generated by the tactics.
+
+To each subgoal is associated  a number of
+hypotheses we call the {\em \index*{local context}} of the goal.
+Initially, the local context is empty. It is enriched by the use of
+certain tactics (see mainly section \ref{Intro}).
+
+When a proof is achieved the message {\tt Subtree proved!} is
+displayed. One can then store this proof as a defined constant in the
+environment. Because there exists a correspondence between proofs and
+terms of $\lambda$-calculus, known as the {\em Curry-Howard
+isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
+terms of {\sc Cic}. Those terms are called {\em proof
+  terms}\index{Proof term}.
+
+It is possible to edit several proofs at the same time: see section
+\ref{Resume}
+
+\ErrMsg When one attempts to use a proof editing command out of the
+proof editing mode, \Coq~ raises the error message : {\tt No focused
+  proof}.
+
+\section{Switching on/off the proof editing mode}
+
+\subsection{\tt Goal {\form}.}
+\comindex{Goal}\label{Goal}
+This command switches \Coq~ to editing proof mode and sets {\form} as
+the original goal. It associates the name {\tt Unnamed\_thm} to
+that goal.
+
+\begin{ErrMsgs}
+\item \errindex{Proof objects can only be abstracted}
+\item \errindex{A goal should be a type}
+\item \errindex{repeated goal not permitted in refining mode}
+\end{ErrMsgs}
+
+\SeeAlso section \ref{Theorem}
+
+\subsection{\tt Qed.}\comindex{Qed}\label{Qed}
+This command is available in interactive editing proof mode when the
+proof is completed.  Then {\tt Qed} extracts a proof term from the
+proof script, switches back to {\Coq} top-level and attaches the
+extracted proof term to the declared name of the original goal. This
+name is added to the environment as an {\tt Opaque} constant.
+
+\begin{ErrMsgs}
+\item \errindex{Attempt to save an incomplete proof}
+\item \errindex{Clash with previous constant ...}\\ 
+  The implicit name is already defined. You have then to provide
+  explicitly a new name (see variant 2 below).
+\item Sometimes an error occurs when building the proof term,
+because tactics do not enforce completely the term construction
+constraints.
+
+The user should also be aware of the fact that since the proof term is
+completely rechecked at this point, one may have to wait a while when
+the proof is large. In some exceptional cases one may even incur a
+memory overflow.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Save.}\comindex{Save}\
+  Is equivalent to {\tt Qed}.
+\item {\tt Save {\ident}.}\\
+  Forces the name of the original goal to be {\ident}.
+\item {\tt Save Theorem {\ident}.} \\
+  Is equivalent to {\tt Save {\ident}.}
+\item {\tt Save Remark {\ident}.}\\
+  Defines the proved term as a local constant that will not exist
+  anymore after the end of the current section.
+\item {\tt Defined.}\comindex{Defined} \label{Defined} \\
+  Defines the proved term as a transparent constant.
+\end{Variants}
+
+\subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem}
+This command switches to interactive editing proof mode and declares
+{\ident} as being the name of the original goal {\form}. When declared
+as a {\tt Theorem}, the name {\ident} is known at all section levels:
+{\tt Theorem} is a {\sl global} lemma.
+
+\ErrMsg (see section \ref{Goal})
+
+\begin{Variants}
+\item {\tt Lemma {\ident} : {\form}.}\comindex{Lemma}\\
+  It is equivalent to {\tt Theorem {\ident} : {\form}.}
+\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
+  Analogous to {\tt Theorem} except that {\ident} will be unknown
+  after closing the current section. All proofs of persistent objects
+  (such as theorems) referring to {\ident} within the section will be
+  replaced by the proof of {\ident}.  
+\item {\tt Fact {\ident} : {\form}.}\comindex{Fact}\\
+  Analogous to {\tt Theorem} except that {\ident} is known after
+  closing the current section but 
+ will be unknown  after closing the section which is above the current section.
+\item {\tt Definition {\ident} : {\form}.}
+\comindex{Definition}\\
+  Analogous to {\tt Theorem}, intended to be used in conjunction with
+  {\tt Defined} (see \ref{Defined}) in order to define a
+  transparent constant.
+\end{Variants}
+
+\subsection{\tt Proof {\term}.}\comindex{Proof}
+This command applies in proof editing mode. It is equivalent to {\tt
+  Exact {\term}; Save.} That is, you have to give the full proof in
+one gulp, as a proof term (see section \ref{Exact}).
+
+\begin{Variants}
+\item{\tt Proof.} is a noop which is useful to delimit the sequence of
+tactic commands which start a proof, after a {\tt Theorem} command.
+It is a good practice to use {\tt Proof.} as an opening parenthesis,
+closed in the script with a closing {\tt Qed.}
+\end{Variants}
+
+\subsection{\tt Abort.}\comindex{Abort}
+This command cancels the current proof development, switching back to
+the previous proof development, or to the \Coq\ toplevel if no other
+proof was edited.
+
+\begin{ErrMsgs}
+\item \errindex{No focused proof}\texttt{ (No proof-editing in progress)}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Abort {\ident}.}\\
+  Aborts the editing of the proof named {\ident}.
+\item {\tt Abort All.}\\
+  Aborts all current goals, switching back to the \Coq\ toplevel.
+\end{Variants}
+
+\subsection{\tt Suspend.}\comindex{Suspend}
+This command applies in proof editing mode. It switches back to the
+\Coq\ toplevel, but without canceling the current proofs.
+
+\subsection{\tt Resume.}
+\comindex{Resume}\label{Resume}
+This commands switches back to the editing of the last edited proof.
+
+\begin{ErrMsgs}
+\item \errindex{No proof-editing in progress}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Resume {\ident}.}\\
+  Restarts the editing of the proof named {\ident}. This can be used
+  to navigate between currently edited proofs.
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{No such proof}
+\end{ErrMsgs}
+
+\section{Navigation in the proof tree}
+
+\subsection{\tt Undo.}\comindex{Undo}
+This command cancels the effect of the last tactic command.  Thus, it
+backtracks one step.
+
+\begin{ErrMsgs}
+\item \errindex{No focused proof (No proof-editing in progress)}
+\item \errindex{Undo stack would be exhausted}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Undo {\num}.}\\
+  Repeats {\tt Undo} {\num} times.
+\end{Variants}
+
+\subsection{\tt Set Undo {\num}.}\comindex{Set Undo}
+This command changes the maximum number of {\tt Undo}'s that will be
+possible when doing a proof. It only affects proofs started after
+this command, such that if you want to change the current undo limit
+inside a proof, you should first restart this proof.
+
+\subsection{\tt Unset Undo.}\comindex{Unset Undo}
+This command resets the default number of possible {\tt Undo} commands
+(which is currently 12).
+
+\subsection{\tt Restart.}\comindex{Restart}
+This command restores the proof editing process to the original goal.
+
+\begin{ErrMsgs}
+\item \errindex{No focused proof to restart}
+\end{ErrMsgs}
+
+\subsection{\tt Focus.}\comindex{Focus}
+Will focus the attention on the first subgoal to prove, the remaining
+subgoals will no more be printed after the application of a tactic.
+This is useful when there are many current subgoals which clutter your
+screen.
+
+\subsection{\tt Unfocus.}\comindex{Unfocus}
+Turns off the focus mode.
+
+
+\section{Displaying information}
+
+\subsection{\tt Show.}\comindex{Show}\label{Show}
+This command displays the current goals.
+
+\begin{Variants}
+\item {\tt Show {\num}.}\\ 
+  Displays only the {\num}-th subgoal.\\ 
+\begin{ErrMsgs}
+\errindex{No such goal}
+\errindex{No focused proof}
+\end{ErrMsgs}
+
+\item {\tt Show Implicits.}\comindex{Show Implicits}\\
+  Displays the current goals, printing the implicit arguments of
+  constants.
+
+\item {\tt Show Implicits {\num}.}\\
+  Same as above, only displaying the {\num}-th subgoal.
+
+\item {\tt Show Script.}\comindex{Show Script}\\
+  Displays the whole list of tactics applied from the beginning
+  of the current proof. 
+  This tactics script may contain some holes (subgoals not yet proved).
+  They are printed as \verb!<Your Tactic Text here>!.
+
+\item {\tt Show Tree.}\comindex{Show Tree}\\
+This command can be seen as a more structured way of
+displaying the state of the proof than that 
+provided by {\tt Show Script}. Instead of just giving
+the list of tactics that have been applied, it 
+shows the derivation tree constructed by then. 
+Each node of the tree contains the conclusion
+of the corresponding sub-derivation (i.e. a
+goal with its corresponding local context) and 
+the tactic that has generated all the 
+sub-derivations. The leaves of this tree are
+the goals which still remain to be proved.
+
+%\item {\tt Show Node}\comindex{Show Node}\\
+%        Not yet documented
+
+\item {\tt Show Proof.}\comindex{Show Proof}\\
+It displays the proof term generated by the 
+tactics that have been applied. 
+If the proof is not completed, this term contain holes,
+which correspond to the sub-terms which are still to be 
+constructed. These holes appear as a question mark indexed 
+by an integer, and applied to the list of variables in 
+the context, since it may depend on them. 
+The types obtained by abstracting away the context from the
+type of each hole-placer are also printed.
+
+\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
+It prints the list of the names of all the theorems that 
+are currently being proved.
+As it is possible to start proving a previous lemma during
+the proof of a theorem, this list may contain several 
+names. 
+\end{Variants}
+
+\subsection{\tt Set Hyps\_limit {\num}.}
+\comindex{Set Hyps\_limit}
+This command sets the maximum number of hypotheses displayed in
+goals after the application of a tactic. 
+All the hypotheses remains usable in the proof development.
+
+\subsection{\tt Unset Hyps\_limit.}
+\comindex{Unset Hyps\_limit}
+This command goes back to the default mode which is to print all
+available hypotheses.
+
+% $Id$
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: