diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/AsyncProofs.tex | 27 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 6 | ||||
| -rw-r--r-- | doc/refman/Extraction.tex | 28 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-int.tex | 14 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 165 | ||||
| -rw-r--r-- | doc/refman/Universes.tex | 65 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
12 files changed, 280 insertions, 57 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7ffe252253..1609e4a041 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -6,7 +6,7 @@ This chapter explains how proofs can be asynchronously processed by Coq. This feature improves the reactivity of the system when used in interactive -mode via CoqIDE. In addition to that, it allows Coq to take advantage of +mode via CoqIDE. In addition, it allows Coq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs objects. @@ -22,7 +22,12 @@ For example, in interactive mode, some errors coming from the kernel of Coq are signaled late. The type of errors belonging to this category are universe inconsistencies. -Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. +At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running CoqIDE in Windows. The +current implementation of the feature is not stable on Windows. It can be +enabled, as described below at \ref{interactivecaveats}, though doing so is not +recommended. \section{Proof annotations} @@ -46,6 +51,12 @@ 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. +\subsubsection{Automatic suggestion of proof annotations} + +The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a +\texttt{Qed} command is processed, a correct proof annotation. It is up +to the user to modify the proof script accordingly. + \section{Proof blocks and error resilience} Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq @@ -81,13 +92,7 @@ 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 -\texttt{Qed} command is processed, a correct proof annotation. It is up -to the user to modify the proof script accordingly. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. \section{Interactive mode} @@ -112,6 +117,7 @@ the kernel to check all the proof objects, one has to click the button with the gears. Only then are all the universe constraints checked. \subsubsection{Caveats} +\label{interactivecaveats} The number of worker processes can be increased by passing CoqIDE the \texttt{-async-proofs-j $n$} flag. Note that the memory consumption @@ -120,7 +126,8 @@ the master process. Also note that increasing the number of workers may 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. +CoqIDE. Conversely, on Windows, where the feature is disabled by default, +pass the \texttt{-async-proofs on} flag to enable it. 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. diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 5966ac468c..7e07868a38 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -486,15 +486,17 @@ where there is a hole in that place. \subsection{\tt Set Typeclasses Legacy Resolution} \optindex{Typeclasses Legacy Resolution} +\emph{Deprecated since 8.7} 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} +\emph{Deprecated since 8.7} This option allows eta-conversion for functions and records during -unification of type-classes. This option is now unsupported in 8.6 with +unification of type-classes. This option is unsupported since 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 @@ -505,7 +507,7 @@ 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 +This option (on by default) 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 diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index fa3d61b1cd..8cb049d50e 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -21,9 +21,14 @@ be used (abusively) to refer to any of the three. Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly -via {\tt Require Extraction}. Note that in earlier versions of Coq, these -commands and options were directly available without any preliminary -{\tt Require}. +via {\tt Require Extraction}, or via the more robust +{\tt From Coq Require Extraction}. +Note that in earlier versions of Coq, these commands and options were +directly available without any preliminary {\tt Require}. + +\begin{coq_example} +Require Extraction. +\end{coq_example} \asection{Generating ML code} \comindex{Extraction} @@ -82,9 +87,20 @@ one monolithic file or one file per \Coq\ library. using prefixes \verb!coq_! or \verb!Coq_!. \end{description} -\noindent The list of globals \qualid$_i$ does not need to be -exhaustive: it is automatically completed into a complete and minimal -environment. +\noindent The following command is meant to help automatic testing of + the extraction, see for instance the {\tt test-suite} directory + in the \Coq\ sources. + +\begin{description} +\item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par + All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all + their dependencies are extracted to a temporary Ocaml file, just as in + {\tt Extraction "{\em file}"}. Then this temporary file and its + signature are compiled with the same Ocaml compiler used to built + \Coq. This command succeeds only if the extraction and the Ocaml + compilation succeed (and it fails if the current target language + of the extraction is not Ocaml). +\end{description} \asection{Extraction options} diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 2fc1c8764a..f60908da6c 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -278,7 +278,8 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations should have their +\emph{Deprecated since 8.7} + This option (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index f338c30551..713f344cbe 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -705,20 +705,20 @@ when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: This command can be seen as a generalization of {\tt Fixpoint}. It is actually a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the -recursive structure of the function (see \ref{FunInduction}), and its +recursive structure of the function (see \ref{FunInduction}) and its fixpoint equality. The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be -given (unless the function is not recursive), but it must not -necessary be \emph{structurally} decreasing. The point of the {\tt +given (unless the function is not recursive), but it might not +necessarily be \emph{structurally} decreasing. The point of the {\tt \{\}} annotation is to name the decreasing argument \emph{and} to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. -The {\tt Function} construction enjoys also the {\tt with} extension +The {\tt Function} construction also enjoys the {\tt with} extension to define mutually recursive definitions. However, this feature does -not work for non structural recursive functions. % VRAI?? +not work for non structurally recursive functions. % VRAI?? See the documentation of {\tt functional induction} (see Section~\ref{FunInduction}) and {\tt Functional Scheme} @@ -749,7 +749,7 @@ Function plus (n m : nat) {struct n} : nat := \end{coq_example*} \paragraph[Limitations]{Limitations\label{sec:Function-limitations}} -\term$_0$ must be build as a \emph{pure pattern-matching tree} +\term$_0$ must be built as a \emph{pure pattern-matching tree} (\texttt{match...with}) with applications only \emph{at the end} of each branch. @@ -776,7 +776,7 @@ For now dependent cases are not treated for non structurally terminating functio The generation of the graph relation \texttt{(R\_\ident)} used to compute the induction scheme of \ident\ raised a typing error. Only - the ident is defined, the induction scheme will not be generated. + the ident is defined; the induction scheme will not be generated. This error happens generally when: @@ -848,14 +848,14 @@ the following: being the decreasing argument and \term$_1$ being a function from type of \ident$_0$ to \texttt{nat} for which value on the decreasing argument decreases (for the {\tt lt} order on {\tt - nat}) at each recursive call of \term$_0$, parameters of the + nat}) at each recursive call of \term$_0$. Parameters of the function are bound in \term$_0$; \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ an ordering relation on the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which the decreasing argument decreases at each recursive call of - \term$_0$. The order must be well founded. parameters of the + \term$_0$. The order must be well founded. Parameters of the function are bound in \term$_0$. \end{itemize} diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index fbeccb664d..eca3efcdd6 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -100,6 +100,11 @@ corresponds to the Chapter~\ref{Addoc-syntax}. presented. Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated development environment. + +\item The fifth part documents a number of advanced features, including + coercions, canonical structures, typeclasses, program extraction, and + specialized solvers and tactics. See the table of contents for a complete + list. \end{itemize} At the end of the document, after the global index, the user can find @@ -120,15 +125,6 @@ documents: user can read also the tutorial on recursive types (document {\tt RecTutorial.ps}). -\item[Addendum] The fifth part (the Addendum) of the Reference Manual - is distributed as a separate document. It contains more - detailed documentation and examples about some specific aspects of the - system that may interest only certain users. It shares the indexes, - the page numbers and - the bibliography with the Reference Manual. If you see in one of the - indexes a page number that is outside the Reference Manual, it refers - to the Addendum. - \item[Installation] A text file INSTALL that comes with the sources explains how to install \Coq{}. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index f3bc2dd05e..3ce1d4ecd8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below. \optindex{Shrink Abstract} {\tt Set Shrink Abstract} \end{quote} +\emph{Deprecated since 8.7} -When set, all lemmas generated through \texttt{abstract {\tacexpr}} +When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the variables that appear in the term constructed by \texttt{\tacexpr}. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3daaac88b1..bf48057cdf 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -656,7 +656,7 @@ dynamically. searched into the current {\ocaml} loadpath (see the command {\tt Add ML Path} in the Section~\ref{loadpath}). Loading of {\ocaml} files is only possible under the bytecode version of {\tt coqtop} -(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter +(i.e. {\tt coqtop.byte}, see chapter \ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11). @@ -739,7 +739,7 @@ the command {\tt Declare ML Module} in the Section~\ref{compiled}). \subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}} This command displays the current {\ocaml} loadpath. This command makes sense only under the bytecode version of {\tt -coqtop}, i.e. using option {\tt -byte} (see the +coqtop}, i.e. {\tt coqtop.byte} (see the command {\tt Declare ML Module} in the section \ref{compiled}). diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ecb89b5fb8..b13ae9b7b3 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3485,6 +3485,7 @@ reduced to \texttt{S t}. \optindex{Refolding Reduction} {\tt Refolding Reduction} \end{quote} +\emph{Deprecated since 8.7} This option (off by default) controls the use of the refolding strategy of {\tt cbn} while doing reductions in unification, type inference and @@ -4112,7 +4113,7 @@ is to set the cut expression to $c | e$, the initial cut expression being \texttt{emp}. -\item \texttt{Mode} {\tt (+ | ! | -)}$^*$ {\qualid} +\item \texttt{Mode} {\qualid} {\tt (+ | ! | -)}$^*$ \label{HintMode} \comindex{Hint Mode} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index fee4de3364..768d0df763 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -60,7 +60,7 @@ subdirectory of the sources. The majority of \Coq\ projects are very similar: a collection of {\tt .v} files and eventually some {\tt .ml} ones (a \Coq\ plugin). The main piece -of metadata needed in order to build the project are the command +of metadata needed in order to build the project are the command line options to {\tt coqc} (e.g. {\tt -R, -I}, \SeeAlso Section~\ref{coqoptions}). Collecting the list of files and options is the job of the {\tt \_CoqProject} file. @@ -108,12 +108,171 @@ used in order to decide how to build them. In particular: \end{itemize} The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib} -files, since it results in a ``packed'' plugin: All auxiliary +files, since it results in a ``packed'' plugin: All auxiliary modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside the plugin's ``name space'' ({\tt Qux\_plugin}). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names. +\paragraph{Timing targets and performance testing} +The generated \texttt{Makefile} supports the generation of two kinds +of timing data: per-file build-times, and per-line times for an +individual file. + +The following targets and \texttt{Makefile} variables allow collection +of per-file timing data: +\begin{itemize} +\item \texttt{TIMED=1} --- passing this variable will cause + \texttt{make} to emit a line describing the user-space build-time + and peak memory usage for each file built. + + \texttt{Note}: On Mac OS, this works best if you've installed + \texttt{gnu-time}. + + \texttt{Example}: For example, the output of \texttt{make TIMED=1} + may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.34 mem: 395448 ko) +COQC Fast.v +Fast (user: 0.01 mem: 45184 ko) +\end{verbatim} +\item \texttt{pretty-timed} --- this target stores the output of + \texttt{make TIMED=1} into \texttt{time-of-build.log}, and displays + a table of the times, sorted from slowest to fastest, which is also + stored in \texttt{time-of-build-pretty.log}. If you want to + construct the log for targets other than the default one, you can + pass them via the variable \texttt{TGTS}, e.g., \texttt{make + pretty-timed TGTS="a.vo b.vo"}. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: This target will \emph{append} to the timing log; if + you want a fresh start, you must remove the file + \texttt{time-of-build.log} or run \texttt{make cleanall}. + + \texttt{Example}: For example, the output of \texttt{make + pretty-timed} may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.36 mem: 393912 ko) +COQC Fast.v +Fast (user: 0.05 mem: 45992 ko) +Time | File Name +-------------------- +0m00.41s | Total +-------------------- +0m00.36s | Slow +0m00.05s | Fast +\end{verbatim} +\item \texttt{print-pretty-timed-diff} --- this target builds a table + of timing changes between two compilations; run \texttt{make + make-pretty-timed-before} to build the log of the ``before'' + times, and run \texttt{make make-pretty-timed-after} to build the + log of the ``after'' times. The table is printed on the command + line, and stored in \texttt{time-of-build-both.log}. This target is + most useful for profiling the difference between two commits to a + repo. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: The \texttt{make-pretty-timed-before} and + \texttt{make-pretty-timed-after} targets will \emph{append} to the + timing log; if you want a fresh start, you must remove the files + \texttt{time-of-build-before.log} and + \texttt{time-of-build-after.log} or run \texttt{make cleanall} + \emph{before} building either the ``before'' or ``after'' targets. + + \texttt{Note}: The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then + by times in the ``after'' column, and finally lexicographically by + file name. This will put the biggest changes in either direction + first, and will prefer sorting by build-time over subsecond changes + in build time (which are frequently noise); lexicographic sorting + forces an order on files which take effectively no time to compile. + + \texttt{Example}: For example, the output table from \texttt{make + print-pretty-timed-diff} may look like this: +\begin{verbatim} +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% +-------------------------------------------------------- +0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% +0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% +\end{verbatim} +\end{itemize} + +The following targets and \texttt{Makefile} variables allow collection +of per-line timing data: +\begin{itemize} +\item \texttt{TIMING=1} --- passing this variable will cause + \texttt{make} to use \texttt{coqc -time} to write to a + \texttt{.v.timing} file for each \texttt{.v} file compiled, which + contains line-by-line timing information. + + \texttt{Example}: For example, running \texttt{make all TIMING=1} may + result in a file like this: +\begin{verbatim} +Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) +Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) +Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) +Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) +\end{verbatim} + +\item \texttt{print-pretty-single-time-diff + BEFORE=path/to/file.v.before-timing + AFTER=path/to/file.v.after-timing} --- this target will make a + sorted table of the per-line timing differences between the timing + logs in the \texttt{BEFORE} and \texttt{AFTER} files, display it, + and save it to the file specified by the + \texttt{TIME\_OF\_PRETTY\_BUILD\_FILE} variable, which defaults to + \texttt{time-of-build-pretty.log}. + + To generate the \texttt{.v.before-timing} or + \texttt{.v.after-timing} files, you should pass + \texttt{TIMING=before} or \texttt{TIMING=after} rather than + \texttt{TIMING=1}. + + \texttt{Note}: The sorting used here is the same as in the + \texttt{print-pretty-timed-diff} target. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Example}: For example, running + \texttt{print-pretty-single-time-diff} might give a table like this: +\begin{verbatim} +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% +\end{verbatim} + +\item \texttt{all.timing.diff}, \texttt{path/to/file.v.timing.diff} + --- The \texttt{path/to/file.v.timing.diff} target will make a + \texttt{.v.timing.diff} file for the corresponding \texttt{.v} file, + with a table as would be generated by the + \texttt{print-pretty-single-time-diff} target; it depends on having + already made the corresponding \texttt{.v.before-timing} and + \texttt{.v.after-timing} files, which can be made by passing + \texttt{TIMING=before} and \texttt{TIMING=after}. The + \texttt{all.timing.diff} target will make such timing difference + files for all of the \texttt{.v} files that the \texttt{Makefile} + knows about. It will fail if some \texttt{.v.before-timing} or + \texttt{.v.after-timing} files don't exist. + + \texttt{Note}: This target requires \texttt{python} to build the table. +\end{itemize} + \paragraph{Notes about including the generated Makefile} This practice is discouraged. The contents of this file, including variable names @@ -165,7 +324,7 @@ invoke-coqmakefile: CoqMakefile or after the build (like invoking make on a subdirectory) one can hook in {\tt pre-all} and {\tt post-all} extension points \item \texttt{-extra-phony} and \texttt{-extra} are deprecated. To provide - additional target ({\tt .PHONY} or not) please use + additional target ({\tt .PHONY} or not) please use {\tt CoqMakefile.local} \end{itemize} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 2bb1301c79..cd36d1d320 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -134,12 +134,14 @@ producing global universe constraints, one can use the \asection{{\tt Cumulative, NonCumulative}} \comindex{Cumulative} \comindex{NonCumulative} -\optindex{Inductive Cumulativity} +\optindex{Polymorphic Inductive Cumulativity} -Inductive types, coinductive types, variants and records can be +Polymorphic inductive types, coinductive types, variants and records can be declared cumulative using the \texttt{Cumulative}. Alternatively, -there is an option \texttt{Set Inductive Cumulativity} which when set, -makes all subsequent inductive definitions cumulative. Consider the examples below. +there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, +makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, +inductive types and the like can be enforced to be +\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below. \begin{coq_example*} Polymorphic Cumulative Inductive list {A : Type} := | nil : list @@ -158,24 +160,61 @@ This also means that any two instances of \texttt{list} are convertible: $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully applied to convertible arguments) constructors. See Chapter~\ref{Cic} for more details on convertibility and subtyping. -Also notice the subtyping constraints for the \emph{non-cumulative} version of list: +The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} -Polymorphic NonCumulative Inductive list' {A : Type} := -| nil' : list' -| cons' : A -> list' -> list'. +Polymorphic Cumulative Record packType := {pk : Type}. \end{coq_example*} \begin{coq_example} -Print list'. +Print packType. +\end{coq_example} +Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are +convertible if and only if \texttt{i $=$ j}. + +Cumulative inductive types, coninductive types, variants and records +only make sense when they are universe polymorphic. Therefore, an +error is issued whenever the user uses the \texttt{Cumulative} or +\texttt{NonCumulative} prefix in a monomorphic context. +Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}. +That is, this option, when set, makes all subsequent \emph{polymorphic} +inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used) +but has no effect on \emph{monomorphic} inductive declarations. +Consider the following examples. +\begin{coq_example} +Monomorphic Cumulative Inductive Unit := unit. +\end{coq_example} +\begin{coq_example} +Monomorphic NonCumulative Inductive Unit := unit. \end{coq_example} -The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} -Polymorphic Cumulative Record packType := {pk : Type}. +Set Polymorphic Inductive Cumulativity. +Inductive Unit := unit. \end{coq_example*} \begin{coq_example} -Print packType. +Print Unit. \end{coq_example} -Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. +\subsection*{An example of a proof using cumulativity} + +\begin{coq_example} +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. + +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + +Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + +Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. + Proof. + exact H. + Defined. +\end{coq_example} \asection{Global and local universes} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 48f82f2d92..48048b7a0f 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -591,5 +591,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq85.v theories/Compat/Coq86.v + theories/Compat/Coq87.v </dd> </dl> |