diff options
-rw-r--r-- | Makefile.doc | 1 | ||||
-rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
-rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst (renamed from doc/refman/RefMan-pro.tex) | 104 |
3 files changed, 52 insertions, 54 deletions
diff --git a/Makefile.doc b/Makefile.doc index fc791ce1c..a8b5376a6 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -59,7 +59,6 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-pro.v.tex \ Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index e51116007..8909c0fef 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -99,7 +99,6 @@ Options A and B of the licence are {\em not} elected.} \part{The proof engine} \include{RefMan-oth.v}% Vernacular commands -\include{RefMan-pro.v}% Proof handling \include{RefMan-ltac.v}% Writing tactics \lstset{language=SSR} diff --git a/doc/refman/RefMan-pro.tex b/doc/sphinx/proof-engine/proof-handling.rst index bd74a40d7..eb3a24a2b 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -2,15 +2,15 @@ \label{Proof-handling}} %HEVEA\cutname{proof-handling.html} -In \Coq's proof editing mode all top-level commands documented in +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}.\\ +documented in Chapter~\ref{Tactics}.\\ When switching in editing proof mode, the prompt -\index{Prompt} +\index{Prompt} {\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the declared name of the theorem currently edited. @@ -70,7 +70,7 @@ 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}\\ +%\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, @@ -86,13 +86,13 @@ memory overflow. \begin{Variants} \item {\tt Defined.} -\comindex{Defined} -\label{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. @@ -110,7 +110,7 @@ This command applies in proof editing mode. It is equivalent to {\tt 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 @@ -122,9 +122,9 @@ one gulp, as a proof term (see Section~\ref{exact}). {{\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 +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. @@ -133,20 +133,20 @@ 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 .} +\variant {\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$} {\tt with} {\tac}{\tt .} in Section~\ref{ProofWith}. -\variant {\tt Proof using All.} +\variant {\tt Proof using All.} Use all section variables. -\variant {\tt Proof using Type.} -\variant {\tt Proof using.} - +\variant {\tt Proof using Type.} +\variant {\tt Proof using.} + Use only section variables occurring in the statement. -\variant {\tt Proof using Type*.} - +\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}. @@ -154,7 +154,7 @@ in Section~\ref{ProofWith}. 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$ .} @@ -178,7 +178,7 @@ in Section~\ref{ProofWith}. The following options modify the behavior of {\tt Proof using}. -\variant {\tt Set Default Proof Using "expression".} +\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 } @@ -190,11 +190,11 @@ The following options modify the behavior of {\tt Proof using}. 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} @@ -203,15 +203,15 @@ 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} + 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 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.} -\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". @@ -296,7 +296,7 @@ solved or unfocused. This is useful when there are many current subgoals which clutter your screen. \begin{Variant} -\item {\tt Focus {\num}.}\\ +\item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. \end{Variant} @@ -430,8 +430,8 @@ This makes bullets active (this is the default behavior). This command displays the current goals. \begin{Variants} -\item {\tt Show {\num}.}\\ - Displays only the {\num}-th subgoal.\\ +\item {\tt Show {\num}.}\\ + Displays only the {\num}-th subgoal.\\ \begin{ErrMsgs} \item \errindex{No such goal} \item \errindex{No focused proof} @@ -457,54 +457,54 @@ Goal exists n, n = 0. \item {\tt Show Script.}\comindex{Show Script}\\ Displays the whole list of tactics applied from the beginning - of the current proof. + 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. +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. +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 +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. +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 +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 +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. +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 +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, +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 +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. +Show Match nat. \end{coq_example} \begin{ErrMsgs} \item \errindex{Unknown inductive type} @@ -535,7 +535,7 @@ of the proof without having to wait the completion of the proof." \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. +goals after the application of a tactic. All the hypotheses remains usable in the proof development. @@ -575,7 +575,7 @@ 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: +%%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% End: +%%% End: |