From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- doc/refman/RefMan-pro.tex | 385 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 385 insertions(+) create mode 100644 doc/refman/RefMan-pro.tex (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex new file mode 100644 index 00000000..3a8936eb --- /dev/null +++ b/doc/refman/RefMan-pro.tex @@ -0,0 +1,385 @@ +\chapter[Proof handling]{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 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}. + +It is possible to edit several proofs in parallel: 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 : \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.} +\comindex{Save} + + This is a deprecated equivalent to {\tt Qed}. + +\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. + +\item {\tt Save Theorem {\ident}.} \\ + {\tt Save Lemma {\ident}.} \\ + {\tt Save Remark {\ident}.}\\ + {\tt Save Fact {\ident}.} + {\tt Save Corollary {\ident}.} + {\tt Save Proposition {\ident}.} + + Are equivalent to {\tt Save {\ident}.} +\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}; Save.} 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 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 Suspend.]{\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.]{\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} + + +%%%% +\subsection[\tt Existential {\num} := {\term}.]{\tt Existential {\num} := {\term}.\comindex{Existential} +\label{Existential}} + +This command allows to instantiate 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}. + + +%%%%%%%% +\section{Navigation in the proof tree} +%%%%%%%% + +\subsection[\tt Undo.]{\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}.]{\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.]{\tt Unset Undo.\comindex{Unset Undo}} + +This command resets the default number of possible {\tt Undo} commands +(which is currently 12). + +\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} + +\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} +Turns off the focus mode. + + +\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 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 under the form \verb!!. + +\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. + +\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 +Proof General 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}\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. + +\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 to verify 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}.\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.]{\tt Unset Hyps Limit.\comindex{Unset Hyps Limit}} +This command goes back to the default mode which is to print all +available hypotheses. + +% $Id: RefMan-pro.tex 13091 2010-06-08 13:56:19Z herbelin $ + + +\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset 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. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3