aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/common/macros.tex5
-rw-r--r--doc/common/styles/html/coqremote/cover.html2
-rw-r--r--doc/common/styles/html/simple/cover.html2
-rw-r--r--doc/common/title.tex2
-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
-rw-r--r--doc/stdlib/index-list.html.template9
-rw-r--r--doc/tutorial/Tutorial.tex56
15 files changed, 611 insertions, 315 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 3b12f259b6..df5ee405f9 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -198,6 +198,7 @@
\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
\newcommand{\orpattern}{\nterm{or\_pattern}}
\newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\intropatternlist}{\nterm{intro\_pattern\_list}}
\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
@@ -405,8 +406,8 @@
\newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4
\,)\end{array}$}}
%END LATEX
-%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
-%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
+%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}}
+%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}}
\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
\,)\end{array}$}}
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index db82717094..6ec4dc1af0 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -60,7 +60,7 @@
<li>V8.2 © INRIA 2008-2011</li>
<li>V8.3 © INRIA 2010-2011</li>
<li>V8.4 © INRIA 2012-2014</li>
- <li>V8.5 © INRIA 2015</li>
+ <li>V8.5 © INRIA 2015-2016</li>
</ul>
<p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html
index 1641a1ed37..328bd68daf 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -38,7 +38,7 @@
<li>V8.2 © INRIA 2008-2011</li>
<li>V8.3 © INRIA 2010-2011</li>
<li>V8.4 © INRIA 2012-2014</li>
- <li>V8.5 © INRIA 2015</li>
+ <li>V8.5 © INRIA 2015-2016</li>
</ul>
<p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156a..0e072b6b65 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -45,7 +45,7 @@ V\coqversion, \today
%END LATEX
\copyright INRIA 1999-2004 ({\Coq} versions 7.x)
-\copyright INRIA 2004-2015 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
#3
\end{flushleft}
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}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a8bbdeb374..fb45777e7f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -21,6 +21,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Init/Peano.v
theories/Init/Specif.v
theories/Init/Tactics.v
+ theories/Init/Tauto.v
theories/Init/Wf.v
(theories/Init/Prelude.v)
</dd>
@@ -203,6 +204,7 @@ through the <tt>Require Import</tt> command.</p>
(theories/QArith/QArith.v)
theories/QArith/Qreals.v
theories/QArith/Qcanon.v
+ theories/QArith/Qcabs.v
theories/QArith/Qround.v
theories/QArith/QOrderedType.v
theories/QArith/Qminmax.v
@@ -477,13 +479,6 @@ through the <tt>Require Import</tt> command.</p>
theories/MSets/MSetPositive.v
theories/MSets/MSetToFiniteSet.v
(theories/MSets/MSets.v)
- theories/MMaps/MMapAVL.v
- theories/MMaps/MMapFacts.v
- theories/MMaps/MMapInterface.v
- theories/MMaps/MMapList.v
- theories/MMaps/MMapPositive.v
- theories/MMaps/MMapWeakList.v
- (theories/MMaps/MMaps.v)
</dd>
<dt> <b>FSets</b>:
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index e09feeb8eb..973a0b75e0 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -248,11 +248,14 @@ explicitly the type of the quantified variable. We check:
\begin{coq_example}
Check (forall m:nat, gt m 0).
\end{coq_example}
-We may clean-up the development by removing the contents of the
-current section:
+We may revert to the clean state of
+our initial session using the \Coq~ \verb:Reset: command:
\begin{coq_example}
-Reset Declaration.
+Reset Initial.
\end{coq_example}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
\section{Introduction to the proof engine: Minimal Logic}
@@ -658,10 +661,8 @@ respectively 1 and 2. Such abstract entities may be entered in the context
as global variables. But we must be careful about the pollution of our
global environment by such declarations. For instance, we have already
polluted our \Coq~ session by declaring the variables
-\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. If we want to revert to the clean state of
-our initial session, we may use the \Coq~ \verb:Reset: command, which returns
-to the state just prior the given global notion as we did before to
-remove a section, or we may return to the initial state using~:
+\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
+
\begin{coq_example}
Reset Initial.
\end{coq_example}
@@ -770,7 +771,7 @@ Let us now close the current section.
End R_sym_trans.
\end{coq_example}
-Here \Coq's printout is a warning that all local hypotheses have been
+All the local hypotheses have been
discharged in the statement of \verb:refl_if:, which now becomes a general
theorem in the first-order language declared in section
\verb:Predicate_calculus:. In this particular example, the use of section
@@ -1105,8 +1106,14 @@ mathematical justification of a logical development relies only on
Conversely, ordinary mathematical definitions can be unfolded at will, they
are {\sl transparent}.
+
\chapter{Induction}
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
\section{Data Types as Inductively Defined Mathematical Collections}
All the notions which were studied until now pertain to traditional
@@ -1195,7 +1202,7 @@ That is, instead of computing for natural \verb:i: an element of the indexed
\verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of
\verb:nat:. Let us check the type of \verb:prim_rec::
\begin{coq_example}
-Check prim_rec.
+About prim_rec.
\end{coq_example}
Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
@@ -1241,22 +1248,16 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
For the rest of the session, we shall clean up what we did so far with
types \verb:bool: and \verb:nat:, in order to use the initial definitions
given in \Coq's \verb:Prelude: module, and not to get confusing error
-messages due to our redefinitions. We thus revert to the state before
-our definition of \verb:bool: with the \verb:Reset: command:
+messages due to our redefinitions. We thus revert to the initial state:
\begin{coq_example}
-Reset bool.
-\end{coq_example}
-
-
-\subsection{Simple proofs by induction}
-
-\begin{coq_eval}
Reset Initial.
-\end{coq_eval}
+\end{coq_example}
\begin{coq_eval}
Set Printing Width 60.
\end{coq_eval}
+\subsection{Simple proofs by induction}
+
Let us now show how to do proofs by structural induction. We start with easy
properties of the \verb:plus: function we just defined. Let us first
show that $n=n+0$.
@@ -1480,6 +1481,11 @@ Qed.
\chapter{Modules}
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
+
\section{Opening library modules}
When you start \Coq~ without further requirements in the command line,
@@ -1543,9 +1549,13 @@ definitions available in the current context, especially if large
libraries have been loaded. A convenient \verb:Search: command
is available to lookup all known facts
concerning a given predicate. For instance, if you want to know all the
-known lemmas about the less or equal relation, just ask:
+known lemmas about both the successor and the less or equal relation, just ask:
+\begin{coq_eval}
+Reset Initial.
+Set Printing Width 60.
+\end{coq_eval}
\begin{coq_example}
-Search le.
+Search S le.
\end{coq_example}
Another command \verb:SearchHead: displays only lemmas where the searched
predicate appears at the head position in the conclusion.
@@ -1553,9 +1563,9 @@ predicate appears at the head position in the conclusion.
SearchHead le.
\end{coq_example}
-A new and more convenient search tool is \textsf{SearchPattern}
+A new and more convenient search tool is \verb:SearchPattern:
developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:\_: can be used in
+conclusion matching a given pattern, where \verb:_: can be used in
place of an arbitrary term. We remark in this example, that \Coq{}
provides usual infix notations for arithmetic operators.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:52:15 +0000