diff options
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 401 |
1 files changed, 0 insertions, 401 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex deleted file mode 100644 index ca3a9cc9..00000000 --- a/doc/refman/RefMan-pro.tex +++ /dev/null @@ -1,401 +0,0 @@ -\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}. - -\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 Proof using {\ident$_1$ \dots {\ident$_n$}}.] -{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}. -\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$ \dots {\ident$_n$}} 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 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}. -\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 tactic command. Thus, it -backtracks one step. - -\begin{ErrMsgs} -\item \errindex{No focused proof (No proof-editing in progress)} -\end{ErrMsgs} - -\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} - -\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} -This command restores to focus the goal that were suspended by the -last {\tt Focus} command. - -\subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}} -Succeeds in the proof is fully unfocused, fails is there are some -goals out of focus. - -\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}} -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. - -\subsection[Bullets]{Bullets\comindex{+ (command)}\comindex{- (command)}\comindex{* (command)}\index{Bullets}} -Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with -bullets. The use of a bullet for the first time focuses on the first -goal, the same bullet cannot be used again until the subproof in -completed, then it focuses on the next goal. 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 -level provided they are delimited by these. Available bullets are -{\tt -}, {\tt +} and {\tt *} (without a terminating period). - -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. - - trivial. -\end{coq_example*} - - -\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!<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}. - -\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. - - -\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: |