diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/macros.tex | 3 | ||||
| -rw-r--r-- | doc/common/styles/html/coqremote/cover.html | 1 | ||||
| -rw-r--r-- | doc/common/styles/html/simple/cover.html | 1 | ||||
| -rw-r--r-- | doc/faq/FAQ.tex | 4 | ||||
| -rw-r--r-- | doc/faq/fk.bib | 2 | ||||
| -rw-r--r-- | doc/refman/AsyncProofs.tex | 40 | ||||
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 178 | ||||
| -rw-r--r-- | doc/refman/Extraction.tex | 42 | ||||
| -rw-r--r-- | doc/refman/Micromega.tex | 90 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 19 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 169 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 23 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 133 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 38 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 235 | ||||
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 8 | ||||
| -rw-r--r-- | doc/refman/Universes.tex | 4 | ||||
| -rw-r--r-- | doc/refman/biblio.bib | 2 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 3 | ||||
| -rw-r--r-- | doc/tutorial/Tutorial.tex | 61 |
25 files changed, 877 insertions, 217 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index df5ee405f9..5abdecfc18 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -72,7 +72,8 @@ %\newcommand{\spec}[1]{\{\,#1\,\}} % Building regular expressions -\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}} +\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}} +\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}} %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*} %\newcommand{\onemany}[1]{$\{$#1$\}$+} \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}} diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 6ec4dc1af0..1c415eca69 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -61,6 +61,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 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 328bd68daf..25fb56320b 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -39,6 +39,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 2016</li> </ul> <p style="text-indent:0pt">This research was partly supported by IST diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 48b61827d1..213fb03137 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots} \Question{What is a dependent type?} -A dependant type is a type which depends on some term. For instance -``vector of size n'' is a dependant type representing all the vectors +A dependent type is a type which depends on some term. For instance +``vector of size n'' is a dependent type representing all the vectors of size $n$. Its type depends on $n$ \Question{What is a proof by reflection?} diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib index 4d90efcdb1..3410427dee 100644 --- a/doc/faq/fk.bib +++ b/doc/faq/fk.bib @@ -2171,7 +2171,7 @@ Decomposition}}, @Misc{ProofGeneral, author = {David Aspinall}, title = {Proof General}, - note = {\url{http://proofgeneral.inf.ed.ac.uk/}} + note = {\url{https://proofgeneral.github.io/}} } 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/Classes.tex b/doc/refman/Classes.tex index e8ebb9f995..acfc4bea93 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -9,10 +9,6 @@ \aauthor{Matthieu Sozeau} \label{typeclasses} -\begin{flushleft} - \em The status of Type Classes is experimental. -\end{flushleft} - This chapter presents a quick reference of the commands related to type classes. For an actual introduction to type classes, there is a description of the system \cite{sozeau08} and the literature on type @@ -382,6 +378,71 @@ projections as instances. This is almost equivalent to {\tt Hint Resolve Declares variables according to the given binding context, which might use implicit generalization (see \ref{SectionContext}). +\asubsection{\tt typeclasses eauto} +\tacindex{typeclasses eauto} +\label{typeclasseseauto} + +The {\tt typeclasses eauto} tactic uses a different resolution engine +than {\tt eauto} and {\tt auto}. The main differences are the following: +\begin{itemize} +\item Contrary to {\tt eauto} and {\tt auto}, the resolution is done + entirely in the new proof engine (as of Coq v8.6), meaning that + backtracking is available among dependent subgoals, and shelving goals + is supported. {\tt typeclasses eauto} is a multi-goal tactic. + It analyses the dependencies between subgoals to avoid + backtracking on subgoals that are entirely independent. +\item When called with no arguments, {\tt typeclasses eauto} uses the + {\tt typeclass\_instances} database by default (instead of {\tt + core}). + Dependent subgoals are automatically shelved, and shelved + goals can remain after resolution ends (following the behavior of + \Coq{} 8.5). + + \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} + faithfully mimicks what happens during typeclass resolution when it is + called during refinement/type-inference, except that \emph{only} + declared class subgoals are considered at the start of resolution + during type inference, while ``all'' can select non-class subgoals as + well. It might move to {\tt all:typeclasses eauto} in future versions + when the refinement engine will be able to backtrack. +\item When called with specific databases (e.g. {\tt with}), {\tt + typeclasses eauto} allows shelved goals to remain at any point + during search and treat typeclasses goals like any other. +\item The transparency information of databases is used consistently for + all hints declared in them. It is always used when calling the unifier. + When considering the local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with {\tt Create HintDb} for example) with + unfoldable variables and constants as the first argument of + typeclasses eauto hence makes resolution with the local hypotheses use + full conversion during unification. +\end{itemize} + +\begin{Variants} +\item \label{depth} {\tt typeclasses eauto \zeroone{\num}} + \emph{Warning:} The semantics for the limit {\num} is different than + for {\tt auto}. By default, if no limit is given the search is + unbounded. Contrary to {\tt auto}, introduction steps ({\tt intro}) + are counted, which might result in larger limits being necessary + when searching with {\tt typeclasses eauto} than {\tt auto}. + +\item \label{with} {\tt typeclasses eauto with {\ident}$_1$ \ldots {\ident}$_n$}. + This variant runs resolution with the given hint databases. It treats + typeclass subgoals the same as other subgoals (no shelving of + non-typeclass goals in particular). +\end{Variants} + +\asubsection{\tt autoapply {\term} with {\ident}} +\tacindex{autoapply} + +The tactic {\tt autoapply} applies a term using the transparency +information of the hint database {\ident}, and does \emph{no} typeclass +resolution. This can be used in {\tt Hint Extern}'s for typeclass +instances (in hint db {\tt typeclass\_instances}) to +allow backtracking on the typeclass subgoals created by the lemma +application, rather than doing type class resolution locally at the hint +application time. + \subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}} \comindex{Typeclasses Transparent} \comindex{Typeclasses Opaque} @@ -400,20 +461,123 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}. This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}. +\subsection{\tt Set Typeclasses Dependency Order} +\optindex{Typeclasses Dependency Order} + +This option (on by default since 8.6) respects the dependency order between +subgoals, meaning that subgoals which are depended on by other subgoals +come first, while the non-dependent subgoals were put before the +dependent ones previously (Coq v8.5 and below). This can result in quite +different performance behaviors of proof search. + +\subsection{\tt Set Typeclasses Filtered Unification} +\optindex{Typeclasses Filtered Unification} + +This option, available since Coq 8.6 and off by default, switches the +hint application procedure to a filter-then-unify strategy. To apply a +hint, we first check that the goal \emph{matches} syntactically the +inferred or specified pattern of the hint, and only then try to +\emph{unify} the goal with the conclusion of the hint. This can +drastically improve performance by calling unification less often, +matching syntactic patterns being very quick. This also provides more +control on the triggering of instances. For example, forcing a constant +to explicitely appear in the pattern will make it never apply on a goal +where there is a hole in that place. + +\subsection{\tt Set Typeclasses Legacy Resolution} +\optindex{Typeclasses Legacy Resolution} + +This option (off by default) uses the 8.5 implementation of resolution. +Use for compatibility purposes only (porting and debugging). + +\subsection{\tt Set Typeclasses Module Eta} +\optindex{Typeclasses Modulo Eta} + +This option allows eta-conversion for functions and records during +unification of type-classes. This option is now unsupported in 8.6 with +{\tt Typeclasses Filtered Unification} set, but still affects the +default unification strategy, and the one used in {\tt Legacy + Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses + Filtered Unification} is set, this has no effect and unification will +find solutions up-to eta conversion. Note however that syntactic +pattern-matching is not up-to eta. + +\subsection{\tt Set Typeclasses Limit Intros} +\optindex{Typeclasses Limit Intros} + +This option (on by default in Coq 8.6 and below) controls the ability to +apply hints while avoiding (functional) eta-expansions in the generated +proof term. It does so by allowing hints that conclude in a product to +apply to a goal with a matching product directly, avoiding an +introduction. \emph{Warning:} this can be expensive as it requires +rebuilding hint clauses dynamically, and does not benefit from the +invertibility status of the product introduction rule, resulting in +potentially more expensive proof-search (i.e. more useless +backtracking). + +\subsection{\tt Set Typeclass Resolution After Apply} +\optindex{Typeclasses Resolution After Apply} +\emph{Deprecated since 8.6} + +This option (off by default in Coq 8.6 and 8.5) controls the resolution +of typeclass subgoals generated by the {\tt apply} tactic. + +\subsection{\tt Set Typeclass Resolution For Conversion} +\optindex{Typeclasses Resolution For Conversion} + +This option (on by default) controls the use of typeclass resolution +when a unification problem cannot be solved during +elaboration/type-inference. With this option on, when a unification +fails, typeclass resolution is tried before launching unification once again. + +\subsection{\tt Set Typeclasses Strict Resolution} +\optindex{Typeclasses Strict Resolution} + +Typeclass declarations introduced when this option is set have a +stricter resolution behavior (the option is off by default). When +looking for unifications of a goal with an instance of this class, we +``freeze'' all the existentials appearing in the goals, meaning that +they are considered rigid during unification and cannot be instantiated. + +\subsection{\tt Set Typeclasses Unique Solutions} +\optindex{Typeclasses Unique Solutions} + +When a typeclass resolution is launched we ensure that it has a single +solution or fail. This ensures that the resolution is canonical, but can +make proof search much more expensive. + +\subsection{\tt Set Typeclasses Unique Instances} +\optindex{Typeclasses Unique Instances} + +Typeclass declarations introduced when this option is set have a +more efficient resolution behavior (the option is off by default). When +a solution to the typeclass goal of this class is found, we never +backtrack on it, assuming that it is canonical. + \subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} \comindex{Typeclasses eauto} \label{TypeclassesEauto} -This command allows customization of the type class resolution tactic, -based on a variant of eauto. The flags semantics are: +This command allows more global customization of the type class +resolution tactic. +The semantics of the options are: \begin{itemize} \item {\tt debug} In debug mode, the trace of successfully applied tactics is printed. \item {\tt dfs, bfs} This sets the search strategy to depth-first search (the default) or breadth-first search. -\item {\emph{depth}} This sets the depth of the search (the default is 100). +\item {\emph{depth}} This sets the depth limit of the search. \end{itemize} +\subsection{\tt Set Typeclasses Debug [Verbosity {\num}]} +\optindex{Typeclasses Debug} +\optindex{Typeclasses Debug Verbosity} + +These options allow to see the resolution steps of typeclasses that are +performed during search. The {\tt Debug} option is synonymous to +{\tt Debug Verbosity 1}, and {\tt Debug Verbosity 2} provides more +information (tried tactics, shelving of goals, etc\ldots). + \subsection{\tt Set Refine Instance Mode} \optindex{Refine Instance Mode} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index a963662f64..01dbcfb1cb 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} @@ -448,7 +448,7 @@ let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) happens when there is a quantification over types inside the type of a constructor; for example: \begin{verbatim} -Inductive anything : Set := dummy : forall A:Set, A -> anything. +Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. @@ -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/Micromega.tex b/doc/refman/Micromega.tex index 1efed6ef76..4daf98f87a 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -4,16 +4,19 @@ \asection{Short description of the tactics} -\tacindex{psatz} \tacindex{lra} +\tacindex{psatz} \tacindex{lra} \tacindex{lia} \tacindex{nia} \tacindex{nra} \label{sec:psatz-hurry} The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and {\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by - pre-processing the goal with the {\tt zify} tactic.} + pre-processing the goal with the {\tt zify} tactic.}. +It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} +and reals {\tt Require Import Lra}. \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); -\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); +\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic (see Section~\ref{sec:lra}); +\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic (see Section~\ref{sec:nra}); \item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and {\tt n} is an optional integer limiting the proof search depth is is an incomplete proof procedure for non-linear arithmetic. It is based on @@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} -\label{sec:psatz} -The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a -refutation. - -To illustrate the working of the tactic, consider we wish to prove the following Coq goal. -\begin{coq_eval} -Require Import ZArith Psatz. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example*} -Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; psatz Z 2. -\end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the -cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times -(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in -bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, -x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By -Theorem~\ref{thm:psatz}, the goal is valid. -% - -%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a -%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. -%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. -% \asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} @@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} -\tacindex{nia} -\label{sec:nia} -The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. + +\asection{{\tt nra}: a proof procedure for non-linear arithmetic} +\tacindex{nra} +\label{sec:nra} +The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic. % The tactic performs a limited amount of non-linear reasoning before running the -linear prover of {\tt lia}. +linear prover of {\tt lra}. This pre-processing does the following: \begin{itemize} \item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a monomial, the context is enriched with $x^2\ge 0$; \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} searches for a proof +After this pre-processing, the linear prover of {\tt lra} searches for a proof by abstracting monomials by variables. +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} +\tacindex{nia} +\label{sec:nia} +The {\tt nia} tactic is a proof procedure for non-linear integer arithmetic. +% +It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}. + +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} +\label{sec:psatz} +The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. +In theory, such a proof search is complete -- if the goal is provable the search eventually stops. +Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a +refutation. + +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. +\begin{coq_eval} +Require Import ZArith Psatz. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example*} +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +\end{coq_example*} +\begin{coq_eval} +intro x; psatz Z 2. +\end{coq_eval} +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Theorem~\ref{thm:psatz}, the goal is valid. +% + +%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a +%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. +%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. +% + %%% Local Variables: diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 11dd3a0517..2fc1c8764a 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -63,10 +63,27 @@ will be first rewritten to: previous one, an inequality is added in the context of the second branch. See for example the definition of {\tt div2} below, where the second branch is typed in a context where $\forall p, \_ <> S (S p)$. - + \item Coercion. If the object being matched is coercible to an inductive type, the corresponding coercion will be automatically inserted. This also works with the previous mechanism. + +\end{itemize} + +There are options to control the generation of equalities +and coercions. + +\begin{itemize} +\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates + the special treatment of pattern-matching generating equalities and + inequalities when using \Program\ (it is on by default). All + pattern-matchings and let-patterns are handled using the standard + algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is + deactivated. +\item {\tt Unset Program Generalized Coercion}\optindex{Program + Generalized Coercion} This deactivates the coercion of general + inductive types when using \Program\ (the option is on by default). + Coercion of subset types and pairs is still active in this case. \end{itemize} \subsection{Syntactic control over equalities} diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 6f85849888..bef0a1686f 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -26,13 +26,13 @@ run by the command {\tt coqtop}. They are two different binary images of \Coq: the byte-code one and the native-code one (if {\ocaml} provides a native-code compiler for your platform, which is supposed in the following). By default, -\verb!coqc! executes the native-code version; this can be overridden -using the \verb!-byte! option. +\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to +get the byte-code version. The byte-code toplevel is based on an {\ocaml} toplevel (to allow the dynamic link of tactics). You can switch to the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the -\Coq~toplevel with the command \verb!Toplevel.loop();;!. +\Coq~toplevel with the command \verb!Coqloop.loop();;!. \section{Batch compilation ({\tt coqc})} The {\tt coqc} command takes a name {\em file} as argument. Then it @@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt available for {\tt coqc} only; it is the counterpart of {\tt -compile-verbose}. + \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ % + + Configure the display of warnings. This option expects {\tt all}, {\tt none} + or a comma-separated list of warning names or categories (see + Section~\ref{SetWarnings}). + %Mostly unused in the code %\item[{\tt -debug}]\ % % diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 51e881bff4..b475a5233c 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1315,10 +1315,10 @@ command: \begin{quote} \tt Arguments {\qualid} \nelist{\possiblybracketedident}{} \end{quote} -where the list of {\possiblybracketedident} is the list of all arguments of -{\qualid} where the ones to be declared implicit are surrounded by -square brackets and the ones to be declared as maximally inserted implicits -are surrounded by curly braces. +where the list of {\possiblybracketedident} is a prefix of the list of arguments +of {\qualid} where the ones to be declared implicit are surrounded by square +brackets and the ones to be declared as maximally inserted implicits are +surrounded by curly braces. After the above declaration is issued, implicit arguments can just (and have to) be skipped in any expression involving an application of @@ -1591,7 +1591,7 @@ Implicit arguments names can be redefined using the following syntax: {\tt Arguments {\qualid} \nelist{\name}{} : rename} \end{quote} -Without the {\tt rename} flag, {\tt Arguments} can be used to assert +With the {\tt assert} flag, {\tt Arguments} can be used to assert that a given object has the expected number of arguments and that these arguments are named as expected. @@ -1600,7 +1600,7 @@ these arguments are named as expected. Arguments p [s t] _ [u] _: rename. Check (p r1 (u:=c)). Check (p (s:=a) (t:=b) r1 (u:=c) r2). -Fail Arguments p [s t] _ [w] _. +Fail Arguments p [s t] _ [w] _ : assert. \end{coq_example} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index fcccd9cb4b..3814e4403a 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter {\binder} & ::= & {\name} & (\ref{Binders}) \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ + & $|$ & {\tt '} {\pattern} &\\ & & &\\ {\name} & ::= & {\ident} &\\ & $|$ & {\tt \_} &\\ @@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt )}. There is also a notation for a sequence of binding variables sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt -:}\,{\type}\,{\tt )}. +:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote, +e.g. {\tt '(x,y)}. Some constructions allow the binding of a variable to value. This is called a ``let-binder''. The entry {\binder} of the grammar accepts @@ -711,9 +713,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ -{\inductivebody} & ::= & - {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ - && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\ +{\inductivebody} & ::= & + {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\ + && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\ & & \\ %% TODO: where ... %% Fixpoints {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index cc7e6b53bf..9378529cbe 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -25,6 +25,8 @@ problems. \def\contexthyp{\textrm{\textsl{context\_hyp}}} \def\tacarg{\nterm{tacarg}} \def\cpattern{\nterm{cpattern}} +\def\selector{\textrm{\textsl{selector}}} +\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}} The syntax of the tactic language is given Figures~\ref{ltac} and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of @@ -78,7 +80,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$).} @@ -104,6 +106,7 @@ is understood as & | & {\tt exactly\_once} {\tacexprpref}\\ & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\ +& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\ & | & {\tacexprinf} \\ \\ {\tacexprinf} & ::= & @@ -174,7 +177,7 @@ is understood as \\ {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ \\ -\tacarg & ::= & +\tacarg & ::= & {\qualid}\\ & $|$ & {\tt ()} \\ & $|$ & {\tt ltac :} {\atom}\\ @@ -203,7 +206,18 @@ is understood as & $|$ & {\integer} {\tt \,<\,} {\integer}\\ & $|$ & {\integer} {\tt <=} {\integer}\\ & $|$ & {\integer} {\tt \,>\,} {\integer}\\ -& $|$ & {\integer} {\tt >=} {\integer} +& $|$ & {\integer} {\tt >=} {\integer}\\ +\\ +\selector & ::= & + [{\ident}]\\ +& $|$ & {\integer}\\ +& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}} + {\tt ,}\\ +\\ +\toplevelselector & ::= & + \selector\\ +& $|$ & {\tt all}\\ +& $|$ & {\tt par} \end{tabular} \end{centerframe} \caption{Syntax of the tactic language (continued)} @@ -344,7 +358,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 @@ -358,7 +372,58 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. \end{Variants} +\subsubsection[Goal selectors]{Goal selectors\label{ltac:selector} +\tacindex{\tt :}\index{Tacticals!:@{\tt :}}} + +We can restrict the application of a tactic to a subset of +the currently focused goals with: +\begin{quote} + {\toplevelselector} {\tt :} {\tacexpr} +\end{quote} +We can also use selectors as a tactical, which allows to use them nested in +a tactic expression, by using the keyword {\tt only}: +\begin{quote} + {\tt only} {\selector} {\tt :} {\tacexpr} +\end{quote} +When selecting several goals, the tactic {\tacexpr} is applied globally to +all selected goals. + +\begin{Variants} + \item{} [{\ident}] {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied locally to a goal + previously named by the user. + + \item {\num} {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied locally to the + {\num}-th goal. + + \item $n_1$-$m_1$, \dots, $n_k$-$m_k$ {\tt :} {\tacexpr} + + In this variant, {\tacexpr} is applied globally to the subset + of goals described by the given ranges. You can write a single + $n$ as a shortcut for $n$-$n$ when specifying multiple ranges. + + \item {\tt all:} {\tacexpr} + + In this variant, {\tacexpr} is applied to all focused goals. + {\tt all:} can only be used at the toplevel of a tactic expression. + + \item {\tt par:} {\tacexpr} + In this variant, {\tacexpr} is applied to all focused goals + in parallel. The number of workers can be controlled via the + command line option {\tt -async-proofs-tac-j} taking as argument + the desired number of workers. Limitations: {\tt par: } only works + on goals containing no existential variables and {\tacexpr} must + either solve the goal completely or do nothing (i.e. it cannot make + some progress). + {\tt par:} can only be used at the toplevel of a tactic expression. + +\end{Variants} + +\ErrMsg \errindex{No such goal} \subsubsection[For loop]{For loop\tacindex{do} \index{Tacticals!do@{\tt do}}} @@ -782,7 +847,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 +1091,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 @@ -1103,7 +1168,7 @@ using the syntax: \end{quote} A previous definition of {\qualid} must exist in the environment. The new definition will always be used instead of the old one and -it goes accross module boundaries. +it goes across module boundaries. If preceded by the keyword {\tt Local} the tactic definition will not be exported outside the current module. @@ -1116,6 +1181,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 +1261,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 Ltac Profile}. +\end{quote} +Resets the profile, that is, deletes all accumulated information. Note that backtracking across a {\tt Reset Ltac Profile} will not restore the 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 +1374,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 +1700,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 +1720,7 @@ Qed. \label{isoslem} \end{figure} -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% End: +%%% End: diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index aea2bae38d..56ce753cd6 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -87,7 +87,7 @@ is restored when the current \emph{section} ends. \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\ This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is +if set in a file, {\rm\sl flag} is switched off when the file is {\tt Require}-d. \end{Variants} @@ -914,6 +914,19 @@ This command turns off the normal displaying. \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. +\subsection[\tt Set Warnings ``(\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$)''.]{{\tt Set Warnings ``(\nterm{w}$_1$,\ldots,% + \nterm{w}$_n$)''}.\optindex{Warnings}} +\label{SetWarnings} +This command configures the display of warnings. It is experimental, and +expects, between quotes, a comma-separated list of warning names or +categories. Adding~\texttt{-} in front of a warning or category disables it, +adding~\texttt{+} makes it an error. It is possible to use the special +categories \texttt{all} and \texttt{default}, the latter containing the warnings +enabled by default. The flags are interpreted from left to right, so in case of +an overlap, the flags on the right have higher priority, meaning that +\texttt{A,-A} is equivalent to \texttt{-A}. + \subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only} \label{Search-Output-Name-Only} \index{Search Output Name Only mode}} @@ -947,6 +960,14 @@ time of writing this documentation, the default value is 50). \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}} This command displays the current nesting depth used for display. +\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} +This command enables the printing of the ``{\tt (dependent evars: \ldots)}'' +line when {\tt -emacs} is passed. + +\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} +This command disables the printing of the ``{\tt (dependent evars: \ldots)}'' +line when {\tt -emacs} is passed. + %\subsection{\tt Abstraction ...} %Not yet documented. diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index cb2ab5dc2f..f36969e821 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1087,6 +1087,139 @@ Paris, January 2015, revised December 2015,\\ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\ \end{flushright} +\section*{Credits: version 8.6} + +{\Coq} version 8.6 contains the result of refinements, stabilization of +8.5's features and cleanups of the internals of the system. Over the +year of (now time-based) development, about 450 bugs were resolved and +over 100 contributions integrated. The main user visible changes are: +\begin{itemize} +\item A new, faster state-of-the-art universe constraint checker, by + Jacques-Henri Jourdan. +\item In CoqIDE and other asynchronous interfaces, more fine-grained + asynchronous processing and error reporting by Enrico Tassi, making {\Coq} + capable of recovering from errors and continue processing the document. +\item More access to the proof engine features from Ltac: goal + management primitives, range selectors and a {\tt typeclasses + eauto} engine handling multiple goals and multiple successes, by + Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. +\item Tactic behavior uniformization and specification, generalization + of intro-patterns by Hugo Herbelin and others. +\item A brand new warning system allowing to control warnings, turn them + into errors or ignore them selectively by Maxime Dénès, Guillaume + Melquiond, Pierre-Marie Pédrot and others. +\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre. +\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and + Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching} + plugin. +\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason + Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi. +\end{itemize} + +{\Coq} 8.6 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system. We shall +only list a few of them. + +The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt + fix} and {\tt cofix} flags controlling the corresponding reduction +rules (by Hugo Herbelin and Maxime Dénès). + +Maxime Dénès maintained the native compilation machinery. + +Pierre-Marie Pédrot separated the Ltac code from general purpose +tactics, and generalized and rationalized the handling of generic +arguments, allowing to create new versions of Ltac more easily in the +future. + +In patterns and terms, {\tt @}, abbreviations and notations are now +interpreted the same way, by Hugo Herbelin. + +Name handling for universes has been improved by Pierre-Marie Pédrot and +Matthieu Sozeau. The minimization algorithm has been improved by +Matthieu Sozeau. + +The unifier has been improved by Hugo Herbelin and Matthieu Sozeau, +fixing some incompatibilities introduced in Coq 8.5. Unification +constraints can now be left floating around and be seen by the user +thanks to a new option. The {\tt Keyed Unification} mode has been +improved by Matthieu Sozeau. + +The typeclass resolution engine and associated proof-search tactic have +been reimplemented on top of the proof-engine monad, providing better +integration in tactics, and new options have been introduced to control +it, by Matthieu Sozeau with help from Théo Zimmermann. + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and +Matthieu Sozeau and performance issue tracking by Jason Gross and Paul +Steckler. + +Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre +Letouzey and others. + +Emilio Jesús Gallego Arias contributed many cleanups and refactorings of +the pretty-printing and user interface communication components. + +Frédéric Besson maintained the micromega tactic. + +The OPAM repository for {\Coq} packages has been maintained by Guillaume +Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A +list of packages is now available at \url{https://coq.inria.fr/opam/www/}. + +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly +built on the continuous integration server. {\Coq} now comes with a {\tt + META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús +Gallego Arias, Gregory Malecha, and Matthieu Sozeau. + +Matej Košík maintained and greatly improved the continuous integration +setup and the testing of {\Coq} contributions. He also contributed many +API improvement and code cleanups throughout the system. + +The contributors for this version are Bruno Barras, C.J. Bell, Yves +Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume +Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin, +Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, +Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, +Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel +de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, +Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent +Théry, Nickolai Zeldovich and Théo Zimmermann. The development process +was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of +Maxime Dénès, who was also in charge of the release process. + +Many power users helped to improve the design of the new features via +the bug tracker, the pull request system, the {\Coq} development mailing +list or the coq-club mailing list. Special thanks to the users who +contributed patches and intensive brain-storming and code reviews, +starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan +Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel +Scherer and Beta Ziliani. It would however be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.6 is the first release of {\Coq} developed on a time-based +development cycle. Its development spanned 10 months from the release of +{\Coq} 8.5 and was based on a public roadmap. To date, it contains more +external contributions than any previous {\Coq} system. Code reviews +were systematically done before integration of new features, with an +important focus given to compatibility and performance issues, resulting +in a hopefully more robust release than {\Coq} 8.5. + +Coq Enhancement Proposals (CEPs for short) were introduced by Enrico +Tassi to provide more visibility and a discussion period on new +features, they are publicly available \url{https://github.com/coq/ceps}. + +Started during this period, an effort is led by Yves Bertot and Maxime +Dénès to put together a {\Coq} consortium. + +\begin{flushright} +Paris, November 2016,\\ +Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + %new Makefile diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 1f08b6a2f1..21c39de967 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -321,6 +321,10 @@ Sometimes, a notation is expected only for the parser. To do so, the option {\em only parsing} is allowed in the list of modifiers of \texttt{Notation}. +Conversely, the {\em only printing} can be used to declare +that a notation should only be used for printing and should not declare a +parsing rule. In particular, such notations do not modify the parser. + \subsection{The \texttt{Infix} command \comindex{Infix}} @@ -480,6 +484,7 @@ Locate "exists _ .. _ , _". & $|$ & {\ident} {\tt global} \\ & $|$ & {\ident} {\tt bigint} \\ & $|$ & {\tt only parsing} \\ + & $|$ & {\tt only printing} \\ & $|$ & {\tt format} {\str} \end{tabular} \end{centerframe} @@ -584,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := (t at level 39). \end{coq_example*} +Recursive patterns can occur several times on the right-hand side. +Here is an example: + +\begin{coq_example*} +Notation "[> a , .. , b <]" := + (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). +\end{coq_example*} + Notations with recursive patterns can be reserved like standard notations, they can also be declared within interpretation scopes (see section \ref{scopes}). @@ -629,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders: \begin{coq_example*} Notation "'mylet' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (x closed binder, y closed binder, at level 200, right associativity). + (at level 200, x closed binder, y closed binder, right associativity). +\end{coq_example*} + +A recursive pattern for binders can be used in position of a recursive +pattern for terms. Here is an example: + +\begin{coq_example*} +Notation "'FUNAPP' x .. y , f" := + (fun x => .. (fun y => (.. (f x) ..) y ) ..) + (at level 200, x binder, y binder, right associativity). \end{coq_example*} \subsection{Summary} @@ -789,13 +811,13 @@ constant have to be interpreted in a given scope. The command is \begin{quote} {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} \end{quote} -where the list is the list of the arguments of {\qualid} eventually -annotated with their {\scope}. Grouping round parentheses can -be used to decorate multiple arguments with the same scope. -{\scope} can be either a scope name or its delimiting key. For example -the following command puts the first two arguments of {\tt plus\_fct} -in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the -last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}). +where the list is a prefix of the list of the arguments of {\qualid} eventually +annotated with their {\scope}. Grouping round parentheses can be used to +decorate multiple arguments with the same scope. {\scope} can be either a scope +name or its delimiting key. For example the following command puts the first two +arguments of {\tt plus\_fct} in the scope delimited by the key {\tt F} ({\tt + Rfun\_scope}) and the last argument in the scope delimited by the key {\tt R} +({\tt R\_scope}). \begin{coq_example*} Arguments plus_fct (f1 f2)%F x%R. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 54450fe7dc..3f12411863 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -42,19 +42,17 @@ language will be described in Chapter~\ref{TacticLanguage}. \index{tactic@{\tac}}} A tactic is applied as an ordinary command. It may be preceded by a -goal selector: {\tt all} if the tactic is to be applied to every -focused goal simultaneously, or a natural number $n$ if it is to be -applied to the $n$-th goal. If no selector is specified, the default +goal selector (see Section \ref{ltac:selector}). +If no selector is specified, the default selector (see Section \ref{default-selector}) is used. -\newcommand{\selector}{\nterm{selector}} +\newcommand{\toplevelselector}{\nterm{toplevel\_selector}} \begin{tabular}{lcl} -{\selector} & := & {\tt all} | {\num}\\ -{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\ +{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\ & $|$ & {\tac} {\tt .} \end{tabular} -\subsection[\tt Set Default Goal Selector ``\selector''.] - {\tt Set Default Goal Selector ``\selector''. +\subsection[\tt Set Default Goal Selector ``\toplevelselector''.] + {\tt Set Default Goal Selector ``\toplevelselector''. \optindex{Default Goal Selector} \label{default-selector}} After using this command, the default selector -- used when no selector @@ -63,7 +61,9 @@ initial value is $1$, hence the tactics are, by default, applied to the first goal. Using {\tt Set Default Goal Selector ``all''} will make is so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic {\tt tac} to the first goal -only, you can write {\tt 1:tac}. +only, you can write {\tt 1:tac}. Although more selectors are available, +only {\tt ``all''} or a single natural number are valid default +goal selectors. \subsection[\tt Test Default Goal Selector.] {\tt Test Default Goal Selector.} @@ -114,7 +114,7 @@ following syntax: \begin{tabular}{lcl} {\occclause} & ::= & {\tt in} {\occgoalset} \\ {\occgoalset} & ::= & - \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ + \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ & & {\dots} {\tt ,}\\ & & {\ident$_m$} \zeroone{\atoccurrences}}\\ & & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\ @@ -263,6 +263,16 @@ Defined. This tactic behaves like {\tt refine}, but it does not shelve any subgoal. It does not perform any beta-reduction either. +\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine} + + This tactic behaves like {\tt refine} except it performs typechecking + without resolution of typeclasses. + +\item {\tt simple notypeclasses refine \term}\tacindex{simple + notypeclasses refine} + + This tactic behaves like {\tt simple refine} except it performs typechecking + without resolution of typeclasses. \end{Variants} \subsection{\tt apply \term} @@ -292,7 +302,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}. \begin{ErrMsgs} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} The {\tt apply} tactic failed to match the conclusion of {\term} and the current goal. @@ -1278,7 +1288,7 @@ in the list of subgoals remaining to prove. In particular, \texttt{pose proof {\term} as {\ident}} behaves as \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term} - as {\intropattern}\tacindex{pose proof}} is the same as applying + as {\intropattern}} is the same as applying the {\intropattern} to {\term}. \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} @@ -1491,10 +1501,10 @@ the local context. \tacindex{contradiction} This tactic applies to any goal. The {\tt contradiction} tactic -attempts to find in the current context (after all {\tt intros}) one -hypothesis that is equivalent to {\tt False}. It permits to prune -irrelevant cases. This tactic is a macro for the tactics sequence -{\tt intros; elimtype False; assumption}. +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. \begin{ErrMsgs} \item \errindex{No such assumption} @@ -2280,6 +2290,21 @@ hypothesis. \end{Variants} +\optindex{Structural Injection} + +It is possible to ensure that \texttt{injection {\term}} erases the +original hypothesis and leaves the generated equalities in the context +rather than putting them as antecedents of the current goal, as if +giving \texttt{injection {\term} as} (with an empty list of names). To +obtain this behavior, the option {\tt Set Structural Injection} must +be activated. This option is off by default. + +By default, \texttt{injection} only creates new equalities between +terms whose type is in sort \texttt{Type} or \texttt{Set}, thus +implementing a special behavior for objects that are proofs +of a statement in \texttt{Prop}. This behavior can be turned off +by setting the option \texttt{Set Keep Proof Equalities}. +\optindex{Keep Proof Equalities} \subsection{\tt inversion \ident} \tacindex{inversion} @@ -2299,6 +2324,14 @@ latter is first introduced in the local context using stock the lemmas whenever the same instance needs to be inverted several times. See Section~\ref{Derive-Inversion}. +\Rem Part of the behavior of the \texttt{inversion} tactic is to generate +equalities between expressions that appeared in the hypothesis that is +being processed. By default, no equalities are generated if they relate +two proofs (i.e. equalities between terms whose type is in +sort \texttt{Prop}). This behavior can be turned off by using the option +\texttt{Set Keep Proof Equalities.} +\optindex{Keep Proof Equalities} + \begin{Variants} \item \texttt{inversion \num} @@ -2872,6 +2905,9 @@ activated, {\tt subst} also deals with the following corner cases: subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ respectively. +\item The presence of a recursive equation which without the option + would be a cause of failure of {\tt subst}. + \item A context with cyclic dependencies as with hypotheses {\tt \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}. @@ -3030,8 +3066,10 @@ $\beta$ (reduction of functional application), $\delta$ (unfolding of transparent constants, see \ref{Transparent}), $\iota$ (reduction of pattern-matching over a constructed term, and unfolding of {\tt fix} and {\tt cofix} expressions) and $\zeta$ (contraction of local -definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota} -or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt +definitions), the flags are either {\tt beta}, {\tt delta}, +{\tt match}, {\tt fix}, {\tt cofix}, {\tt iota} or {\tt zeta}. +The {\tt iota} flag is a shorthand for {\tt match}, {\tt fix} and {\tt cofix}. +The {\tt delta} flag itself can be refined into {\tt delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta -[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the constants to unfold to the constants listed, and restricting in the @@ -3279,6 +3317,16 @@ reduced to \texttt{S t}. \end{Variants} +\begin{quote} +\optindex{Refolding Reduction} +{\tt Refolding Reduction} +\end{quote} + +This option (off by default) controls the use of the refolding strategy +of {\tt cbn} while doing reductions in unification, type inference and +tactic applications. It can result in expensive unifications, as +refolding currently uses a potentially exponential heuristic. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} @@ -3451,12 +3499,11 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} - Uses all existing hint databases, minus the special database - {\tt v62}. See Section~\ref{Hints-databases} + Uses all existing hint databases. See Section~\ref{Hints-databases} \item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ @@ -3465,9 +3512,17 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ +\item {\tt info\_auto} - This combines the effects of the {\tt using} and {\tt with} options. + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. \item {\tt trivial}\tacindex{trivial} @@ -3479,6 +3534,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3492,8 +3555,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. This tactic generalizes {\tt auto}. While {\tt auto} does not try resolution hints which would leave existential variables in the goal, -{\tt eauto} does try them (informally speaking, it uses {\tt eapply} -where {\tt auto} uses {\tt apply}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3508,8 +3571,17 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. + +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} \SeeAlso Section~\ref{Hints-databases} @@ -3655,19 +3727,22 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is The {\hintdef} is one of the following expressions: \begin{itemize} -\item {\tt Resolve \term} +\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}} \comindex{Hint Resolve} This command adds {\tt simple apply {\term}} to the hint list with the head symbol of the type of \term. The cost of that hint is - the number of subgoals generated by {\tt simple apply {\term}}. + the number of subgoals generated by {\tt simple apply {\term}} or \num + if specified. The associated pattern is inferred from the conclusion + of the type of \term or the given \pattern if specified. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % 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 - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not @@ -3697,6 +3772,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} @@ -3832,17 +3918,19 @@ Abort. \comindex{Hint Cut} \textit{Warning:} these hints currently only apply to typeclass proof search and - the \texttt{typeclasses eauto} tactic. + the \texttt{typeclasses eauto} tactic (\ref{typeclasseseauto}). This command can be used to cut the proof-search tree according to a regular expression matching paths to be cut. The grammar for regular - expressions is the following: + expressions is the following. Beware, there is no operator precedence + during parsing, one can check with \texttt{Print HintDb} to verify the + current cut expression: \[\begin{array}{lcll} e & ::= & \ident & \text{ hint or instance identifier } \\ - & & \texttt{*} & \text{ any hint } \\ + & & \texttt{\_} & \text{ any hint } \\ & & e | e' & \text{ disjunction } \\ - & & e ; e' & \text{ sequence } \\ - & & ! e & \text{ Kleene star } \\ + & & e e' & \text{ sequence } \\ + & & e * & \text{ Kleene star } \\ & & \texttt{emp} & \text{ empty } \\ & & \texttt{eps} & \text{ epsilon } \\ & & \texttt{(} e \texttt{)} & @@ -3860,25 +3948,33 @@ is to set the cut expression to $c | e$, the initial cut expression being \texttt{emp}. -\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid} +\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. +hints associated to qualid can be applied or not. A mode specification +is a list of $n$ {\tt +}, {\tt !} or {\tt -} items that specify if an +argument of the identifier is to be treated as an input ({\tt +}), if +its head only is an input ({\tt !}) or an output ({\tt -}) of the +identifier. For a mode to match a list of arguments, input terms and +input heads \emph{must not} contain existential variables or be +existential variables respectively, 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. + +The head of a term is understood here as the applicative head, or the +match or projection scrutinee's head, recursively, casts being ignored. {\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. +to be driven by that index of the class, with {\tt !} giving more +flexibility by allowing existentials to still appear deeper in the index +but not at its head. \end{itemize} @@ -3914,8 +4010,8 @@ Several hint databases are defined in the \Coq\ standard library. The actual content of a database is the collection of the hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules potentially extend a -database. At {\Coq} startup, only the {\tt core} and {\tt v62} -databases are non empty and can be used. +database. At {\Coq} startup, only the {\tt core} database is non empty +and can be used. \begin{description} @@ -3950,18 +4046,8 @@ databases are non empty and can be used. from the \texttt{Classes} directory. \end{description} -There is also a special database called {\tt v62}. It collects all -hints that were declared in the versions of {\Coq} prior to version -6.2.4 when the databases {\tt core}, {\tt arith}, and so on were -introduced. The purpose of the database {\tt v62} is to ensure -compatibility with further versions of {\Coq} for developments done in -versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}). -The database {\tt v62} is intended not to be extended (!). It is not -included in the hint databases list used in the {\tt auto with *} tactic. - -Furthermore, you are advised not to put your own hints in the -{\tt core} database, but use one or several databases specific to your -development. +You are advised not to put your own hints in the {\tt core} database, +but use one or several databases specific to your development. \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ \mbox{\dots} \ident$_m$} @@ -4322,22 +4408,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder Tries to solve the goal with {\tac} when no logical rule may apply. - \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } - \tacindex{firstorder with} - - Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search - environment. - \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ } \tacindex{firstorder using} - Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$ - to the proof-search environment. If {\qualid}$_i$ refers to an inductive - type, it is the collection of its constructors which is added as hints. + Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search + environment. If {\qualid}$_i$ refers to an inductive type, it is + the collection of its constructors which are added to the + proof-search environment. + + \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} + + Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$ + to the proof-search environment. -\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} +\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} - This combines the effects of the {\tt using} and {\tt with} options. + This combines the effects of the different variants of \texttt{firstorder}. \end{Variants} @@ -4534,7 +4621,7 @@ It is equivalent to {\tt apply refl\_equal}. \begin{ErrMsgs} \item \errindex{The conclusion is not a substitutive equation} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} \end{ErrMsgs} \subsection{\tt symmetry} diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 3e29886762..797b0adedd 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -1012,7 +1012,7 @@ the different kinds of errors used in \Coq{} : \fun{val Std.error : string -> 'a} {For simple error messages} -\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a} +\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a} {See Section~\ref{PrettyPrinter} : this can be used if the user want to display a term or build a complex error message} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c282083b5c..9962ce9961 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -102,7 +102,7 @@ generator using for instance the command: This command generates a file \texttt{Makefile} that can be used to compile all the sources of the current project. It follows the -syntax described by the output of \texttt{\% coq\_makefile ----help}. +syntax described by the output of \texttt{\% coq\_makefile -{}-help}. Once the \texttt{Makefile} file has been generated a first time, it can be used by the \texttt{make} command to compile part or all of the project. Note that once it has been generated once, as soon as @@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}. The following command generates a minimal example of \texttt{\_CoqProject} file: \begin{quotation} -\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name - '*.v' -print \} > \_CoqProject} +\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name + "*.v" -print ) > \_CoqProject} \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files @@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some files. {\ProofGeneral} is developed and distributed independently of the -system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. +system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!. \section[Module specification]{Module specification\label{gallina}\ttindex{gallina}} 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/refman/biblio.bib b/doc/refman/biblio.bib index 70ee1f41f0..e69725838e 100644 --- a/doc/refman/biblio.bib +++ b/doc/refman/biblio.bib @@ -1199,7 +1199,7 @@ Decomposition}}, @Misc{ProofGeneral, author = {David Aspinall}, title = {Proof General}, - note = {\url{http://proofgeneral.inf.ed.ac.uk/}} + note = {\url{https://proofgeneral.github.io/}} } @Book{CoqArt, diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a12983ab84..9216c81fcd 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 @@ -614,5 +616,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq84.v theories/Compat/Coq85.v + theories/Compat/Coq86.v </dd> </dl> diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 973a0b75e0..0d537256bb 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -3,6 +3,7 @@ \usepackage[utf8]{inputenc} \usepackage{textcomp} \usepackage{pslatex} +\usepackage{hyperref} \input{../common/version.tex} \input{../common/macros.tex} @@ -17,7 +18,7 @@ \chapter*{Getting started} -\Coq\ is a Proof Assistant for a Logical Framework known as the Calculus +\Coq{} is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It runs as a computer program @@ -29,7 +30,7 @@ possibilities of \Coq, but rather to present in the most elementary manner a tutorial on the basic specification language, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools. For more advanced information, the reader could refer to -the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. +the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y. Bertot and P. Castéran on practical uses of the \Coq{} system. Coq can be used from a standard teletype-like shell window but @@ -39,9 +40,9 @@ and Pcoq.}. Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, -which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}. +which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}. -In the following, we assume that \Coq~ is called from a standard +In the following, we assume that \Coq{} is called from a standard teletype-like shell window. All examples preceded by the prompting sequence \verb:Coq < : represent user input, terminated by a period. @@ -51,10 +52,10 @@ users screen. When used from a graphical user interface such as CoqIde, the prompt is not displayed: user input is given in one window and \Coq's answers are displayed in a different window. -The sequence of such examples is a valid \Coq~ +The sequence of such examples is a valid \Coq{} session, unless otherwise specified. This version of the tutorial has been prepared on a PC workstation running Linux. The standard -invocation of \Coq\ delivers a message such as: +invocation of \Coq{} delivers a message such as: \begin{small} \begin{flushleft} @@ -67,17 +68,17 @@ Coq < \end{flushleft} \end{small} -The first line gives a banner stating the precise version of \Coq~ +The first line gives a banner stating the precise version of \Coq{} used. You should always return this banner when you report an anomaly to our bug-tracking system -\verb|http://logical.futurs.inria.fr/coq-bugs| +\url{https://coq.inria.fr/bugs/}. \chapter{Basic Predicate Calculus} \section{An overview of the specification language Gallina} A formal development in Gallina consists in a sequence of {\sl declarations} -and {\sl definitions}. You may also send \Coq~ {\sl commands} which are +and {\sl definitions}. You may also send \Coq{} {\sl commands} which are not really part of the formal development, but correspond to information requests, or service routine invocations. For instance, the command: \begin{verbatim} @@ -106,7 +107,7 @@ of the system, called respectively \verb:Prop:, \verb:Set:, and Every valid expression $e$ in Gallina is associated with a specification, itself a valid expression, called its {\sl type} $\tau(E)$. We write $e:\tau(E)$ for the judgment that $e$ is of type $E$. -You may request \Coq~ to return to you the type of a valid expression by using +You may request \Coq{} to return to you the type of a valid expression by using the command \verb:Check:: \begin{coq_eval} @@ -130,7 +131,7 @@ Check nat. The specification \verb:Set: is an abstract type, one of the basic sorts of the Gallina language, whereas the notions $nat$ and $O$ are notions which are defined in the arithmetic prelude, -automatically loaded when running the \Coq\ system. +automatically loaded when running the \Coq{} system. We start by introducing a so-called section name. The role of sections is to structure the modelisation by limiting the scope of parameters, @@ -206,7 +207,7 @@ We may optionally indicate the required type: Definition two : nat := S one. \end{coq_example} -Actually \Coq~ allows several possible syntaxes: +Actually \Coq{} allows several possible syntaxes: \begin{coq_example} Definition three := S two : nat. \end{coq_example} @@ -249,7 +250,7 @@ explicitly the type of the quantified variable. We check: Check (forall m:nat, gt m 0). \end{coq_example} We may revert to the clean state of -our initial session using the \Coq~ \verb:Reset: command: +our initial session using the \Coq{} \verb:Reset: command: \begin{coq_example} Reset Initial. \end{coq_example} @@ -340,7 +341,7 @@ assumption. \end{coq_example} The proof is now finished. We may either discard it, by using the -command \verb:Abort: which returns to the standard \Coq~ toplevel loop +command \verb:Abort: which returns to the standard \Coq{} toplevel loop without further ado, or else save it as a lemma in the current context, under name say \verb:trivial_lemma:: \begin{coq_example} @@ -414,7 +415,7 @@ backtrack one step, and more generally \verb:Undo n: to backtrack n steps. We end this section by showing a useful command, \verb:Inspect n.:, -which inspects the global \Coq~ environment, showing the last \verb:n: declared +which inspects the global \Coq{} environment, showing the last \verb:n: declared notions: \begin{coq_example} Inspect 3. @@ -429,7 +430,7 @@ their value (or proof-term) is omitted. \subsection{Conjunction} We have seen how \verb:intro: and \verb:apply: tactics could be combined -in order to prove implicational statements. More generally, \Coq~ favors a style +in order to prove implicational statements. More generally, \Coq{} favors a style of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into so called {\sl introduction rules}, which tell how to prove a goal whose main operator is a given propositional connective, and {\sl elimination rules}, @@ -528,7 +529,7 @@ such a simple tautology. The reason is that we want to keep \subsection{Tauto} A complete tactic for propositional -tautologies is indeed available in \Coq~ as the \verb:tauto: tactic. +tautologies is indeed available in \Coq{} as the \verb:tauto: tactic. \begin{coq_example} Restart. tauto. @@ -555,7 +556,7 @@ The two instantiations are effected automatically by the tactic \verb:apply: when pattern-matching a goal. The specialist will of course recognize our proof term as a $\lambda$-term, used as notation for the natural deduction proof term through the Curry-Howard isomorphism. The -naive user of \Coq~ may safely ignore these formal details. +naive user of \Coq{} may safely ignore these formal details. Let us exercise the \verb:tauto: tactic on a more complex example: \begin{coq_example} @@ -579,7 +580,7 @@ argument fails. This may come as a surprise to someone familiar with classical reasoning. Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation -of Peirce's law may be proved in \Coq~ using \verb:tauto:: +of Peirce's law may be proved in \Coq{} using \verb:tauto:: \begin{coq_example} Abort. Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A). @@ -588,7 +589,7 @@ Qed. \end{coq_example} In classical logic, the double negation of a proposition is equivalent to this -proposition, but in the constructive logic of \Coq~ this is not so. If you +proposition, but in the constructive logic of \Coq{} this is not so. If you want to use classical logic in \Coq, you have to import explicitly the \verb:Classical: module, which will declare the axiom \verb:classic: of excluded middle, and classical tautologies such as de Morgan's laws. @@ -652,7 +653,7 @@ function and predicate symbols. \subsection{Sections and signatures} Usually one works in some domain of discourse, over which range the individual -variables and function symbols. In \Coq~ we speak in a language with a rich +variables and function symbols. In \Coq{} we speak in a language with a rich variety of types, so me may mix several domains of discourse, in our multi-sorted language. For the moment, we just do a few exercises, over a domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two @@ -660,7 +661,7 @@ predicate symbols \verb:P: and \verb:R: over \verb:D:, of arities 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 +polluted our \Coq{} session by declaring the variables \verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. \begin{coq_example} @@ -714,7 +715,7 @@ Check ex. \end{coq_example} and the notation \verb+(exists x:D, P x)+ is just concrete syntax for the expression \verb+(ex D (fun x:D => P x))+. -Existential quantification is handled in \Coq~ in a similar +Existential quantification is handled in \Coq{} in a similar fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by the proof combinator \verb:ex_intro:, which is invoked by the specific tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to @@ -951,7 +952,7 @@ Abort. \subsection{Equality} -The basic equality provided in \Coq~ is Leibniz equality, noted infix like +The basic equality provided in \Coq{} is Leibniz equality, noted infix like \verb+x=y+, when \verb:x: and \verb:y: are two expressions of type the same Set. The replacement of \verb:x: by \verb:y: in any term is effected by a variety of tactics, such as \verb:rewrite: @@ -1208,7 +1209,7 @@ About prim_rec. Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we get an apparently more complicated expression. Indeed the type of \verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may -be checked in \Coq~ by command \verb:Eval Cbv Beta:, which $\beta$-reduces +be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces an expression to its {\sl normal form}: \begin{coq_example} Eval cbv beta in @@ -1228,7 +1229,7 @@ That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n: according to its main constructor; when \verb:n = O:, we get \verb:m:; when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result of the recursive computation \verb+(addition p m)+. Let us verify it by -asking \Coq~to compute for us say $2+3$: +asking \Coq{} to compute for us say $2+3$: \begin{coq_example} Eval compute in (addition (S (S O)) (S (S (S O)))). \end{coq_example} @@ -1275,7 +1276,7 @@ as subgoals the corresponding instantiations of the base case \verb:(P O): , and of the inductive step \verb+forall y:nat, P y -> P (S y)+. In each case we get an instance of function \verb:plus: in which its second argument starts with a constructor, and is thus amenable to simplification -by primitive recursion. The \Coq~tactic \verb:simpl: can be used for +by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for this purpose: \begin{coq_example} simpl. @@ -1488,7 +1489,7 @@ Set Printing Width 60. \section{Opening library modules} -When you start \Coq~ without further requirements in the command line, +When you start \Coq{} without further requirements in the command line, you get a bare system with few libraries loaded. As we saw, a standard prelude module provides the standard logic connectives, and a few arithmetic notions. If you want to load and open other modules from @@ -1503,9 +1504,9 @@ Such a command looks for a (compiled) module file \verb:Arith.vo: in the libraries registered by \Coq. Libraries inherit the structure of the file system of the operating system and are registered with the command \verb:Add LoadPath:. Physical directories are mapped to -logical directories. Especially the standard library of \Coq~ is +logical directories. Especially the standard library of \Coq{} is pre-registered as a library of name \verb=Coq=. Modules have absolute -unique names denoting their place in \Coq~ libraries. An absolute +unique names denoting their place in \Coq{} libraries. An absolute name is a sequence of single identifiers separated by dots. E.g. the module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because it resides in eponym subdirectory \verb=Arith= of the standard |