aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/RefMan-cic.tex263
-rw-r--r--doc/refman/RefMan-com.tex225
-rw-r--r--doc/refman/RefMan-ext.tex2
-rw-r--r--doc/refman/RefMan-lib.tex13
-rw-r--r--doc/refman/RefMan-ltac.tex2
-rw-r--r--doc/refman/RefMan-pre.tex3
-rw-r--r--doc/refman/RefMan-pro.tex13
-rw-r--r--doc/refman/RefMan-syn.tex10
-rw-r--r--doc/refman/RefMan-tac.tex319
9 files changed, 570 insertions, 280 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1554ee04d3..b9c17d8148 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -544,32 +544,109 @@ $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of param
\def\colon{@{\hskip.5em:\hskip.5em}}
The declaration for parameterized lists is:
+\begin{latexonly}
\vskip.5em
-\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l}
- \Nil & \forall A:\Set,\List~A \\
- \cons & \forall A:\Set, A \ra \List~A \ra \List~A
- \end{array}\right]}
+\ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r \colon l}
+ \Nil & \forall A:\Set,\List~A \\
+ \cons & \forall A:\Set, A \ra \List~A \ra \List~A
+ \end{array}
+ \right]}
\vskip.5em
-
-which corresponds to the result of the \Coq\ declaration:
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎝</td>
+ <td style="width:120pt;text-align:center">[ <span style="font-family:monospace">list : Set → Set</span> ]</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">nil</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="text-align:left;font-family:monospace">∀A : Set, list A</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">cons</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="text-align:left;font-family:monospace">∀A : Set, A → list A → list A</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\ declaration:
\begin{coq_example*}
Inductive list (A:Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.
\end{coq_example*}
-The declaration for a mutual inductive definition of forests and trees is:
+\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is:
+\begin{latexonly}
\vskip.5em
-\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
- {\left[\begin{array}{r \colon l}
- \node & \forest \ra \tree\\
- \emptyf & \forest\\
- \consf & \tree \ra \forest \ra \forest\\
- \end{array}\right]}
+\ind{~}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
+ {\left[\begin{array}{r \colon l}
+ \node & \forest \ra \tree\\
+ \emptyf & \forest\\
+ \consf & \tree \ra \forest \ra \forest\\
+ \end{array}\right]}
\vskip.5em
-
-which corresponds to the result of the \Coq\
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">tree</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">Set</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">forest</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">Set</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">node</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">forest → tree</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">emptyf</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">forest</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">consf</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">tree → forest → forest</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\
declaration:
\begin{coq_example*}
Inductive tree : Set :=
@@ -579,7 +656,8 @@ with forest : Set :=
| consf : tree -> forest -> forest.
\end{coq_example*}
-The declaration for a mutual inductive definition of even and odd is:
+\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is:
+\begin{latexonly}
\newcommand\GammaI{\left[\begin{array}{r \colon l}
\even & \nat\ra\Prop \\
\odd & \nat\ra\Prop
@@ -594,7 +672,55 @@ The declaration for a mutual inductive definition of even and odd is:
\vskip.5em
\ind{1}{\GammaI}{\GammaC}
\vskip.5em
-which corresponds to the result of the \Coq\
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">nat → Prop</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">odd</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">nat → Prop</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even_O</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">even O</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even_S</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">∀n : nat, odd n → even (S n)</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">odd_S</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">∀n : nat, even n → odd (S n)</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
+\noindent which corresponds to the result of the \Coq\
declaration:
\begin{coq_example*}
Inductive even : nat -> Prop :=
@@ -610,9 +736,9 @@ contains an inductive declaration.
\begin{description}
\item[Ind] \index{Typing rules!Ind}
- \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
+ \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
\item[Constr] \index{Typing rules!Constr}
- \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
+ \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
\end{description}
\begin{latexonly}%
@@ -726,19 +852,16 @@ any $u_i$
the type $V$ satisfies the nested positivity condition for $X$
\end{itemize}
-%% \begin{latexonly}%
- \newcommand\vv{\textSFxi} % │
- \newcommand\hh{\textSFx} % ─
- \newcommand\vh{\textSFviii} % ├
- \newcommand\hv{\textSFii} % └
- \newlength\framecharacterwidth
- \settowidth\framecharacterwidth{\hh}
- \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
- \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-%% \def\captionstrut{\vbox to 1.5em{}}
+\newcommand\vv{\textSFxi} % │
+\newcommand\hh{\textSFx} % ─
+\newcommand\vh{\textSFviii} % ├
+\newcommand\hv{\textSFii} % └
+\newlength\framecharacterwidth
+\settowidth\framecharacterwidth{\hh}
+\newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
+\newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-%% \begin{figure}[H]
-For instance, if one considers the type
+\noindent For instance, if one considers the type
\begin{verbatim}
Inductive tree (A:Type) : Type :=
@@ -746,29 +869,49 @@ Inductive tree (A:Type) : Type :=
| node : A -> (nat -> tree A) -> tree A
\end{verbatim}
-Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$
-
+\begin{latexonly}
+\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\
\noindent
- \ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
- \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
- \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
- \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
- \ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
- \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
-%% \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
-%% \end{figure}
-%% \end{latexonly}%
+\ws\ws\vv\\
+\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
+\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
+\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
+\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
+\ws\ws\vv\\
+\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
+\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
+\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+\end{latexonly}
+\begin{rawhtml}
+<pre>
+<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span>
+ │
+ ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span>
+ │ <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span>
+ │ <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span>
+ │ <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span>
+ │
+ ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span>
+ <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span>
+ <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span>
+ │
+ ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
+</pre>
+\end{rawhtml}
\paragraph{Correctness rules.}
We shall now describe the rules allowing the introduction of a new
@@ -783,7 +926,7 @@ inductive definition.
\inference{
\frac{
(\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots k}
- ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n}
+ ~~~~~~~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n}
}
{\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
provided that the following side conditions hold:
@@ -811,23 +954,23 @@ inductive definition.
The following declaration introduces the second-order existential
quantifier $\exists X.P(X)$.
\begin{coq_example*}
-Inductive exProp (P:Prop->Prop) : Prop
- := exP_intro : forall X:Prop, P X -> exProp P.
+Inductive exProp (P:Prop->Prop) : Prop :=
+ exP_intro : forall X:Prop, P X -> exProp P.
\end{coq_example*}
The same definition on \Set{} is not allowed and fails:
% (********** The following is not correct and should produce **********)
% (*** Error: Large non-propositional inductive types must be in Type***)
\begin{coq_example}
-Fail Inductive exSet (P:Set->Prop) : Set
- := exS_intro : forall X:Set, P X -> exSet P.
+Fail Inductive exSet (P:Set->Prop) : Set :=
+ exS_intro : forall X:Set, P X -> exSet P.
\end{coq_example}
It is possible to declare the same inductive definition in the
universe \Type.
The \texttt{exType} inductive definition has type $(\Type_i \ra\Prop)\ra
\Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $k<j$ and $k\leq i$.
\begin{coq_example*}
-Inductive exType (P:Type->Prop) : Type
- := exT_intro : forall X:Type, P X -> exType P.
+Inductive exType (P:Type->Prop) : Type :=
+ exT_intro : forall X:Type, P X -> exType P.
\end{coq_example*}
%We shall assume for the following definitions that, if necessary, we
%annotated the type of constructors such that we know if the argument
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8bb1cc331b..6f85849888 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -5,9 +5,9 @@
There are three \Coq~commands:
\begin{itemize}
-\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ;
-\item {\tt coqc} : The \Coq\ compiler (batch compilation).
-\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
+\item {\tt coqtop}: the \Coq\ toplevel (interactive mode);
+\item {\tt coqc}: the \Coq\ compiler (batch compilation);
+\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries).
\end{itemize}
The options are (basically) the same for the first two commands, and
roughly described below. You can also look at the \verb!man! pages of
@@ -39,11 +39,10 @@ The {\tt coqc} command takes a name {\em file} as argument. Then it
looks for a vernacular file named {\em file}{\tt .v}, and tries to
compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
-\Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the Section~\ref{lexical}. It
-must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+.
+\Warning The name {\em file} should be a regular {\Coq} identifier, as
+defined in Section~\ref{lexical}. It should contain only letters, digits
+or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but
+\verb+/bar/foo/to-to.v+ is invalid.
\section[Customization]{Customization at launch time}
@@ -64,7 +63,7 @@ directories to the load path of \Coq.
It is possible to skip the loading of the resource file with the
option \verb:-q:.
-\section{By environment variables\label{EnvVariables}
+\subsection{By environment variables\label{EnvVariables}
\index{Environment variables}\label{envars}}
Load path can be specified to the \Coq\ system by setting up
@@ -93,13 +92,13 @@ The following command-line options are recognized by the commands {\tt
coqc} and {\tt coqtop}, unless stated otherwise:
\begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ %
-Add physical path {\em directory} to the {\ocaml} loadpath.
+ Add physical path {\em directory} to the {\ocaml} loadpath.
\SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
-\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+\item[{\tt -Q} {\em directory} {\dirpath}]\ %
Add physical path \emph{directory} to the list of directories where
{\Coq} looks for a file and bind it to the the logical directory
@@ -109,147 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
\SeeAlso Section~\ref{Libraries}.
-\item[{\tt -R} {\em directory} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}]\ %
Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
subdirectory structure of \emph{directory} recursively visible so
that the recursive contents of physical \emph{directory} is available
from {\Coq} using short or partially qualified names.
-
+
\SeeAlso Section~\ref{Libraries}.
-\item[{\tt -top} {\dirpath}, {\tt -notop}]\
+\item[{\tt -top} {\dirpath}]\ %
+
+ Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not
+ valid for {\tt coqc} as the toplevel module name is inferred from the
+ name of the output file.
+
+\item[{\tt -notop}]\ %
+
+ Use the empty logical path for the toplevel module name instead of {\tt
+ Top}. Not valid for {\tt coqc} as the toplevel module name is
+ inferred from the name of the output file.
+
+\item[{\tt -exclude-dir} {\em directory}]\ %
- This sets the toplevel module name to {\dirpath}/the empty logical path instead
- of {\tt Top}. Not valid for {\tt coqc}.
+ Exclude any subdirectory named {\em directory} while
+ processing options such as {\tt -R} and {\tt -Q}. By default, only the
+ conventional version control management directories named {\tt CVS} and
+ {\tt \_darcs} are excluded.
-\item[{\tt -exclude-dir} {\em subdirectory}]\
+\item[{\tt -nois}]\ %
- This tells to exclude any subdirectory named {\em subdirectory}
- while processing option {\tt -R}. Without this option only the
- conventional version control management subdirectories named {\tt
- CVS} and {\tt \_darcs} are excluded.
+ Start from an empty state instead of loading the {\tt Init.Prelude}
+ module.
-\item[{\tt -nois}]\
+\item[{\tt -init-file} {\em file}]\ %
- Cause \Coq~to begin with an empty state.
+ Load {\em file} as the resource file instead of loading the default
+ resource file from the standard configuration directories.
-\item[{\tt -init-file} {\em file}, {\tt -q}]\
+\item[{\tt -q}]\ %
- Take {\em file} as the resource file. /
- Cause \Coq~not to load the resource file.
+ Do not to load the default resource file.
-\item[{\tt -load-ml-source} {\em file}]\
+\item[{\tt -load-ml-source} {\em file}]\ %
Load the {\ocaml} source file {\em file}.
-\item[{\tt -load-ml-object} {\em file}]\
+\item[{\tt -load-ml-object} {\em file}]\ %
Load the {\ocaml} object file {\em file}.
-\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\
+\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ %
+
+ Load and execute the {\Coq} script from {\em file.v}.
+
+\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em
+ file}]\ %
+
+ Load and execute the {\Coq} script from {\em file.v}.
+ Output its content on the standard input as it is executed.
+
+\item[{\tt -load-vernac-object} {\dirpath}]\ %
+
+ Load \Coq~compiled library {\dirpath}. This is equivalent to running
+ {\tt Require} {\dirpath}.
- Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
- standard input.
+\item[{\tt -require} {\dirpath}]\ %
-\item[{\tt -load-vernac-object} {\em path}]\
+ Load \Coq~compiled library {\dirpath} and import it. This is equivalent
+ to running {\tt Require Import} {\dirpath}.
- Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
+\item[{\tt -batch}]\ %
-\item[{\tt -require} {\em path}]\
+ Exit just after argument parsing. Available for {\tt coqtop} only.
- Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
- Require Import} {\em path}).
+\item[{\tt -compile} {\em file.v}]\ %
-\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\
+ Compile file {\em file.v} into {\em file.vo}. This options imply {\tt
+ -batch} (exit just after argument parsing). It is available only
+ for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}.
- {\tt coqtop} options only used internally by {\tt coqc}.
+\item[{\tt -compile-verbose} {\em file.v}]\ %
- This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
- copy of the contents of the file on standard input. This option implies options
- {\tt -batch} (exit just after arguments parsing). It is only
- available for {\tt coqtop}.
+ Same as {\tt -compile} but also output the content of {\em file.v} as
+ it is compiled.
-\item[{\tt -verbose}]\
+\item[{\tt -verbose}]\ %
- This option is only for {\tt coqc}. It tells to compile the file with
- a copy of its contents on standard input.
+ Output the content of the input file as it is compiled. This option is
+ available for {\tt coqc} only; it is the counterpart of {\tt
+ -compile-verbose}.
%Mostly unused in the code
-%\item[{\tt -debug}]\
+%\item[{\tt -debug}]\ %
%
% Switch on the debug flag.
-\item[{\tt -with-geoproof} (yes|no)]\
+\item[{\tt -with-geoproof} (yes|no)]\ %
- Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
+ Enable or not special functions for Geoproof within {\CoqIDE} (default
+ is yes).
-\item[{\tt -color} (on|off|auto)]\
+\item[{\tt -color} (on|off|auto)]\ %
- Activate or not the coloring of output of {\tt coqtop}. The default, auto,
- means that {\tt coqtop} will dynamically decide whether to activate it
- depending if the output channels of {\tt coqtop} can handle ANSI styles.
+ Enable or not the coloring of output of {\tt coqtop}. Default is auto,
+ meaning that {\tt coqtop} dynamically decides, depending on whether the
+ output channel supports ANSI escape sequences.
-\item[{\tt -beautify}]\
+\item[{\tt -beautify}]\ %
- While compiling {\em file}, pretty prints each command just after having parsing
- it in {\em file}{\tt .beautified} in order to get old-fashion
- syntax/definitions/notations.
+ Pretty-print each command to {\em file.beautified} when compiling {\em
+ file.v}, in order to get old-fashioned syntax/definitions/notations.
-\item[{\tt -emacs}, {\tt -ide-slave}]\
+\item[{\tt -emacs}, {\tt -ide-slave}]\ %
- Start a special main loop to communicate with ide.
+ Start a special toplevel to communicate with a specific IDE.
-\item[{\tt -impredicative-set}]\
+\item[{\tt -impredicative-set}]\ %
Change the logical theory of {\Coq} by declaring the sort {\tt Set}
- impredicative; warning: this is known to be inconsistent with
+ impredicative. Warning: this is known to be inconsistent with
some standard axioms of classical mathematics such as the functional
- axiom of choice or the principle of description
+ axiom of choice or the principle of description.
-\item[{\tt -type-in-type}]\
+\item[{\tt -type-in-type}]\ %
- This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+ Collapse the universe hierarchy of {\Coq}. Warning: this makes the
+ logic inconsistent.
-\item[{\tt -compat} {\em version}] \mbox{}
+\item[{\tt -compat} {\em version}]\ %
- Attempt to maintain some of the incompatible changes in their {\em version}
- behavior.
+ Attempt to maintain some backward-compatibility with a previous version.
-\item[{\tt -dump-glob} {\em file}]\
+\item[{\tt -dump-glob} {\em file}]\ %
- This dumps references for global names in file {\em file}
- (to be used by coqdoc, see~\ref{coqdoc})
+ Dump references for global names in file {\em file} (to be used
+ by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being
+ compiled, {\em file.glob} is used.
-\item[{\tt -no-hash-consing}] \mbox{}
+\item[{\tt -no-glob}]\ %
-\item[{\tt -image} {\em file}]\
+ Disable the dumping of references for global names.
- This option sets the binary image to be used by {\tt coqc} to be {\em file}
+%\item[{\tt -no-hash-consing}]\ %
+
+\item[{\tt -image} {\em file}]\ %
+
+ Set the binary image to be used by {\tt coqc} to be {\em file}
instead of the standard one. Not of general use.
-\item[{\tt -bindir} {\em directory}]\
+\item[{\tt -bindir} {\em directory}]\ %
+
+ Set the directory containing {\Coq} binaries to be used by {\tt coqc}.
+ It is equivalent to doing \texttt{export COQBIN=}{\em directory} before
+ launching {\tt coqc}.
+
+\item[{\tt -where}]\ %
+
+ Print the location of \Coq's standard library and exit.
- Set for {\tt coqc} the directory containing \Coq\ binaries.
- It is equivalent to do \texttt{export COQBIN=}{\em directory}
- before launching {\tt coqc}.
+\item[{\tt -config}]\ %
-\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\
+ Print the locations of \Coq's binaries, dependencies, and libraries, then exit.
- Print the \Coq's standard library location or \Coq's binaries, dependencies,
- libraries locations or the list of command line arguments that {\tt coqtop} has
- recognize as options and exit.
+\item[{\tt -filteropts}]\ %
-\item[{\tt -v}]\
+ Print the list of command line arguments that {\tt coqtop} has
+ recognized as options and exit.
- Print the \Coq's version and exit.
+\item[{\tt -v}]\ %
-\item[{\tt -list-tags}]\
+ Print \Coq's version and exit.
- Print the highlight tags known by \Coq as well as their currently associated
- color.
+\item[{\tt -list-tags}]\ %
-\item[{\tt -h}, {\tt --help}]\
+ Print the highlight tags known by {\Coq} as well as their currently associated
+ color and exit.
+
+\item[{\tt -h}, {\tt --help}]\ %
Print a short usage and exit.
@@ -293,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
{\tt -impredicative-set} are supported by {\tt coqchk} and have the
same meaning as for {\tt coqtop}. Extra options are:
\begin{description}
-\item[{\tt -norec} $module$]\
+\item[{\tt -norec} {\em module}]\ %
+
+ Check {\em module} but do not check its dependencies.
- Check $module$ but do not force check of its dependencies.
-\item[{\tt -admit} $module$] \
+\item[{\tt -admit} {\em module}]\ %
- Do not check $module$ and any of its dependencies, unless
+ Do not check {\em module} and any of its dependencies, unless
explicitly required.
-\item[{\tt -o}]\
+
+\item[{\tt -o}]\ %
At exit, print a summary about the context. List the names of all
assumptions and variables (constants without body).
-\item[{\tt -silent}]\
+
+\item[{\tt -silent}]\ %
Do not write progress information in standard output.
\end{description}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f2ab79dced..51e881bff4 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -2014,7 +2014,7 @@ variables, use
Instead of letting the unification engine try to solve an existential variable
by itself, one can also provide an explicit hole together with a tactic to solve
-it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a
+it. Using the syntax {\tt ltac:(\expr)}, the user can put a
tactic anywhere a term is expected. The order of resolution is not specified and
is implementation-dependent. The inner tactic may use any variable defined in
its scope, including repeated alternations between variables introduced by term
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b6..4ebb484e7c 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -17,10 +17,11 @@ The \Coq\ library is structured into two parts:
In addition, user-provided libraries or developments are provided by
\Coq\ users' community. These libraries and developments are available
-for download at \texttt{http://coq.inria.fr} (see
+for download at \url{http://coq.inria.fr} (see
Section~\ref{Contributions}).
-The chapter briefly reviews the \Coq\ libraries.
+The chapter briefly reviews the \Coq\ libraries whose contents can
+also be browsed at \url{http://coq.inria.fr/stdlib}.
\section[The basic library]{The basic library\label{Prelude}}
@@ -799,7 +800,9 @@ At the end, it defines data-types at the {\Type} level.
\subsection{Tactics}
A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}.
+state\footnote{This is in module {\tt Tactics.v}}. They are listed at
+\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
+ Tactics}).
\section{The standard library}
@@ -842,7 +845,7 @@ Chapter~\ref{Other-commands}).
The different modules of the \Coq\ standard library are described in the
additional document \verb!Library.dvi!. They are also accessible on the WWW
through the \Coq\ homepage
-\footnote{\texttt{http://coq.inria.fr}}.
+\footnote{\url{http://coq.inria.fr}}.
\subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
@@ -1035,7 +1038,7 @@ intros; split_Rmult.
\end{itemize}
-All this tactics has been written with the tactic language Ltac
+These tactics has been written with the tactic language Ltac
described in Chapter~\ref{TacticLanguage}.
\begin{coq_eval}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index cc7e6b53bf..12dea9a306 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1116,6 +1116,8 @@ Defined {\ltac} functions can be displayed using the command
{\tt Print Ltac {\qualid}.}
\end{quote}
+The command {\tt Print Ltac Signatures\comindex{Print Ltac Signatures}} displays a list of all user-defined tactics, with their arguments.
+
\section{Debugging {\ltac} tactics}
\subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e0dc496666..cb2ab5dc2f 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1080,8 +1080,7 @@ Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
-Ripault, Carst Tankink. Maxime Dénès brilliantly coordinated the
-release process.
+Ripault, Carst Tankink. Maxime Dénès coordinated the release process.
\begin{flushright}
Paris, January 2015, revised December 2015,\\
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index ed1b79e56e..c37367de5b 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -407,6 +407,19 @@ Proof.
\end{ErrMsgs}
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
\section{Requesting information}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index aabc8a8995..1f08b6a2f1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -358,7 +358,7 @@ state of {\Coq}.
Reserved Notation "x = y" (at level 70, no associativity).
\end{coq_example}
-Reserving a notation is also useful for simultaneously defined an
+Reserving a notation is also useful for simultaneously defining an
inductive type or a recursive constant and a notation for it.
\Rem The notations mentioned on Figure~\ref{init-notations} are
@@ -860,11 +860,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type
{\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
recognized as an argument to be interpreted in scope {\scope}.
-\comindex{Bind Scope}
-Any global reference can be bound by default to an
-interpretation scope. The command to do it is
+\comindex{Bind Scope}
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+bound to an interpretation scope. The command to do it is
\begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
+{\tt Bind Scope} {\scope} \texttt{with} {\class}
\end{quote}
\Example
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f268d82764..54450fe7dc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -802,7 +802,7 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
\end{Variants}
-\subsection{\tt intros {\intropattern} \mbox{\dots} \intropattern}
+\subsection{\tt intros {\intropatternlist}}
\label{intros-pattern}
\tacindex{intros \intropattern}
\index{Introduction patterns}
@@ -811,9 +811,11 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
\index{Disjunctive/conjunctive introduction patterns}
\index{Equality introduction patterns}
-
-This extension of the tactic {\tt intros} combines introduction of
-variables or hypotheses and case analysis. An {\em introduction pattern} is
+This extension of the tactic {\tt intros} allows to apply tactics on
+the fly on the variables or hypotheses which have been introduced. An
+{\em introduction pattern list} {\intropatternlist} is a list of
+introduction patterns possibly containing the filling introduction
+patterns {\tt *} and {\tt **}. An {\em introduction pattern} is
either:
\begin{itemize}
\item a {\em naming introduction pattern}, i.e. either one of:
@@ -827,7 +829,7 @@ either:
\item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
\begin{itemize}
\item a disjunction of lists of patterns:
- {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
+ {\tt [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}
\item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
\item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
for sequence of right-associative binary constructs
@@ -844,10 +846,6 @@ either:
\item the wildcard: {\tt \_}
\end{itemize}
-Introduction patterns can be combined into lists. An {\em introduction
- pattern list} is a list of introduction patterns possibly containing
-the filling introduction patterns {\tt *} and {\tt **}.
-
Assuming a goal of type $Q \to P$ (non-dependent product), or
of type $\forall x:T,~P$ (dependent product), the behavior of
{\tt intros $p$} is defined inductively over the structure of the
@@ -860,20 +858,22 @@ introduction pattern~$p$:
\item introduction on \texttt{\ident} behaves as described in
Section~\ref{intro};
\item introduction over a disjunction of list of patterns {\tt
- [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
- expects the product to be over an inductive type
- whose number of constructors is $n$ (or more generally over a type
- of conclusion an inductive type built from $n$ constructors,
- e.g. {\tt C -> A\textbackslash/B if $n=2$}): it destructs the introduced
- hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
- applies on each generated subgoal the corresponding tactic;
- \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
- pattern is part of a sequence of patterns and is not the last
- pattern of the sequence, then {\Coq} completes the pattern so that all
- the argument of the constructors of the inductive type are
- introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
- applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
- the list of patterns {\tt [$\,$|$\,$?$\,$] H});
+ [$\intropatternlist_{1}$ | \dots\ | $\intropatternlist_n$]} expects
+ the product to be over an inductive type whose number of
+ constructors is $n$ (or more generally over a type of conclusion an
+ inductive type built from $n$ constructors, e.g. {\tt C ->
+ A\textbackslash/B} with $n=2$ since {\tt A\textbackslash/B} has 2
+ constructors): it destructs the introduced hypothesis as {\tt
+ destruct} (see Section~\ref{destruct}) would and applies on each
+ generated subgoal the corresponding tactic;
+ \texttt{intros}~$\intropatternlist_i$. The introduction patterns in
+ $\intropatternlist_i$ are expected to consume no more than the
+ number of arguments of the $i^{\mbox{\scriptsize th}}$
+ constructor. If it consumes less, then {\Coq} completes the pattern
+ so that all the arguments of the constructors of the inductive type
+ are introduced (for instance, the list of patterns {\tt [$\;$|$\;$]
+ H} applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same
+ as the list of patterns {\tt [$\,$|$\,$?$\,$] H});
\item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
$p_n$)} expects the goal to be a product over an inductive type $I$ with a
single constructor that itself has at least $n$ arguments: it
@@ -887,10 +887,10 @@ introduction pattern~$p$:
{\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
hypothesis to be a sequence of right-associative binary inductive
constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
- hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+ hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be
introduced via pattern {\tt (a \& x \& b \& c \& d)};
\item if the product is over an equality type, then a pattern of the
- form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
+ form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
(see Section~\ref{injection}) or {\tt discriminate} (see
Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt
injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are
@@ -925,19 +925,6 @@ introduction pattern~$p$:
not any more a quantification or an implication.
\end{itemize}
-Then, if $p_1$ ... $p_n$ is a list of introduction patterns possibly
-containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
-\begin{itemize}
-\item introduction over {\tt *} introduces all forthcoming quantified
- variables appearing in a row;
-\item introduction over {\tt **} introduces all forthcoming quantified
- variables or hypotheses until the goal is not any more a
- quantification or an implication;
-\item introduction over an introduction pattern $p$ introduces the
- forthcoming quantified variables or premise of the goal and applies
- the introduction pattern $p$ to it.
-\end{itemize}
-
\Example
\begin{coq_example}
@@ -948,28 +935,38 @@ intros * [a | (_,c)] f.
Abort.
\end{coq_eval}
-\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
-\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
-\begin{itemize}
-\item A wildcard pattern never succeeds when applied isolated on a
- dependent product, while it succeeds as part of a list of
- introduction patterns if the hypotheses that depends on it are
- erased too.
-\item A disjunctive or conjunctive pattern followed by an introduction
- pattern forces the introduction in the context of all arguments of
- the constructors before applying the next pattern while a terminal
- disjunctive or conjunctive pattern does not. Here is an example
+\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
+ $p_1$;\ldots; intros $p_n$} for the following reason: If one of the
+$p_i$ is a wildcard pattern, he might succeed in the first case
+because the further hypotheses it depends in are eventually erased too
+while it might fail in the second case because of dependencies in
+hypotheses which are not yet introduced (and a fortiori not yet
+erased).
+
+\Rem In {\tt intros $\intropatternlist$}, if the last introduction
+pattern is a disjunctive or conjunctive pattern {\tt
+ [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}, the
+completion of $\intropatternlist_i$ so that all the arguments of the
+$i^{\mbox{\scriptsize th}}$ constructors of the corresponding
+inductive type are introduced can be controlled with the
+following option:
+\optindex{Bracketing Last Introduction Pattern}
+
+\begin{quote}
+{\tt Set Bracketing Last Introduction Pattern}
+\end{quote}
+
+Force completion, if needed, when the last introduction pattern is a
+disjunctive or conjunctive pattern (this is the default).
+
+\begin{quote}
+{\tt Unset Bracketing Last Introduction Pattern}
+\end{quote}
+
+Deactivate completion when the last introduction pattern is a disjunctive
+or conjunctive pattern.
-\begin{coq_example}
-Goal forall n:nat, n = 0 -> n = 0.
-intros [ | ] H.
-Show 2.
-Undo.
-intros [ | ]; intros H.
-Show 2.
-\end{coq_example}
-\end{itemize}
\subsection{\tt clear \ident}
\tacindex{clear}
@@ -1459,6 +1456,24 @@ a hypothesis or in the body or the type of a local definition.
\end{Variants}
+\subsection{\tt admit}
+\tacindex{admit}
+\tacindex{give\_up}
+\label{admit}
+
+The {\tt admit} tactic allows temporarily skipping a subgoal so as to
+progress further in the rest of the proof. A proof containing
+admitted goals cannot be closed with {\tt Qed} but only with
+{\tt Admitted}.
+
+\begin{Variants}
+
+ \item {\tt give\_up}
+
+ Synonym of {\tt admit}.
+
+\end{Variants}
+
\subsection{\tt absurd \term}
\tacindex{absurd}
\label{absurd}
@@ -2818,42 +2833,57 @@ This tactic is deprecated. It can be replaced by {\tt enough}
\tacindex{subst}
\optindex{Regular Subst Tactic}
-This tactic applies to a goal that has \ident\ in its context and
-(at least) one hypothesis, say {\tt H}, of type {\tt
- \ident=t} or {\tt t=\ident}. Then it replaces
-\ident\ by {\tt t} everywhere in the goal (in the hypotheses
-and in the conclusion) and clears \ident\ and {\tt H} from the context.
+This tactic applies to a goal that has \ident\ in its context and (at
+least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$
+{\tt = \ident} with {\ident} not occurring in $t$. Then it replaces
+{\ident} by $t$ everywhere in the goal (in the hypotheses and in the
+conclusion) and clears {\ident} and $H$ from the context.
+
+If {\ident} is a local definition of the form {\ident} := $t$, it is
+also unfolded and cleared.
\Rem
-When several hypotheses have the form {\tt \ident=t} or {\tt
- t=\ident}, the first one is used.
+When several hypotheses have the form {\tt \ident} = $t$ or {\tt
+ $t$ = \ident}, the first one is used.
+
+\Rem
+If $H$ is itself dependent in the goal, it is replaced by the
+proof of reflexivity of equality.
\begin{Variants}
- \item {\tt subst \ident$_1$ \dots \ident$_n$}
+ \item {\tt subst \ident$_1$ {\dots} \ident$_n$}
- Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
+ This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
\item {\tt subst}
- Applies {\tt subst} repeatedly to all identifiers from the context
- for which an equality exists.
+ This applies {\tt subst} repeatedly from top to bottom to all
+ identifiers of the context for which an equality of the form {\tt
+ \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with
+ {\ident} not occurring in $t$.
-\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set
- Regular Subst Tactic}. When this option is activated, {\tt subst}
- manages the following corner cases which otherwise it
- does not:
+\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled
+using option {\tt Set Regular Subst Tactic}. When this option is
+activated, {\tt subst} also deals with the following corner cases:
\begin{itemize}
\item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$}
and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a
variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$}
- or {\tt $u$ = \ident$_2$}
+ or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt
+ subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$
+ respectively.
+
\item A context with cyclic dependencies as with hypotheses {\tt
- \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$}
+ \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which
+ without the option would be a cause of failure of {\tt subst}.
\end{itemize}
-Additionally, it prevents a local definition such as {\tt \ident :=
- $t$} to be unfolded which otherwise it would exceptionally unfold in
+Additionally, it prevents a local definition such as {\tt \ident} :=
+ $t$ to be unfolded which otherwise it would exceptionally unfold in
configurations containing hypotheses of the form {\tt {\ident} = $u$},
or {\tt $u'$ = \ident} with $u'$ not a variable.
+Finally, it preserves the initial order of hypotheses, which without
+the option it may break.
+
The option is on by default.
\end{Variants}
@@ -3011,23 +3041,33 @@ variables bound by a let-in construction inside the term itself (use
here the {\tt zeta} flag). In any cases, opaque constants are not
unfolded (see Section~\ref{Opaque}).
-The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
-tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
-is a call-by-need strategy, with sharing of reductions: the arguments of a
-function call are partially evaluated only when necessary, and if an
-argument is used several times then it is computed only once. This
-reduction is efficient for reducing expressions with dead code. For
-instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a
-pair of a witness $t$, and a proof that $t$ satisfies the predicate
-$P$. Most of the time, $t$ may be computed without computing the proof
-of $P(t)$, thanks to the lazy strategy.
+Normalization according to the flags is done by first evaluating the
+head of the expression into a {\em weak-head} normal form, i.e. until
+the evaluation is bloked by a variable (or an opaque constant, or an
+axiom), as e.g. in {\tt x\;u$_1$\;...\;u$_n$}, or {\tt match x with
+ ... end}, or {\tt (fix f x \{struct x\} := ...) x}, or is a
+constructed form (a $\lambda$-expression, a constructor, a cofixpoint,
+an inductive type, a product type, a sort), or is a redex that the
+flags prevent to reduce. Once a weak-head normal form is obtained,
+subterms are recursively reduced using the same strategy.
+
+Reduction to weak-head normal form can be done using two strategies:
+{\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv}
+tactic). The lazy strategy is a call-by-need strategy, with sharing of
+reductions: the arguments of a function call are weakly evaluated only
+when necessary, and if an argument is used several times then it is
+weakly computed only once. This reduction is efficient for reducing
+expressions with dead code. For instance, the proofs of a proposition
+{\tt exists~$x$. $P(x)$} reduce to a pair of a witness $t$, and a
+proof that $t$ satisfies the predicate $P$. Most of the time, $t$ may
+be computed without computing the proof of $P(t)$, thanks to the lazy
+strategy.
The call-by-value strategy is the one used in ML languages: the
-arguments of a function call are evaluated first, using a weak
-reduction (no reduction under the $\lambda$-abstractions). Despite the
-lazy strategy always performs fewer reductions than the call-by-value
-strategy, the latter is generally more efficient for evaluating purely
-computational expressions (i.e. with few dead code).
+arguments of a function call are systematically weakly evaluated
+first. Despite the lazy strategy always performs fewer reductions than
+the call-by-value strategy, the latter is generally more efficient for
+evaluating purely computational expressions (i.e. with few dead code).
\begin{Variants}
\item {\tt compute} \tacindex{compute}\\
@@ -3623,9 +3663,6 @@ The {\hintdef} is one of the following expressions:
the number of subgoals generated by {\tt simple apply {\term}}.
%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
- The cost of that hint is the number of subgoals generated by that
- tactic.
-
% Is it really needed?
%% In case the inferred type of \term\ does not start with a product
%% the tactic added in the hint list is {\tt exact {\term}}. In case
@@ -3823,7 +3860,25 @@ is to set the cut expression to $c | e$, the initial cut expression
being \texttt{emp}.
+\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid}
+\label{HintMode}
+\comindex{Hint Mode}
+This sets an optional mode of use of the identifier {\qualid}. When
+proof-search faces a goal that ends in an application of {\qualid} to
+arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the
+hints associated to qualid can be applied or not. A mode specification
+is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is
+to be treated as an input {\tt +} or an output {\tt -} of the
+identifier. For a mode to match a list of arguments, input terms \emph{must
+not} contain existential variables, while outputs can be any term.
+Multiple modes can be declared for a single identifier, in that case
+only one mode needs to match the arguments for the hints to be applied.
+
+{\tt Hint Mode} is especially useful for typeclasses, when one does not
+want to support default instances and avoid ambiguity in
+general. Setting a parameter of a class as an input forces proof-search
+to be driven by that index of the class.
\end{itemize}
@@ -3831,25 +3886,6 @@ being \texttt{emp}.
pattern-matching on hypotheses using \texttt{match goal with} inside
the tactic.
-\begin{Variants}
-\item {\tt Hint \hintdef}
-
- No database name is given: the hint is registered in the {\tt core}
- database.
-
-\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$}
-
- This is used to declare hints that must not be exported to the other
- modules that require and import the current module. Inside a
- section, the option {\tt Local} is useless since hints do not
- survive anyway to the closure of sections.
-
-\item {\tt Hint Local \hintdef}
-
- Idem for the {\tt core} database.
-
-\end{Variants}
-
% There are shortcuts that allow to define several goal at once:
% \begin{itemize}
@@ -4113,6 +4149,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
\subsection{\tt tauto}
\tacindex{tauto}
+\tacindex{dtauto}
\label{tauto}
This tactic implements a decision procedure for intuitionistic propositional
@@ -4161,8 +4198,21 @@ Abort.
because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
instantiation of \verb=x= is necessary.
+\begin{Variants}
+
+\item {\tt dtauto}
+
+ While {\tt tauto} recognizes inductively defined connectives
+ isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+ or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+ True}, {\tt dtauto} recognizes also all inductive types with
+ one constructors and no indices, i.e. record-style connectives.
+
+\end{Variants}
+
\subsection{\tt intuition \tac}
\tacindex{intuition}
+\tacindex{dintuition}
\label{intuition}
The tactic \texttt{intuition} takes advantage of the search-tree built
@@ -4195,8 +4245,49 @@ incompatibilities.
\item {\tt intuition}
Is equivalent to {\tt intuition auto with *}.
+
+\item {\tt dintuition}
+
+ While {\tt intuition} recognizes inductively defined connectives
+ isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+ or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+ True}, {\tt dintuition} recognizes also all inductive types with
+ one constructors and no indices, i.e. record-style connectives.
+
\end{Variants}
+\optindex{Intuition Negation Unfolding}
+\optindex{Intuition Iff Unfolding}
+
+Some aspects of the tactic {\tt intuition} can be
+controlled using options. To avoid that inner negations which do not
+need to be unfolded are unfolded, use:
+
+\begin{quote}
+{\tt Unset Intuition Negation Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Negation Unfolding}
+\end{quote}
+
+To avoid that inner occurrence of {\tt iff} which do not need to be
+unfolded are unfolded (this is the default), use:
+
+\begin{quote}
+{\tt Unset Intuition Iff Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Iff Unfolding}
+\end{quote}
+
% En attente d'un moyen de valoriser les fichiers de demos
%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:33:13 +0000