aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/common/macros.tex4
-rw-r--r--doc/refman/AsyncProofs.tex40
-rw-r--r--doc/refman/CanonicalStructures.tex2
-rw-r--r--doc/refman/Extraction.tex40
-rw-r--r--doc/refman/RefMan-cic.tex263
-rw-r--r--doc/refman/RefMan-ltac.tex100
-rw-r--r--doc/refman/RefMan-syn.tex2
-rw-r--r--doc/refman/RefMan-tac.tex53
-rw-r--r--doc/refman/Universes.tex4
-rw-r--r--doc/stdlib/index-list.html.template2
-rw-r--r--doc/tutorial/Tutorial.tex56
11 files changed, 430 insertions, 136 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 077e2f0dfb..df5ee405f9 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -406,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/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7cf5004003..7ffe252253 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an
auxiliary file, produced along with the \texttt{.vo} file, the list of
section variables used.
+\section{Proof blocks and error resilience}
+
+Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq
+is able to completely check a document containing errors instead of bailing
+out at the first failure.
+
+Two kind of errors are supported: errors occurring in vernacular commands and
+errors occurring in proofs.
+
+To properly recover from a failing tactic, Coq needs to recognize the structure of
+the proof in order to confine the error to a sub proof. Proof block detection
+is performed by looking at the syntax of the proof script (i.e. also looking at indentation).
+Coq comes with four kind of proof blocks, and an ML API to add new ones.
+
+\begin{description}
+\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling}
+\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector
+\item[indent] blocks end with a tactic indented less than the previous one
+\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level
+\end{description}
+
+\subsection{Caveats}
+
+When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by
+the first error. Error resiliency for vernacular commands can be switched off passing
+\texttt{-async-proofs-command-error-resilience off} to CoqIDE.
+
+An incorrect proof block detection can result into an incorrect error recovery and
+hence in bogus errors. Proof block detection cannot be precise for bullets or
+any other non well parenthesized proof structure. Error resiliency can be
+turned off or selectively activated for any set of block kind passing to
+CoqIDE one of the following options:
+\texttt{-async-proofs-tactic-error-resilience off},
+\texttt{-async-proofs-tactic-error-resilience all},
+\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}.
+Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''.
+
\subsubsection{Automatic suggestion of proof annotations}
The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
@@ -85,6 +122,9 @@ reduce the reactivity of the master process to user commands.
To disable this feature, one can pass the \texttt{-async-proofs off} flag to
CoqIDE.
+Proofs that are known to take little time to process are not delegated to a
+worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds.
+
\section{Batch mode}
When Coq is used as a batch compiler by running \texttt{coqc} or
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index a3372c2965..275e1c2d55 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -4,7 +4,7 @@
\label{CS-full}
\index{Canonical Structures!presentation}
-This chapter explains the basics of Canonical Structure and how thy can be used
+\noindent This chapter explains the basics of Canonical Structure and how they can be used
to overload notations and build a hierarchy of algebraic structures.
The examples are taken from~\cite{CSwcu}. We invite the interested reader
to refer to this paper for all the details that are omitted here for brevity.
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index a963662f64..9da23b54ed 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -3,7 +3,7 @@
\aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
\index{Extraction}
-We present here the \Coq\ extraction commands, used to build certified
+\noindent We present here the \Coq\ extraction commands, used to build certified
and relatively efficient functional programs, extracting them from
either \Coq\ functions or \Coq\ proofs of specifications. The
functional languages available as output are currently \ocaml{},
@@ -30,7 +30,7 @@ The next two commands are meant to be used for rapid preview of
extraction. They both display extracted term(s) inside \Coq.
\begin{description}
-\item {\tt Extraction \qualid.} ~\par
+\item {\tt Extraction \qualid{}.} ~\par
Extraction of a constant or module in the \Coq\ toplevel.
\item {\tt Recursive Extraction} \qualid$_1$ \dots\ \qualid$_n$. ~\par
@@ -40,7 +40,7 @@ extraction. They both display extracted term(s) inside \Coq.
%% TODO error messages
-All the following commands produce real ML files. User can choose to produce
+\noindent All the following commands produce real ML files. User can choose to produce
one monolithic file or one file per \Coq\ library.
\begin{description}
@@ -76,7 +76,7 @@ one monolithic file or one file per \Coq\ library.
using prefixes \verb!coq_! or \verb!Coq_!.
\end{description}
-The list of globals \qualid$_i$ does not need to be
+\noindent The list of globals \qualid$_i$ does not need to be
exhaustive: it is automatically completed into a complete and minimal
environment.
@@ -215,7 +215,7 @@ arguments. In fact, an argument can also be referred by a number
indicating its position, starting from 1.
\end{description}
-When an actual extraction takes place, an error is normally raised if the
+\noindent When an actual extraction takes place, an error is normally raised if the
{\tt Extraction Implicit}
declarations cannot be honored, that is if any of the implicited
variables still occurs in the final code. This behavior can be relaxed
@@ -260,7 +260,7 @@ what ML term corresponds to a given axiom.
be inlined everywhere instead of being declared via a let.
\end{description}
-Note that the {\tt Extract Inlined Constant} command is sugar
+\noindent Note that the {\tt Extract Inlined Constant} command is sugar
for an {\tt Extract Constant} followed by a {\tt Extraction Inline}.
Hence a {\tt Reset Extraction Inline} will have an effect on the
realized and inlined axiom.
@@ -279,7 +279,7 @@ Extract Constant X => "int".
Extract Constant x => "0".
\end{coq_example*}
-Notice that in the case of type scheme axiom (i.e. whose type is an
+\noindent Notice that in the case of type scheme axiom (i.e. whose type is an
arity, that is a sequence of product finished by a sort), then some type
variables have to be given. The syntax is then:
@@ -287,7 +287,7 @@ variables have to be given. The syntax is then:
\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.}
\end{description}
-The number of type variables is checked by the system.
+\noindent The number of type variables is checked by the system.
\Example
\begin{coq_example*}
@@ -295,7 +295,7 @@ Axiom Y : Set -> Set -> Set.
Extract Constant Y "'a" "'b" => " 'a*'b ".
\end{coq_example*}
-Realizing an axiom via {\tt Extract Constant} is only useful in the
+\noindent Realizing an axiom via {\tt Extract Constant} is only useful in the
case of an informative axiom (of sort Type or Set). A logical axiom
have no computational content and hence will not appears in extracted
terms. But a warning is nonetheless issued if extraction encounters a
@@ -325,7 +325,7 @@ native boolean type instead of \Coq\ one. The syntax is the following:
pattern-matching of the language will be used.
\end{description}
-For an inductive type with $k$ constructor, the function used to
+\noindent For an inductive type with $k$ constructor, the function used to
emulate the match should expect $(k+1)$ arguments, first the $k$
branches in functional form, and then the inductive element to
destruct. For instance, the match branch \verb$| S n => foo$ gives the
@@ -365,7 +365,7 @@ Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
\end{coq_example}
-If an inductive constructor or type has arity 2 and the corresponding
+\noindent If an inductive constructor or type has arity 2 and the corresponding
string is enclosed by parenthesis, then the rest of the string is used
as infix constructor or type.
\begin{coq_example}
@@ -373,7 +373,7 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
\end{coq_example}
-As an example of translation to a non-inductive datatype, let's turn
+\noindent As an example of translation to a non-inductive datatype, let's turn
{\tt nat} into Ocaml's {\tt int} (see caveat above):
\begin{coq_example}
Extract Inductive nat => int [ "0" "succ" ]
@@ -402,7 +402,7 @@ It is possible to instruct the extraction not to use particular filenames.
Allow the extraction to use any filename.
\end{description}
-For Ocaml, a typical use of these commands is
+\noindent For Ocaml, a typical use of these commands is
{\tt Extraction Blacklist String List}.
\asection{Differences between \Coq\ and ML type systems}
@@ -456,7 +456,7 @@ In Ocaml, we must cast any argument of the constructor dummy.
\end{itemize}
-Even with those unsafe castings, you should never get error like
+\noindent Even with those unsafe castings, you should never get error like
``segmentation fault''. In fact even if your program may seem
ill-typed to the Ocaml type-checker, it can't go wrong: it comes
from a Coq well-typed terms, so for example inductives will always
@@ -489,7 +489,7 @@ Inductive nat : Set :=
| S : nat -> nat.
\end{coq_example*}
-This module contains a theorem {\tt eucl\_dev}, whose type is
+\noindent This module contains a theorem {\tt eucl\_dev}, whose type is
\begin{verbatim}
forall b:nat, b > 0 -> forall a:nat, diveucl a b
\end{verbatim}
@@ -506,7 +506,7 @@ Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
Recursive Extraction eucl_dev.
\end{coq_example}
-The inlining of {\tt gt\_wf\_rec} and others is not
+\noindent The inlining of {\tt gt\_wf\_rec} and others is not
mandatory. It only enhances readability of extracted code.
You can then copy-paste the output to a file {\tt euclid.ml} or let
\Coq\ do it for you with the following command:
@@ -515,7 +515,7 @@ You can then copy-paste the output to a file {\tt euclid.ml} or let
Extraction "euclid" eucl_dev.
\end{verbatim}
-Let us play the resulting program:
+\noindent Let us play the resulting program:
\begin{verbatim}
# #use "euclid.ml";;
@@ -543,7 +543,7 @@ val div : int -> int -> int * int = <fun>
- : int * int = (11, 8)
\end{verbatim}
-Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
+\noindent Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
available via a mere {\tt Require Import ExtrOcamlIntConv} and then
adding these functions to the list of functions to extract. This file
{\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/}
@@ -551,7 +551,7 @@ are meant to help building concrete program via extraction.
\asubsection{Extraction's horror museum}
-Some pathological examples of extraction are grouped in the file
+Some pathological examples of extraction are grouped in the file\\
{\tt test-suite/success/extraction.v} of the sources of \Coq.
\asubsection{Users' Contributions}
@@ -579,7 +579,7 @@ extraction test:
\item {\tt stalmarck}
\end{itemize}
-{\tt continuations} and {\tt multiplier} are a bit particular. They are
+\noindent {\tt continuations} and {\tt multiplier} are a bit particular. They are
examples of developments where {\tt Obj.magic} are needed. This is
probably due to an heavy use of impredicativity. After compilation, those
two examples run nonetheless, thanks to the correction of the
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-ltac.tex b/doc/refman/RefMan-ltac.tex
index cc7e6b53bf..ffcb371346 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -78,7 +78,7 @@ For instance
{\tt try repeat \tac$_1$ ||
\tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
\end{quote}
-is understood as
+is understood as
\begin{quote}
{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
@@ -174,7 +174,7 @@ is understood as
\\
{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
\\
-\tacarg & ::= &
+\tacarg & ::= &
{\qualid}\\
& $|$ & {\tt ()} \\
& $|$ & {\tt ltac :} {\atom}\\
@@ -344,7 +344,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
expects multiple goals, such as {\tt swap}, would act as if a single
goal is focused.
- \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+ \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
This variant of local tactic application is paired with a
sequence. In this variant, $n$ must be the number of goals
@@ -782,7 +782,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
\begin{coq_example}
Ltac f x :=
match x with
- context f [S ?X] =>
+ context f [S ?X] =>
idtac X; (* To display the evaluation order *)
assert (p := eq_refl 1 : X=1); (* To filter the case X=1 *)
let x:= context f[O] in assert (x=O) (* To observe the context *)
@@ -1026,7 +1026,7 @@ Reset Initial.
\index{Tacticals!abstract@{\tt abstract}}}
From the outside ``\texttt{abstract \tacexpr}'' is the same as
-{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
+{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
current goal and \textit{n} is chosen so that this is a fresh name.
Such auxiliary lemma is inlined in the final proof term
@@ -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}}
@@ -1194,6 +1196,86 @@ s: & continue current evaluation without stopping\\
r $n$: & advance $n$ steps further\\
r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
\end{tabular}
+
+\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
+
+It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
+
+\begin{quote}
+{\tt Set Ltac Profiling}.
+\end{quote}
+Enables the profiler
+
+\begin{quote}
+{\tt Unset Ltac Profiling}.
+\end{quote}
+Disables the profiler
+
+\begin{quote}
+{\tt Show Ltac Profile}.
+\end{quote}
+Prints the profile
+
+\begin{quote}
+{\tt Show Ltac Profile} {\qstring}.
+\end{quote}
+Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
+
+\begin{quote}
+{\tt Reset Profile}.
+\end{quote}
+Resets the profile, that is, deletes all accumulated information
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Require Import Coq.omega.Omega.
+
+Ltac mytauto := tauto.
+Ltac tac := intros; repeat split; omega || mytauto.
+
+Notation max x y := (x + (y - x)) (only parsing).
+\end{coq_example*}
+\begin{coq_example*}
+Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z,
+ max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z
+ /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z
+ -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A).
+Proof.
+\end{coq_example*}
+\begin{coq_example}
+ Set Ltac Profiling.
+ tac.
+\end{coq_example}
+{\let\textit\texttt% use tt mode for the output of ltacprof
+\begin{coq_example}
+ Show Ltac Profile.
+\end{coq_example}
+\begin{coq_example}
+ Show Ltac Profile "omega".
+\end{coq_example}
+}
+\begin{coq_example*}
+Abort.
+Unset Ltac Profiling.
+\end{coq_example*}
+
+\tacindex{start ltac profiling}\tacindex{stop ltac profiling}
+The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling.
+
+\begin{quote}
+{\tt start ltac profiling}.
+\end{quote}
+
+\begin{quote}
+{\tt stop ltac profiling}.
+\end{quote}
+
+You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end.
+
+Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
+
\endinput
\subsection{Permutation on closed lists}
@@ -1227,7 +1309,7 @@ Another more complex example is the problem of permutation on closed
lists. The aim is to show that a closed list is a permutation of
another one. First, we define the permutation predicate as shown on
Figure~\ref{permutpred}.
-
+
\begin{figure}[p]
\begin{center}
\fbox{\begin{minipage}{0.95\textwidth}
@@ -1553,7 +1635,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
\begin{center}
\fbox{\begin{minipage}{0.95\textwidth}
\begin{coq_example*}
-Lemma isos_ex1 :
+Lemma isos_ex1 :
forall A B:Set, A * unit * B = B * (unit * A).
Proof.
intros; IsoProve.
@@ -1573,7 +1655,7 @@ Qed.
\label{isoslem}
\end{figure}
-%%% Local Variables:
+%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
-%%% End:
+%%% End:
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 3af72db78e..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
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f5a1bf3b22..54450fe7dc 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2833,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.
\Rem
-When several hypotheses have the form {\tt \ident=t} or {\tt
- t=\ident}, the first one is used.
+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}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a08cd1475a..36518e6fae 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions.
In the monorphic case, this command declares a new global universe named
{\ident}. It supports the polymorphic flag only in sections, meaning the
universe quantification will be discharged on each section definition
-independently.
+independently. One cannot mix polymorphic and monomorphic declarations
+in the same section.
\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
\comindex{Constraint}
@@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent,
the constraint is then enforced in the global environment. Like
\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
in sections only to declare constraints discharged at section closing time.
+One cannot declare a global constraint on polymorphic universes.
\begin{ErrMsgs}
\item \errindex{Undeclared universe {\ident}}.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a12983ab84..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
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-04-29 22:27:53 +0000