diff options
| -rwxr-xr-x | doc/common/macros.tex | 18 | ||||
| -rw-r--r-- | doc/refman/Coercion.tex | 12 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 20 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 303 | ||||
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 16 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 123 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
10 files changed, 258 insertions, 247 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index c4e797363..f0fb0883b 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -75,8 +75,8 @@ \newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}} %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*} %\newcommand{\onemany}[1]{$\{$#1$\}$+} -\newcommand{\nelist}[2]{{#1} {\tt #2} {\ldots} {\tt #2} {#1}} -\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} {\ldots} {\tt #2} {#1}{\sl ]}} +\newcommand{\nelist}[2]{{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}} +\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}{\sl ]}} \newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1} \newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$} @@ -123,8 +123,7 @@ \newcommand{\assums}{\nterm{assums}} % vernac \newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions \newcommand{\binder}{\nterm{binder}} -\newcommand{\binderlet}{\nterm{binderlet}} -\newcommand{\binderlist}{\nterm{binderlist}} +\newcommand{\binders}{\nterm{binders}} \newcommand{\caseitems}{\nterm{match\_items}} \newcommand{\caseitem}{\nterm{match\_item}} \newcommand{\eqn}{\nterm{equation}} @@ -137,10 +136,11 @@ \newcommand{\params}{\nterm{params}} % vernac \newcommand{\returntype}{\nterm{return\_type}} \newcommand{\idparams}{\nterm{ident\_with\_params}} -\newcommand{\statkwd}{\nterm{statement\_keyword}} % vernac +\newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac \newcommand{\termarg}{\nterm{arg}} -\newcommand{\typecstr}{\zeroone{{\tt :} {\term}}} +\newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} +\newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} \newcommand{\Fwterm}{\nterm{Fwterm}} @@ -154,8 +154,8 @@ \newcommand{\commandtac}{\nterm{tactic\_invocation}} \newcommand{\constructor}{\nterm{constructor}} \newcommand{\convtactic}{\nterm{conv\_tactic}} -\newcommand{\declarationkeyword}{\nterm{declaration\_keyword}} -\newcommand{\declaration}{\nterm{declaration}} +\newcommand{\assumptionkeyword}{\nterm{assumption\_keyword}} +\newcommand{\assumption}{\nterm{assumption}} \newcommand{\definition}{\nterm{definition}} \newcommand{\digit}{\nterm{digit}} \newcommand{\exteqn}{\nterm{ext\_eqn}} @@ -211,7 +211,7 @@ \newcommand{\simplepattern}{\nterm{simple\_pattern}} \newcommand{\sort}{\nterm{sort}} \newcommand{\specif}{\nterm{specif}} -\newcommand{\statement}{\nterm{statement}} +\newcommand{\assertion}{\nterm{assertion}} \newcommand{\str}{\nterm{string}} \newcommand{\subsequentletter}{\nterm{subsequent\_letter}} \newcommand{\switch}{\nterm{switch}} diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 6877db179..7a74ffd31 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -202,8 +202,8 @@ valid coercion paths are ignored; they are signaled by a warning. source and its target. \item Assumptions can be declared as coercions at declaration -time. This extends the grammar of declarations from Figure -\ref{sentences-syntax} as follows: +time. This extends the grammar of assumptions from +Figure~\ref{sentences-syntax} as follows: \comindex{Variable \mbox{\rm (and coercions)}} \comindex{Axiom \mbox{\rm (and coercions)}} \comindex{Parameter \mbox{\rm (and coercions)}} @@ -211,7 +211,7 @@ time. This extends the grammar of declarations from Figure \begin{tabular}{lcl} %% Declarations -{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\ +{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\ &&\\ {\assums} & ::= & {\simpleassums} \\ & $|$ & \nelist{{\tt (} \simpleassums {\tt )}}{} \\ @@ -236,10 +236,10 @@ grammar of inductive types from Figure \ref{sentences-syntax} as follows: & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ {\inductivebody} & ::= & - {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\ + {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ && ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\ & & \\ -{\constructor} & ::= & {\ident} \sequence{\binderlet}{} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\ +{\constructor} & ::= & {\ident} \zeroone{\binders} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\ \end{tabular} \end{center} @@ -331,7 +331,7 @@ classes as records) by extending the existing {\tt Record} macro \begin{center} \begin{tabular}{l} -{\tt Record \zeroone{>}~{\ident} {\binderlet} : {\sort} := \zeroone{\ident$_0$} \verb+{+} \\ +{\tt Record \zeroone{>}~{\ident} \zeroone{\binders} : {\sort} := \zeroone{\ident$_0$} \verb+{+} \\ ~~~~\begin{tabular}{l} {\tt \ident$_1$ $[$:$|$:>$]$ \term$_1$ ;} \\ ... \\ diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index f7f4d95d9..b41014ab7 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -94,7 +94,7 @@ does not produce an equality, contrary to the let pattern construct {\tt let '(x1, ..., xn) := t in b}. The next two commands are similar to their standard counterparts -Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that +Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that they define constants. However, they may require the user to prove some goals to construct the final definitions. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 503167987..13aef43c7 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -20,7 +20,7 @@ construction allows to define ``signatures''. {\sentence} & ++= & {\record}\\ & & \\ {\record} & ::= & - {\tt Record} {\ident} \sequence{\binderlet}{} \zeroone{{\tt :} {\sort}} \verb.:=. \\ + {\tt Record} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\ && ~~~~\zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ & & \\ @@ -86,7 +86,7 @@ Remark here that the field % %\medskip %\noindent -%{\tt Inductive {\ident} {\binderlet} : {\sort} := \\ +%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\ %\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. %({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.} %\medskip @@ -828,7 +828,7 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe The sectioning mechanism allows to organize a proof in structured sections. Then local declarations become available (see -Section~\ref{Simpl-definitions}). +Section~\ref{Basic-definitions}). \subsection{\tt Section {\ident}\comindex{Section}} @@ -844,13 +844,13 @@ This command is used to open a section named {\ident}. \subsection{\tt End {\ident} \comindex{End}} -This command closes the section named {\ident}. When a section is -closed, all local declarations (variables and local definitions) are -{\em discharged}. This means that all global objects defined in the -section are generalized with respect to all variables and local -definitions it depends on in the section. None of the local -declarations (considered as autonomous declarations) survive the end -of the section. +This command closes the section named {\ident}. After closing of the +section, the local declarations (variables and local definitions) get +{\em discharged}, meaning that they stop being visible and that all +global objects defined in the section are generalized with respect to +the variables and local definitions they each depended on in the +section. + Here is an example : \begin{coq_example} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 5461779fe..d14895917 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -30,7 +30,7 @@ The notation ``\nelist{\entry}{sep}'' stands for a non empty sequence of expressions parsed by {\entry} and separated by the literal ``{\tt sep}''\footnote{This is similar to the expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in -standard BNF, or ``{\entry} $($ {\tt sep} {\entry} $)$*'' in +standard BNF, or ``{\entry}~{$($} {\tt sep} {\entry} {$)$*}'' in the syntax of regular expressions.}. Similarly, the notation ``\nelist{\entry}{}'' stands for a non @@ -228,11 +228,11 @@ Chapter \ref{Addoc-syntax}. \begin{centerframe} \begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad {\term} & ::= & - {\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\ - & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\ + {\tt forall} {\binders} {\tt ,} {\term} &(\ref{products})\\ + & $|$ & {\tt fun} {\binders} {\tt =>} {\term} &(\ref{abstractions})\\ & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\ & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\ - & $|$ & {\tt let} {\idparams} {\tt :=} {\term} + & $|$ & {\tt let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt in} {\term} &(\ref{let-in})\\ & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\ & $|$ & {\tt let cofix} {\cofixpointbody} @@ -263,13 +263,10 @@ Chapter \ref{Addoc-syntax}. %% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )} %% &(\ref{Implicits-explicitation})\\ &&&\\ -{\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\ - & $|$ & {\binder} \nelist{\binderlet}{} &\\ +{\binders} & ::= & \nelist{\binder}{} \\ &&&\\ {\binder} & ::= & {\name} & (\ref{Binders}) \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ -&&&\\ -{\binderlet} & ::= & {\binder} & (\ref{Binders}) \\ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ & & &\\ {\name} & ::= & {\ident} &\\ @@ -292,8 +289,6 @@ Chapter \ref{Addoc-syntax}. \begin{figure}[htb] \begin{centerframe} \begin{tabular}{lcl} -{\idparams} & ::= & {\ident} \sequence{\binderlet}{} {\typecstr} \\ -&&\\ {\fixpointbodies} & ::= & {\fixpointbody} \\ & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}} @@ -304,9 +299,9 @@ Chapter \ref{Addoc-syntax}. {\tt for} {\ident} \\ &&\\ {\fixpointbody} & ::= & - {\ident} \nelist{\binderlet}{} \zeroone{\annotation} {\typecstr} + {\ident} {\binders} \zeroone{\annotation} {\typecstr} {\tt :=} {\term} \\ -{\cofixpointbody} & ::= & {\idparams} {\tt :=} {\term} \\ +{\cofixpointbody} & ::= & {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} \\ & &\\ {\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ &&\\ @@ -418,15 +413,17 @@ sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type}\,{\tt )}. Some constructions allow the binding of a variable to value. This is -called a ``let-binder''. The entry {\binderlet} of the grammar accepts -either a binder as defined above or a let-binder. The notation in the +called a ``let-binder''. The entry {\binder} of the grammar accepts +either an assumption binder as defined above or a let-binder. +The notation in the latter case is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: {\tt (}\,{\ident}\,{\tt :}\,{\term}\,{\tt :=}\,{\term}\,{\tt )}. -Lists of {\binderlet} are allowed. In the case of {\tt fun} and {\tt -forall}, the first binder of the list cannot be a let-binder, but +Lists of {\binder} are allowed. In the case of {\tt fun} and {\tt + forall}, it is intended that at least one binder of the list is an +assumption otherwise {\tt fun} and {\tt forall} gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: {\tt fun~(x~y~z~:~A)~=>~t} can be shortened in {\tt fun~x~y~z~:~A~=>~t}). @@ -517,9 +514,9 @@ symbol ``\_'' and {\Coq} will guess the missing piece of information. the local binding of \term$_1$ to the variable $\ident$ in \term$_2$. There is a syntactic sugar for local definition of functions: {\tt -let} {\ident} {\binder$_1$} \ldots {\binder$_n$} {\tt :=} {\term$_1$} +let} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} {\tt :=} {\term$_1$} {\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun} -{\binder$_1$} \ldots {\binder$_n$} {\tt =>} {\term$_2$} {\tt in} +{\binder$_1$} {\ldots} {\binder$_n$} {\tt =>} {\term$_2$} {\tt in} {\term$_2$}. \subsection{Definition by case analysis @@ -553,8 +550,8 @@ expression. There are several cases. In the {\em non dependent} case, all branches have the same type, and the {\returntype} is the common type of branches. In this case, {\returntype} can usually be omitted as it can be inferred from the type of the branches\footnote{Except if -the inductive type is empty in which case there is no equation to help -to infer the return type.}. +the inductive type is empty in which case there is no equation that can be +used to infer the return type.}. In the {\em dependent} case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being @@ -678,27 +675,27 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt \begin{figure}[tbp] \begin{centerframe} \begin{tabular}{lcl} -{\sentence} & ::= & {\declaration} \\ +{\sentence} & ::= & {\assumption} \\ & $|$ & {\definition} \\ & $|$ & {\inductive} \\ & $|$ & {\fixpoint} \\ - & $|$ & {\statement} \zeroone{\proof} \\ + & $|$ & {\assertion} {\proof} \\ &&\\ -%% Declarations -{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\ +%% Assumptions +{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\ &&\\ -{\declarationkeyword} & ::= & {\tt Axiom} $|$ {\tt Conjecture} \\ +{\assumptionkeyword} & $\!\!$ ::= & {\tt Axiom} $|$ {\tt Conjecture} \\ & $|$ & {\tt Parameter} $|$ {\tt Parameters} \\ & $|$ & {\tt Variable} $|$ {\tt Variables} \\ & $|$ & {\tt Hypothesis} $|$ {\tt Hypotheses}\\ &&\\ {\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\ - & $|$ & \nelist{\binder}{} \\ + & $|$ & \nelist{{\tt (} \nelist{\ident}{} {\tt :} {\term} {\tt )}}{} \\ &&\\ %% Definitions {\definition} & ::= & - {\tt Definition} {\idparams} {\tt :=} {\term} {\tt .} \\ - & $|$ & {\tt Let} {\idparams} {\tt :=} {\term} {\tt .} \\ + {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ + & $|$ & {\tt Let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ &&\\ %% Inductives {\inductive} & ::= & @@ -706,22 +703,25 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ {\inductivebody} & ::= & - {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\ - && ~~~\zeroone{\zeroone{\tt |} \nelist{\idparams}{|}} \\ + {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ + && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\ & & \\ %% TODO: where ... %% Fixpoints {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ & $|$ & {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\ &&\\ %% Lemmas & proofs -{\statement} & ::= & - {\statkwd} {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt .} \\ +{\assertion} & ::= & + {\statkwd} {\ident} \zeroone{\binders} {\tt :} {\term} {\tt .} \\ &&\\ - {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} $|$ {\tt Definition} \\ + {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} \\ + & $|$ & {\tt Remark} $|$ {\tt Fact}\\ + & $|$ & {\tt Corollary} $|$ {\tt Proposition} \\ + & $|$ & {\tt Definition} $|$ {\tt Example} \\\\ &&\\ {\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\ & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\ - & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .} + & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\ \end{tabular} \end{centerframe} \caption{Syntax of sentences} @@ -739,22 +739,20 @@ that the terms occurring in the sentences are well-typed. %% %% Axioms and Parameters %% -\subsection{Declarations +\subsection{Assumptions \index{Declarations} \label{Declarations}} -The declaration mechanism allows the user to specify his own basic -objects. Declared objects play the role of axioms or parameters in -mathematics. A declared object is an {\ident} associated to a \term. A -declaration is accepted by {\Coq} if and only if this {\term} is a -correct type in the current context of the declaration and \ident\ was -not previously defined in the same module. This {\term} is considered -to be the type, or specification, of the \ident. +Assumptions extend the environment\index{Environment} with axioms, +parameters, hypotheses or variables. An assumption binds an {\ident} +to a {\type}. It is accepted by {\Coq} if and only if this {\type} is +a correct type in the environment preexisting the declaration and if +{\ident} was not previously defined in the same module. This {\type} +is considered to be the type (or specification, or statement) assumed +by {\ident} and we say that {\ident} has type {\type}. \subsubsection{{\tt Axiom {\ident} :{\term} .} \comindex{Axiom} -\comindex{Parameter}\comindex{Parameters} -\comindex{Conjecture} \label{Axiom}} This command links {\term} to the name {\ident} as its specification @@ -766,7 +764,8 @@ a postulate. \end{ErrMsgs} \begin{Variants} -\item {\tt Parameter {\ident} :{\term}.} \\ +\item \comindex{Parameter}\comindex{Parameters} + {\tt Parameter {\ident} :{\term}.} \\ Is equivalent to {\tt Axiom {\ident} : {\term}} \item {\tt Parameter {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\ @@ -779,7 +778,8 @@ a postulate. {\term$_n$} {\tt )}.}\\ Adds $n$ blocks of parameters with different specifications. -\item {\tt Conjecture {\ident} :{\term}.}\\ +\item \comindex{Conjecture} + {\tt Conjecture {\ident} :{\term}.}\\ Is equivalent to {\tt Axiom {\ident} : {\term}}. \end{Variants} @@ -790,16 +790,14 @@ a postulate. \subsubsection{{\tt Variable {\ident} :{\term}}. \comindex{Variable} \comindex{Variables} -\comindex{Hypothesis} -\comindex{Hypotheses}} -\label{Variable} +\label{Variable}} This command links {\term} to the name {\ident} in the context of the current section (see Section~\ref{Section} for a description of the section mechanism). When the current section is closed, name {\ident} will be unknown and every object using this variable will be explicitly parametrized (the variable is {\em discharged}). Using the {\tt -Variable} command out of any section is equivalent to {\tt Axiom}. +Variable} command out of any section is equivalent to using {\tt Parameter}. \begin{ErrMsgs} \item \errindex{{\ident} already exists} @@ -814,7 +812,9 @@ Variable} command out of any section is equivalent to {\tt Axiom}. \ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,% {\term$_n$} {\tt )}.}\\ Adds $n$ blocks of variables with different specifications. -\item {\tt Hypothesis {\ident} {\tt :}{\term}.} \\ +\item \comindex{Hypothesis} + \comindex{Hypotheses} + {\tt Hypothesis {\ident} {\tt :}{\term}.} \\ \texttt{Hypothesis} is a synonymous of \texttt{Variable} \end{Variants} @@ -832,19 +832,21 @@ abstract mathematical entity). %% \subsection{Definitions \index{Definitions} -\label{Simpl-definitions}} +\label{Basic-definitions}} + +Definitions extend the environment\index{Environment} with +associations of names to terms. A definition can be seen as a way to +give a meaning to a name or as a way to abbreviate a term. In any +case, the name can later be replaced at any time by its definition. -Definitions differ from declarations in allowing to give a name to a -term whereas declarations were just giving a type to a name. That is -to say that the name of a defined object can be replaced at any time -by its definition. This replacement is called +The operation of unfolding a name into its definition is called $\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see -Section~\ref{delta}). A defined object is accepted by the system if -and only if the defining term is well-typed in the current context of -the definition. Then the type of the name is the type of term. The -defined name is called a {\em constant}\index{Constant} and one says -that {\it the constant is added to the -environment}\index{Environment}. +Section~\ref{delta}). A definition is accepted by the system if and +only if the defined term is well-typed in the current context of the +definition and if the name is not already used. The name defined by +the definition is called a {\em constant}\index{Constant} and the term +it refers to is its {\em body}. A definition has a type which is the +type of its body. A formal presentation of constants and environments is given in Section~\ref{Typed-terms}. @@ -852,7 +854,7 @@ Section~\ref{Typed-terms}. \subsubsection{\tt Definition {\ident} := {\term}. \comindex{Definition}} -This command binds the value {\term} to the name {\ident} in the +This command binds {\term} to the name {\ident} in the environment, provided that {\term} is well-typed. \begin{ErrMsgs} @@ -881,10 +883,10 @@ These are synonyms of the {\tt Definition} forms. \end{Variants} \begin{ErrMsgs} -\item \errindex{Error: The term ``{\term}'' has type ``{\type}'' while it is expected to have type ``{\type}''} +\item \errindex{Error: The term {\term} has type {\type} while it is expected to have type {\type}} \end{ErrMsgs} -\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold} +\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}. \subsubsection{\tt Let {\ident} := {\term}. \comindex{Let}} @@ -905,7 +907,8 @@ section and depending on {\ident} are prefixed by the local definition \end{Variants} \SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque}, -\ref{Transparent} (opaque/transparent constants), \ref{unfold} +\ref{Transparent} (opaque/transparent constants), \ref{unfold} (tactic + {\tt unfold}). %% %% Inductive Types @@ -1137,7 +1140,7 @@ a less convenient rule for case elimination. \subsubsection{Mutually defined inductive types -\comindex{Mutual Inductive} +\comindex{Inductive} \label{Mutual-Inductive}} The definition of a block of mutually inductive types has the form: @@ -1250,7 +1253,7 @@ section is closed, the variables declared in the section and occurring free in the declaration are added as parameters to the inductive definition. -\SeeAlso Section~\ref{Section} +\SeeAlso Section~\ref{Section}. \subsubsection{Co-inductive types \label{CoInductiveTypes} @@ -1458,7 +1461,7 @@ Fixpoint tree_size (t:tree) : nat := A generic command {\tt Scheme} is useful to build automatically various mutual induction principles. It is described in Section~\ref{Scheme}. -\subsubsection{Definition of recursive objects in co-inductive types} +\subsubsection{Definitions of recursive objects in co-inductive types} The command: \begin{center} @@ -1534,47 +1537,51 @@ is possible to introduce a block of mutually dependent methods. %% %% Theorems & Lemmas %% -\subsection{Statement and proofs} +\subsection{Assertions and proofs} +\label{Assertions} + +An assertion states a proposition (or a type) of which the proof (or +an inhabitant of the type) is interactively built using tactics. The +interactive proof mode is described in +Chapter~\ref{Proof-handling} and the tactics in Chapter~\ref{Tactics}. +The basic assertion command is: -A statement claims a goal of which the proof is then interactively done -using tactics. More on the proof editing mode, statements and proofs can be -found in Chapter~\ref{Proof-handling}. +\subsubsection{\tt Theorem {\ident} \zeroone{\binders} : {\type}. +\comindex{Theorem}} -\subsubsection{\tt Theorem {\ident} : {\type}. -\comindex{Theorem} -\comindex{Lemma} -\comindex{Remark} -\comindex{Fact}} +After the statement is asserted, {\Coq} needs a proof. Once a proof of +{\type} under the assumptions represented by {\binders} is given and +validated, the proof is generalized into a proof of {\tt forall + \zeroone{\binders}, {\type}} and the theorem is bound to the name +{\ident} in the environment. -This command binds {\type} to the name {\ident} in the -environment, provided that a proof of {\type} is next given. +\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 is already defined. You have then to choose + another name. -After a statement, {\Coq} needs a proof. +\end{ErrMsgs} \begin{Variants} -\item {\tt Lemma {\ident} : {\type}.}\\ - {\tt Remark {\ident} : {\type}.}\\ - {\tt Fact {\ident} : {\type}.}\\ - {\tt Corollary {\ident} : {\type}.}\\ - {\tt Proposition {\ident} : {\type}.}\\ -\comindex{Proposition} -\comindex{Corollary} -All these commands are synonymous of \texttt{Theorem} -% Same as {\tt Theorem} except -% that if this statement is in one or more levels of sections then the -% name {\ident} will be accessible only prefixed by the sections names -% when the sections (see \ref{Section} and \ref{LongNames}) will be -% closed. -% %All proofs of persistent objects (such as theorems) referring to {\ident} -% %within the section will be replaced by the proof of {\ident}. -% Same as {\tt Remark} except -% that the innermost section name is dropped from the full name. -\item {\tt Theorem \nelist{{\ident} : {\type}}{with}.} +\item {\tt Lemma {\ident} \zeroone{\binders} : {\type}.}\comindex{Lemma}\\ + {\tt Remark {\ident} \zeroone{\binders} : {\type}.}\comindex{Remark}\\ + {\tt Fact {\ident} \zeroone{\binders} : {\type}.}\comindex{Fact}\\ + {\tt Corollary {\ident} \zeroone{\binders} : {\type}.}\comindex{Corollary}\\ + {\tt Proposition {\ident} \zeroone{\binders} : {\type}.}\comindex{Proposition} + +These commands are synonyms of \texttt{Theorem {\ident} \zeroone{\binders} : {\type}}. + +\item {\tt Theorem \nelist{{\ident} \zeroone{\binders}: {\type}}{with}.} This command is useful for theorems that are proved by simultaneous -induction over a mutually inductive assumption, or that state mutually +induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual coinductive type. It is equivalent -to {\tt Fixpoint} (see Section~\ref{Fixpoint}) or {\tt CoFixpoint} +to {\tt Fixpoint} or {\tt CoFixpoint} (see Section~\ref{CoFixpoint}) but using tactics to build the proof of the statements (or the body of the specification, depending on the point of view). The inductive or coinductive types on which the @@ -1593,20 +1600,45 @@ some time of the interactive development of a proof, use the command The command can be used also with {\tt Lemma}, {\tt Remark}, etc. instead of {\tt Theorem}. -\item {\tt Definition {\ident} : {\type}.} \\ -Allow to define a term of type {\type} using the proof editing mode. It -behaves as {\tt Theorem} but is intended for the interactive -definition of expression which computational behavior will be used by -further commands. \SeeAlso~\ref{Transparent} and \ref{unfold}. +\item {\tt Definition {\ident} \zeroone{\binders} : {\type}.} + +This allows to define a term of type {\type} using the proof editing mode. It +behaves as {\tt Theorem} but is intended to be used in conjunction with + {\tt Defined} (see \ref{Defined}) in order to define a + constant of which the computational behavior is relevant. + +The command can be used also with {\tt Example} instead +of {\tt Definition}. + +\SeeAlso Sections~\ref{Opaque} and~\ref{Transparent} ({\tt Opaque} +and {\tt Transparent}) and~\ref{unfold} (tactic {\tt unfold}). + +\item {\tt Let {\ident} \zeroone{\binders} : {\type}.} + +Like {\tt Definition {\ident} \zeroone{\binders} : {\type}.} except +that the definition is turned into a local definition generalized over +the declarations depending on it after closing the current section. + +\item {\tt Fixpoint \nelist{{\ident} {\binders} \zeroone{\annotation} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} +\comindex{Fixpoint} + +This generalizes the syntax of {\tt Fixpoint} so that one or more +bodies can be defined interactively using the proof editing mode (when +a body is omitted, its type is mandatory in the syntax). When the +block of proofs is completed, it is intended to be ended by {\tt + Defined}. + +\item {\tt CoFixpoint \nelist{{\ident} \zeroone{\binders} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} +\comindex{CoFixpoint} + +This generalizes the syntax of {\tt CoFixpoint} so that one or more bodies +can be defined interactively using the proof editing mode. + \end{Variants} -\subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} +\subsubsection{{\tt Proof.} {\dots} {\tt Qed.} \comindex{Proof} -\comindex{Qed} -\comindex{Defined} -\comindex{Save} -\comindex{Goal} -\comindex{Admitted}} +\comindex{Qed}} A proof starts by the keyword {\tt Proof}. Then {\Coq} enters the proof editing mode until the proof is completed. The proof editing @@ -1623,33 +1655,38 @@ environment using the keyword {\tt Qed}. \end{enumerate} \begin{Remarks} -\item Several statements can be simultaneously opened. -\item Not only other statements but any vernacular command can be given -within the proof editing mode. In this case, the command is +\item Several statements can be simultaneously asserted. +\item Not only other assertions but any vernacular command can be given +while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the statements still to be proved. \item {\tt Proof} is recommended but can currently be omitted. On the -opposite, {\tt Qed} (or {\tt Defined}, see below) is mandatory to validate a proof. -\item Proofs ended by {\tt Qed} are declared opaque (see \ref{Opaque}) -and cannot be unfolded by conversion tactics (see \ref{Conversion-tactics}). -To be able to unfold a proof, you should end the proof by {\tt Defined} - (see below). +opposite side, {\tt Qed} (or {\tt Defined}, see below) is mandatory to +validate a proof. +\item Proofs ended by {\tt Qed} are declared opaque. Their content + cannot be unfolded (see \ref{Conversion-tactics}), thus realizing + some form of {\em proof-irrelevance}. To be able to unfold a proof, + the proof should be ended by {\tt Defined} (see below). \end{Remarks} \begin{Variants} -\item {\tt Proof} {\tt .} \dots {\tt Defined} {\tt .}\\ - Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but the proof is - then declared transparent (see \ref{Transparent}), which means it - can be unfolded in conversion tactics (see \ref{Conversion-tactics}). -\item {\tt Proof} {\tt .} \dots {\tt Save.}\\ - Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} -\item {\tt Goal} \type \dots {\tt Save} \ident \\ - Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.} - This is intended to be used in the interactive mode. Conversely to named - lemmas, anonymous goals cannot be nested. -\item {\tt Proof.} \dots {\tt Admitted.}\\ - Turns the current conjecture into an axiom and exits editing of - current proof. +\item \comindex{Defined} + {\tt Proof.} {\dots} {\tt Defined.}\\ + Same as {\tt Proof.} {\dots} {\tt Qed.} but the proof is + then declared transparent, which means that its + content can be explicitly used for type-checking and that it + can be unfolded in conversion tactics (see + \ref{Conversion-tactics}, \ref{Opaque}, \ref{Transparent}). +%Not claimed to be part of Gallina... +%\item {\tt Proof.} {\dots} {\tt Save.}\\ +% Same as {\tt Proof.} {\dots} {\tt Qed.} +%\item {\tt Goal} \type {\dots} {\tt Save} \ident \\ +% Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.} +% This is intended to be used in the interactive mode. +\item \comindex{Admitted} + {\tt Proof.} {\dots} {\tt Admitted.}\\ + Turns the current asserted statement into an axiom and exits the + proof mode. \end{Variants} % Local Variables: diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 7caf6126e..8847d058a 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -416,8 +416,7 @@ data-type. In technical terms, one says that \verb:sig: is a ``weak (dependent) sum''. A variant \verb:sig2: with two predicates is also provided. -\index{\{x:A "| (P x)\}} -\index{"|} +\ttindex{\{x:A $\mid$ (P x)\}} \ttindex{sig} \ttindex{exist} \ttindex{sig2} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index eff98d588..68d572265 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -160,9 +160,9 @@ This command is used to start an interactive module type {\ident}. is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} -\item {\tt {\declarationkeyword} Inline {\assums} } +\item {\tt {\assumptionkeyword} Inline {\assums} } - This declaration will be automatically unfolded at functor + The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a $!$ annotation. \end{enumerate} \subsection{\tt End {\ident} diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index f66416336..34f982378 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -570,7 +570,7 @@ This command displays the list of library files loaded in the current imported. \subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}} -This commands loads the Objective Caml compiled files {\str$_1$} \dots +This commands loads the Objective Caml compiled files {\str$_1$} {\dots} {\str$_n$} (dynamic link). It is mainly used to load tactics dynamically. % (see Chapter~\ref{WritingTactics}). @@ -778,7 +778,7 @@ Chapter~\ref{Proof-handling}). command. \item $\num_2$ is the proof state number after the last command. -\item $id_1$ $id_2$ \dots $id_n$ are the currently opened proof names +\item $id_1$ $id_2$ {\dots} $id_n$ are the currently opened proof names (order not significant). \end{itemize} @@ -943,13 +943,13 @@ computation of algebraic values, such as numbers, and for reflexion-based tactics. The commands to fine-tune the reduction strategies and the lazy conversion algorithm are described first. -\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} +\subsection[\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.]{\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command has an effect on unfoldable constants, i.e. on constants defined by {\tt Definition} or {\tt Let} (with an explicit body), or by a command assimilated to a definition such as {\tt Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt Defined}. The command tells not to unfold -the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using +the constants {\qualid$_1$} {\dots} {\qualid$_n$} in tactics using $\delta$-conversion (unfolding a constant is replacing it by its definition). @@ -959,7 +959,7 @@ case {\Coq} has to check the conversion (see Section~\ref{conv-rules}) of two distinct applied constants. The scope of {\tt Opaque} is limited to the current section, or -current file, unless the variant {\tt Global Opaque \qualid$_1$ \dots +current file, unless the variant {\tt Global Opaque \qualid$_1$ {\dots} \qualid$_n$} is used. \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing}, @@ -973,7 +973,7 @@ environment}\\ and if \texttt{bar} does not exist, \texttt{foo} is set opaque. \end{ErrMsgs} -\subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}} +\subsection[\tt Transparent \qualid$_1$ {\dots} \qualid$_n$.]{\tt Transparent \qualid$_1$ {\dots} \qualid$_n$.\comindex{Transparent}\label{Transparent}} This command is the converse of {\tt Opaque} and it applies on unfoldable constants to restore their unfoldability after an {\tt Opaque} command. @@ -1001,12 +1001,12 @@ environment}\\ \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing}, \ref{Theorem} -\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$ +\subsection{\tt Strategy {\it level} [ \qualid$_1$ {\dots} \qualid$_n$ ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}} This command generalizes the behavior of {\tt Opaque} and {\tt Transparent} commands. It is used to fine-tune the strategy for unfolding constants, both at the tactic level and at the kernel -level. This command associates a level to \qualid$_1$ \dots +level. This command associates a level to \qualid$_1$ {\dots} \qualid$_n$. Whenever two expressions with two distinct head constants are compared (for instance, this comparison can be triggered by a type cast), the one with lower level is expanded first. In case 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" diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3593e9751..8fb055654 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1341,7 +1341,7 @@ applicative subterms whose head occurrence is {\ident}. \label{unfold}} This tactic applies to any goal. The argument {\qualid} must denote a -defined transparent constant or local definition (see Sections~\ref{Simpl-definitions} and~\ref{Transparent}). The tactic {\tt +defined transparent constant or local definition (see Sections~\ref{Basic-definitions} and~\ref{Transparent}). The tactic {\tt unfold} applies the $\delta$ rule to each occurrence of the constant to which {\qualid} refers in the current goal and then replaces it with its $\beta\iota$-normal form. @@ -4182,7 +4182,7 @@ general principle of mutual induction for objects in type {\term$_i$}. \comindex{Set Elimination Schemes} It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the - {\tt UnSet Elimination Schemes} command. It may be + {\tt Unset Elimination Schemes} command. It may be reactivated at any time with {\tt Set Elimination Schemes}. \\ |