diff options
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 393 |
1 files changed, 0 insertions, 393 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex deleted file mode 100644 index 208a014a..00000000 --- a/doc/refman/RefMan-pro.tex +++ /dev/null @@ -1,393 +0,0 @@ -\chapter{Proof handling} -\index{Proof editing} -\label{Proof-handling} - -In \Coq's proof editing mode all top-level commands documented in -chapter \ref{Vernacular-commands} remain available -and the user has access to specialized commands dealing with proof -development pragmas documented in this section. He can also use some -other specialized commands called {\em tactics}. They are the very -tools allowing the user to deal with logical reasoning. They are -documented in chapter \ref{Tactics}.\\ -When switching in editing proof mode, the prompt -\index{Prompt} -{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the -declared name of the theorem currently edited. - -At each stage of a proof development, one has a list of goals to -prove. Initially, the list consists only in the theorem itself. After -having applied some tactics, the list of goals contains the subgoals -generated by the tactics. - -To each subgoal is associated a number of -hypotheses we call the {\em \index*{local context}} of the goal. -Initially, the local context is empty. It is enriched by the use of -certain tactics (see mainly section~\ref{intro}). - -When a proof is achieved the message {\tt Proof completed} is -displayed. One can then store this proof as a defined constant in the -environment. Because there exists a correspondence between proofs and -terms of $\lambda$-calculus, known as the {\em Curry-Howard -isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as -terms of {\sc Cic}. Those terms are called {\em proof - terms}\index{Proof term}. - -It is possible to edit several proofs at the same time: see section -\ref{Resume} - -\ErrMsg When one attempts to use a proof editing command out of the -proof editing mode, \Coq~ raises the error message : \errindex{No focused - proof}. - -\section{Switching on/off the proof editing mode} - -\subsection{\tt Goal {\form}.} -\comindex{Goal}\label{Goal} -This command switches \Coq~ to editing proof mode and sets {\form} as -the original goal. It associates the name {\tt Unnamed\_thm} to -that goal. - -\begin{ErrMsgs} -\item \errindex{the term \form\ has type \ldots{} which should be Set, - Prop or Type} -%\item \errindex{Proof objects can only be abstracted} -%\item \errindex{A goal should be a type} -%\item \errindex{repeated goal not permitted in refining mode} -%the command {\tt Goal} cannot be used while a proof is already being edited. -\end{ErrMsgs} - -\SeeAlso section \ref{Theorem} - -\subsection{\tt Qed.}\comindex{Qed}\label{Qed} -This command is available in interactive editing proof mode when the -proof is completed. Then {\tt Qed} extracts a proof term from the -proof script, switches back to {\Coq} top-level and attaches the -extracted proof term to the declared name of the original goal. This -name is added to the environment as an {\tt Opaque} constant. - -\begin{ErrMsgs} -\item \errindex{Attempt to save an incomplete proof} -%\item \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} - - Is 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}.} - - Are equivalent to {\tt Save {\ident}.} -\end{Variants} - -\subsection{\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 Theorem {\ident} : {\form}.} -\comindex{Theorem} -\label{Theorem} - -This command switches to interactive editing proof mode and declares -{\ident} as being the name of the original goal {\form}. When declared -as a {\tt Theorem}, the name {\ident} is known at all section levels: -{\tt Theorem} is a {\sl global} lemma. - -%\ErrMsg (see section \ref{Goal}) - -\begin{ErrMsgs} - -\item \errindex{the term \form\ has type \ldots{} which should be Set, - Prop or Type} - -\item \errindexbis{\ident already exists}{already exists} - - The name you provided already defined. You have then to choose - another name. - -\end{ErrMsgs} - - -\begin{Variants} - -\item {\tt Lemma {\ident} : {\form}.} -\comindex{Lemma} - - It is equivalent to {\tt Theorem {\ident} : {\form}.} - -\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\ - {\tt Fact {\ident} : {\form}.}\comindex{Fact} - - Used to have a different meaning, but are now equivalent to {\tt - Theorem {\ident} : {\form}.} They are kept for compatibility. - -\item {\tt Definition {\ident} : {\form}.} -\comindex{Definition} - - Analogous to {\tt Theorem}, intended to be used in conjunction with - {\tt Defined} (see \ref{Defined}) in order to define a - transparent constant. - -\item {\tt Let {\ident} : {\form}.} -\comindex{Let} - - Analogous to {\tt Definition} except that the definition is turned - into a local definition on objects depending on it after closing the - current section. -\end{Variants} - -\subsection{\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.} -\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.} -\comindex{Suspend} - -This command applies in proof editing mode. It switches back to the -\Coq\ toplevel, but without canceling the current proofs. - -\subsection{\tt Resume.} -\comindex{Resume}\label{Resume} - -This commands switches back to the editing of the last edited proof. - -\begin{ErrMsgs} -\item \errindex{No proof-editing in progress} -\end{ErrMsgs} - -\begin{Variants} - -\item {\tt Resume {\ident}.} - - Restarts the editing of the proof named {\ident}. This can be used - to navigate between currently edited proofs. - -\end{Variants} - -\begin{ErrMsgs} -\item \errindex{No such proof} -\end{ErrMsgs} - -\section{Navigation in the proof tree} - -\subsection{\tt Undo.} -\comindex{Undo} - -This command cancels the effect of the last tactic command. Thus, it -backtracks one step. - -\begin{ErrMsgs} -\item \errindex{No focused proof (No proof-editing in progress)} -\item \errindex{Undo stack would be exhausted} -\end{ErrMsgs} - -\begin{Variants} - -\item {\tt Undo {\num}.} - - Repeats {\tt Undo} {\num} times. - -\end{Variants} - -\subsection{\tt Set Undo {\num}.} -\comindex{Set Undo} - -This command changes the maximum number of {\tt Undo}'s that will be -possible when doing a proof. It only affects proofs started after -this command, such that if you want to change the current undo limit -inside a proof, you should first restart this proof. - -\subsection{\tt Unset Undo.} -\comindex{Unset Undo} - -This command resets the default number of possible {\tt Undo} commands -(which is currently 12). - -\subsection{\tt Restart.}\comindex{Restart} -This command restores the proof editing process to the original goal. - -\begin{ErrMsgs} -\item \errindex{No focused proof to restart} -\end{ErrMsgs} - -\subsection{\tt Focus.}\comindex{Focus} -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^{\scriptsize th}$ subgoal to prove. - -\end{Variant} - -\subsection{\tt Unfocus.}\comindex{Unfocus} -Turns off the focus mode. - - -\section{Displaying information} - -\subsection{\tt Show.}\comindex{Show}\label{Show} -This command displays the current goals. - -\begin{Variants} -\item {\tt Show {\num}.}\\ - Displays only the {\num}-th subgoal.\\ -\begin{ErrMsgs} -\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!<Your Tactic Text here>!. - -\item {\tt Show Tree.}\comindex{Show Tree}\\ -This command can be seen as a more structured way of -displaying the state of the proof than that -provided by {\tt Show Script}. Instead of just giving -the list of tactics that have been applied, it -shows the derivation tree constructed by then. -Each node of the tree contains the conclusion -of the corresponding sub-derivation (i.e. a -goal with its corresponding local context) and -the tactic that has generated all the -sub-derivations. The leaves of this tree are -the goals which still remain to be proved. - -%\item {\tt Show Node}\comindex{Show Node}\\ -% Not yet documented - -\item {\tt Show Proof.}\comindex{Show Proof}\\ -It displays the proof term generated by the -tactics that have been applied. -If the proof is not completed, this term contain holes, -which correspond to the sub-terms which are still to be -constructed. These holes appear as a question mark indexed -by an integer, and applied to the list of variables in -the context, since it may depend on them. -The types obtained by abstracting away the context from the -type of each hole-placer are also printed. - -\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\ -It prints the list of the names of all the theorems that -are currently being proved. -As it is possible to start proving a previous lemma during -the proof of a theorem, this list may contain several -names. - -\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}. - -\end{Variants} - -\subsection{\tt Set Hyps Limit {\num}.} -\comindex{Set Hyps Limit} -This command sets the maximum number of hypotheses displayed in -goals after the application of a tactic. -All the hypotheses remains usable in the proof development. - -\subsection{\tt Unset Hyps Limit.} -\comindex{Unset Hyps Limit} -This command goes back to the default mode which is to print all -available hypotheses. - -\section{$DPL$ : A Declarative proof language for Coq \emph{(experimental)} } - -An implementation of the $DPL$ declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq. - - Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at : - -\url{http://www.cs.ru.nl/~corbineau/mmode.html} - - - - -% $Id: RefMan-pro.tex 9286 2006-10-26 17:43:00Z corbinea $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |