diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /doc/refman/RefMan-pro.tex | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 389 |
1 files changed, 389 insertions, 0 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex new file mode 100644 index 00000000..739ca6b5 --- /dev/null +++ b/doc/refman/RefMan-pro.tex @@ -0,0 +1,389 @@ +\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} +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}). + +\begin{Variants} + +\item{\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.} + +\item{\tt Proof with {\tac}.} + + This command may be used to start a proof. It defines a default + tactic to be used each time a tactic command is ended by + ``\verb#...#''. In this case the tactic command typed by the user is + equivalent to \emph{command};{\tac}. + +\end{Variants} + +\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. + +% $Id: RefMan-pro.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |