[Sphinx] Move chapter 7 to new infrastructure

1 files changed, 581 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
new file mode 100644
index 0000000000..eb3a24a2bd
--- /dev/null
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -0,0 +1,581 @@
+\chapter[Proof handling]{Proof handling\index{Proof editing}
+\label{Proof-handling}}
+%HEVEA\cutname{proof-handling.html}
+
+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 called the {\em \index*{local context}} of the goal.
+Initially, the local context contains the local variables and
+hypotheses of the current section (see Section~\ref{Variable}) and the
+local variables and hypotheses of the theorem statement.  It is
+enriched by the use of certain tactics (see e.g. {\tt intro} in
+Section~\ref{intro}).
+
+When a proof is completed, the message {\tt Proof completed} is
+displayed. One can then register 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}.
+
+\ErrMsg When one attempts to use a proof editing command out of the
+proof editing mode, \Coq~ raises the error message : \errindex{No focused
+  proof}.
+
+\section{Switching on/off the proof editing mode}
+
+The proof editing mode is entered by asserting a statement, which
+typically is the assertion of a theorem:
+
+\begin{quote}
+{\tt Theorem {\ident} \zeroone{\binders} : {\form}.\comindex{Theorem}
+\label{Theorem}}
+\end{quote}
+
+The list of assertion commands is given in
+Section~\ref{Assertions}. The command {\tt Goal} can also be used.
+
+\subsection[Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}
+
+This is intended for quick assertion of statements, without knowing in
+advance which name to give to the assertion, typically for quick
+testing of the provability of a statement. If the proof of the
+statement is eventually completed and validated, the statement is then
+bound to the name {\tt Unnamed\_thm} (or a variant of this name not
+already used for another statement).
+
+\subsection[\tt Qed.]{\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 \ident\ \errindex{already exists}\\
+%  The implicit name is already defined. You have then to provide
+%  explicitly a new name (see variant 3 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 Defined.}
+\comindex{Defined}
+\label{Defined}
+
+  Defines the proved term as a transparent constant.
+
+\item {\tt Save {\ident}.}
+
+  Forces the name of the original goal to be {\ident}.  This command
+  (and the following ones) can only be used if the original goal has
+  been opened using the {\tt Goal} command.
+
+\end{Variants}
+
+\subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
+This command is available in interactive editing proof mode to give up
+the current proof and declare the initial goal as an axiom.
+
+\subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
+\label{BeginProof}}
+This command applies in proof editing mode. It is equivalent to {\tt
+  exact {\term}. Qed.} That is, you have to give the full proof in
+one gulp, as a proof term (see Section~\ref{exact}).
+
+\variant {\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.}
+
+\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
+
+\subsection[{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}]
+{{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}
+\comindex{Proof using} \label{ProofUsing}}
+
+This command applies in proof editing mode.
+It declares the set of section variables (see~\ref{Variable})
+used by the proof. At {\tt Qed} time, the system will assert that
+the set of section variables actually used in the proof is a subset of
+the declared one.
+
+The set of declared variables is closed under type dependency.
+For example if {\tt T} is variable and {\tt a} is a variable of
+type {\tt T}, the commands {\tt Proof using a} and
+{\tt Proof using T a} are actually equivalent.
+
+\variant {\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$} {\tt with} {\tac}{\tt .}
+in Section~\ref{ProofWith}.
+
+\variant {\tt Proof using All.}
+
+  Use all section variables.
+
+\variant {\tt Proof using Type.}
+\variant {\tt Proof using.}
+
+  Use only section variables occurring in the statement.
+
+\variant {\tt Proof using Type*.}
+
+  The {\tt *} operator computes the forward transitive closure.
+  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+  {\tt Type* } is the forward transitive closure of the entire set of
+  section variables occurring in the statement.
+
+\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
+
+  Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
+
+\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
+
+\variant {\tt Proof using \nterm{collection} * .}
+
+  Use section variables being, respectively, in the set union, set difference,
+  set complement, set forward transitive closure.
+  See Section~\ref{Collection} to know how to form a named
+  collection.
+  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
+
+\subsubsection{{\tt Proof using} options}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+% \optindex{Proof Using Clear Unused}
+
+The following options modify the behavior of {\tt Proof using}.
+
+\variant {\tt Set Default Proof Using "expression".}
+
+  Use {\tt expression} as the default {\tt Proof using} value.
+  E.g. {\tt Set Default Proof Using "a b".} will complete all {\tt Proof }
+  commands not followed by a {\tt using} part with {\tt using a b}.
+
+\variant {\tt Set Suggest Proof Using.}
+
+  When {\tt Qed} is performed, suggest a {\tt using} annotation if
+  the user did not provide one.
+
+% \variant{\tt Unset Proof Using Clear Unused.}
+%
+%   When {\tt Proof using a} all section variables but for {\tt a} and
+%   the variables used in the type of {\tt a} are cleared.
+%   This option can be used to turn off this behavior.
+%
+\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
+\comindex{Collection}\label{Collection}
+
+The command {\tt Collection} can be used to name a set of section hypotheses,
+with the purpose of making {\tt Proof using} annotations more compact.
+
+\variant {\tt Collection Some := x y z.}
+
+  Define the collection named "Some" containing {\tt x y} and {\tt z}
+
+\variant {\tt Collection Fewer := Some - x.}
+
+  Define the collection named "Fewer" containing only {\tt x y}
+
+\variant {\tt Collection Many := Fewer + Some.}
+\variant {\tt Collection Many := Fewer - Some.}
+
+  Define the collection named "Many" containing the set union or set difference
+  of "Fewer" and "Some".
+
+\variant {\tt Collection Many := Fewer - (x y).}
+
+  Define the collection named "Many" containing the set difference
+  of "Fewer" and the unnamed collection {\tt x y}.
+
+\subsection[\tt Abort.]{\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 (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 Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
+\label{Existential}}
+
+This command instantiates an existential variable. {\tt \num}
+is an index in the list of uninstantiated existential variables
+displayed by {\tt Show Existentials} (described in Section~\ref{Show}).
+
+This command is intended to be used to instantiate existential
+variables when the proof is completed but some uninstantiated
+existential variables remain. To instantiate existential variables
+during proof edition, you should use the tactic {\tt instantiate}.
+
+\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
+\SeeAlso {\tt Grab Existential Variables.} below.
+
+\subsection[\tt Grab Existential Variables.]{\tt Grab Existential Variables.\comindex{Grab Existential Variables}
+\label{GrabEvars}}
+
+This command can be run when a proof has no more goal to be solved but has remaining
+uninstantiated existential variables. It takes every uninstantiated existential variable
+and turns it into a goal.
+
+%%%%%%%%
+\section{Navigation in the proof tree}
+%%%%%%%%
+
+\subsection[\tt Undo.]{\tt Undo.\comindex{Undo}}
+
+This command cancels the effect of the last command.  Thus, it
+backtracks one step.
+
+\begin{Variants}
+
+\item {\tt Undo {\num}.}
+
+  Repeats {\tt Undo} {\num} times.
+
+\end{Variants}
+
+\subsection[\tt Restart.]{\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.]{\tt Focus.\comindex{Focus}}
+This focuses the attention on the first subgoal to prove and the printing
+of the other subgoals is suspended until the focused subgoal is
+solved or unfocused. This is useful when there are many current
+subgoals which clutter your screen.
+
+\begin{Variant}
+\item {\tt Focus {\num}.}\\
+This focuses the attention on the $\num^{th}$ subgoal to prove.
+\end{Variant}
+
+\emph{This command is deprecated since 8.8: prefer the use of bullets or
+  focusing brackets instead, including {\tt {\num}: \{}}.
+
+\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
+This command restores to focus the goal that were suspended by the
+last {\tt Focus} command.
+
+\emph{This command is deprecated since 8.8.}
+
+\subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
+Succeeds in the proof if fully unfocused, fails if there are some
+goals out of focus.
+
+\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
+The command {\tt \{} (without a terminating period) focuses on the
+first goal, much like {\tt Focus.} does, however, the subproof can
+only be unfocused when it has been fully solved (\emph{i.e.} when
+there is no focused goal left). Unfocusing is then handled by {\tt \}}
+(again, without a terminating period). See also example in next section.
+
+Note that when a focused goal is proved a message is displayed
+together with a suggestion about the right bullet or {\tt \}} to
+unfocus it or focus the next one.
+
+\begin{Variants}
+
+\item {\tt {\num}: \{}\\
+This focuses on the $\num^{th}$ subgoal to prove.
+
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{This proof is focused, but cannot be unfocused
+    this way} You are trying to use {\tt \}} but the current subproof
+  has not been fully solved.
+\item \errindex{No such goal}
+\item \errindex{Brackets only support the single numbered goal selector}
+\item see also error message about bullets below.
+\end{ErrMsgs}
+
+\subsection[Bullets]{Bullets\comindex{+ (command)}
+  \comindex{- (command)}\comindex{* (command)}\index{Bullets}}\label{bullets}
+Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with
+bullets. The use of a bullet $b$ for the first time focuses on the
+first goal $g$, the same bullet cannot be used again until the proof
+of $g$ is completed, then it is mandatory to focus the next goal with $b$. The
+consequence is that $g$ and all goals present when $g$ was focused are
+focused with the same bullet $b$. See the example below.
+
+Different bullets can be used to nest levels. The scope of bullet does
+not go beyond enclosing {\tt \{} and {\tt \}}, so bullets can be
+reused as further nesting levels provided they are delimited by these.
+Available bullets are {\tt -}, {\tt +}, {\tt *}, {\tt --}, {\tt ++}, {\tt **},
+{\tt ---}, {\tt +++}, {\tt ***}, ... (without a
+terminating period).
+
+Note again that when a focused goal is proved a message is displayed
+together with a suggestion about the right bullet or {\tt \}} to
+unfocus it or focus the next one.
+
+Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use
+bullets with the priority ordering shown above to have a correct
+indentation. For example {\tt -} must be the outer bullet and {\tt **}
+the inner one in the example below.
+
+The following example script illustrates all these features:
+\begin{coq_example*}
+Goal (((True/\True)/\True)/\True)/\True.
+Proof.
+  split.
+  - split.
+    + split.
+      ** { split.
+          - trivial.
+          - trivial.
+        }
+      ** trivial.
+    + trivial.
+  - assert True.
+    { trivial. }
+    assumption.
+\end{coq_example*}
+
+
+\begin{ErrMsgs}
+\item \errindex{Wrong bullet {\abullet}1 : Current bullet
+    {\abullet}2 is not finished.}
+
+  Before using bullet {\abullet}1 again, you should first finish
+  proving the current focused goal. Note that {\abullet}1 and
+  {\abullet}2 may be the same.
+
+\item \errindex{Wrong bullet {\abullet}1 : Bullet {\abullet}2
+    is mandatory here.} You must put {\abullet}2 to focus next goal.
+  No other bullet is allowed here.
+
+
+\item \errindex{No such goal. Focus next goal with bullet
+    {\abullet}.}
+
+  You tried to applied a tactic but no goal where under focus. Using
+  {\abullet} is mandatory here.
+
+\item \errindex{No such goal. Try unfocusing with {"{\tt \}}"}.} You
+  just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}".
+
+\end{ErrMsgs}
+
+\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}}
+
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
+
+\section{Requesting information}
+
+\subsection[\tt Show.]{\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}
+\item \errindex{No such goal}
+\item \errindex{No focused proof}
+\end{ErrMsgs}
+
+\item {\tt Show {\ident}.}\\
+  Displays the named goal {\ident}.
+  This is useful in particular to display a shelved goal but only works
+  if the corresponding existential variable has been named by the user
+  (see~\ref{ExistentialVariables}) as in the following example.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Goal exists n, n = 0.
+  eexists ?[n].
+\end{coq_example*}
+\begin{coq_example}
+  Show n.
+\end{coq_example}
+
+\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 under the form \verb!<Your Tactic Text here>!.
+
+\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.
+
+\item{\tt Show Intro.}\comindex{Show Intro}\\
+If the current goal begins by at least one product, this command
+prints the name of the first product, as it would be generated by
+an anonymous {\tt intro}. The aim of this command is to ease the
+writing of more robust scripts. For example, with an appropriate
+{\ProofGeneral} macro, it is possible to transform any anonymous {\tt
+  intro} into a qualified one such as {\tt intro y13}.
+In the case of a non-product goal, it prints nothing.
+
+\item{\tt Show Intros.}\comindex{Show Intros}\\
+This command is similar to the previous one, it simulates the naming
+process of an {\tt intros}.
+
+\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
+\\ It displays
+the set of all uninstantiated existential variables in the current proof tree,
+along with the type and the context of each variable.
+
+\item{\tt Show Match {\ident}.\label{ShowMatch}}\comindex{Show Match}\\
+This variant displays a template of the Gallina {\tt match} construct
+with a branch for each constructor of the type {\ident}.
+
+Example:
+
+\begin{coq_example}
+Show Match nat.
+\end{coq_example}
+\begin{ErrMsgs}
+\item \errindex{Unknown inductive type}
+\end{ErrMsgs}
+
+\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
+\\ It displays the set of all universe constraints and its
+normalized form at the current stage of the proof, useful for
+debugging universe inconsistencies.
+
+\end{Variants}
+
+
+\subsection[\tt Guarded.]{\tt Guarded.\comindex{Guarded}\label{Guarded}}
+
+Some tactics (e.g. refine \ref{refine}) allow to build proofs using
+fixpoint or co-fixpoint constructions. Due to the incremental nature
+of interactive proof construction, the check of the termination (or
+guardedness) of the recursive calls in the fixpoint or cofixpoint
+constructions is postponed to the time of the completion of the proof.
+
+The command \verb!Guarded! allows checking if the guard condition for
+fixpoint and cofixpoint is violated at some time of the construction
+of the proof without having to wait the completion of the proof."
+
+
+\section{Controlling the effect of proof editing commands}
+
+\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\optindex{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.]{\tt Unset Hyps Limit.\optindex{Hyps Limit}}
+This command goes back to the default mode which is to print all
+available hypotheses.
+
+
+\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\optindex{Automatic Introduction}\label{Set Automatic Introduction}}
+
+The option {\tt Automatic Introduction} controls the way binders are
+handled in assertion commands such as {\tt Theorem {\ident}
+  \zeroone{\binders} : {\form}}. When the option is set, which is the
+default, {\binders} are automatically put in the local context of the
+goal to prove.
+
+The option can be unset by issuing {\tt Unset Automatic Introduction}.
+When the option is unset, {\binders} are discharged on the statement
+to be proved and a tactic such as {\tt intro} (see
+Section~\ref{intro}) has to be used to move the assumptions to the
+local context.
+
+\section{Controlling memory usage\comindex{Optimize Proof}\comindex{Optimize Heap}}
+
+When experiencing high memory usage the following commands can be
+used to force Coq to optimize some of its internal data structures.
+
+\subsection[\tt Optimize Proof.]{\tt Optimize Proof.}
+
+This command forces Coq to shrink the data structure used to represent
+the ongoing proof.
+
+\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
+
+This command forces the OCaml runtime to perform a heap compaction.
+This is in general an expensive operation.  See: \\
+\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
+There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: