From fb73dae49f461f5ec81af870ce8279d619ebef9a Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 8 Jun 2010 13:56:19 +0000 Subject: Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction". Updated documentation in many ways: - merged binder and binderlet as done for a while in implementation - fixed a few technical problems (bad indexation of {x:A|P x}, missing spaces in html code in many situations due to missing curly brackets around TeX macros - e.g. around \ldots -, missing dots at end of sentences, ...) - renamed "statement" commands into "assertion" commands and "declaration" commands into "assumption" commands - moved Goal and Save out of the Gallina chapter - avoid some recovering in the Gallina and proof mode chapters - slight smoothing of some hard-to-read paragraphs of the manual git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-pro.tex | 123 ++++++++++++++++++---------------------------- 1 file changed, 49 insertions(+), 74 deletions(-) (limited to 'doc/refman/RefMan-pro.tex') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index a8bb7966a..d73ab5d2c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -19,20 +19,23 @@ 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 +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 at the same time: see section -\ref{Resume} +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 @@ -40,21 +43,25 @@ proof editing mode, \Coq~ raises the error message : \errindex{No focused \section{Switching on/off the proof editing mode} -\subsection[\tt Goal {\form}.]{\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. +The proof editing mode is entered by asserting a statement, which +typically is the assertion of a theorem: -\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} +\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. -\SeeAlso Section~\ref{Theorem} +\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 @@ -89,7 +96,7 @@ memory overflow. \item {\tt Save.} \comindex{Save} - Is equivalent to {\tt Qed}. + This is a deprecated equivalent to {\tt Qed}. \item {\tt Save {\ident}.} @@ -101,6 +108,8 @@ memory overflow. {\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} @@ -109,57 +118,6 @@ memory overflow. 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}.]{\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}.]{\tt Proof {\term}.\comindex{Proof} \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt @@ -234,7 +192,7 @@ 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 intented to be used to instantiate existential +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}. @@ -392,6 +350,8 @@ 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. @@ -402,6 +362,21 @@ All the hypotheses remains usable in the proof development. 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" -- cgit v1.2.3