From ca7a7ffbf5e0576e2a50052e644c1d067843fddf Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 3 Apr 2018 14:05:50 +0200 Subject: [Sphinx] Move chapter 7 to new infrastructure --- Makefile.doc | 1 - doc/refman/RefMan-pro.tex | 581 ----------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/proof-engine/proof-handling.rst | 581 +++++++++++++++++++++++++++++ 4 files changed, 581 insertions(+), 583 deletions(-) delete mode 100644 doc/refman/RefMan-pro.tex create mode 100644 doc/sphinx/proof-engine/proof-handling.rst 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/RefMan-pro.tex b/doc/refman/RefMan-pro.tex deleted file mode 100644 index bd74a40d7..000000000 --- a/doc/refman/RefMan-pro.tex +++ /dev/null @@ -1,581 +0,0 @@ -\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!!. - -\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: 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/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst new file mode 100644 index 000000000..eb3a24a2b --- /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!!. + +\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: -- cgit v1.2.3