diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 108 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 46 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 6 |
12 files changed, 116 insertions, 116 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 96e115fc3d..3662822a5e 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -5,10 +5,10 @@ Program extraction :Authors: Jean-Christophe Filliâtre and Pierre Letouzey -We present here the |Coq| extraction commands, used to build certified +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|, Haskell +either Coq functions or Coq proofs of specifications. The +functional languages available as output are currently OCaml, Haskell and Scheme. In the following, "ML" will be used (abusively) to refer to any of the three. @@ -16,7 +16,7 @@ Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly via ``Require Extraction``, or via the more robust ``From Coq Require Extraction``. -Note that in earlier versions of |Coq|, these commands and options were +Note that in earlier versions of Coq, these commands and options were directly available without any preliminary ``Require``. .. coqtop:: in @@ -29,23 +29,23 @@ Generating ML Code .. note:: In the following, a qualified identifier :token:`qualid` - can be used to refer to any kind of |Coq| global "object" : constant, + can be used to refer to any kind of Coq global "object" : constant, inductive type, inductive constructor or module name. The next two commands are meant to be used for rapid preview of -extraction. They both display extracted term(s) inside |Coq|. +extraction. They both display extracted term(s) inside Coq. .. cmd:: Extraction @qualid - Extraction of the mentioned object in the |Coq| toplevel. + Extraction of the mentioned object in the Coq toplevel. .. cmd:: Recursive Extraction {+ @qualid } Recursive extraction of all the mentioned objects and - all their dependencies in the |Coq| toplevel. + all their dependencies in the Coq toplevel. All the following commands produce real ML files. User can choose to -produce one monolithic file or one file per |Coq| library. +produce one monolithic file or one file per Coq library. .. cmd:: Extraction @string {+ @qualid } @@ -57,14 +57,14 @@ produce one monolithic file or one file per |Coq| library. .. cmd:: Extraction Library @ident - Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + Extraction of the whole Coq library :n:`@ident.v` to an ML module :n:`@ident.ml`. In case of name clash, identifiers are here renamed using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. .. cmd:: Recursive Extraction Library @ident - Extraction of the |Coq| library :n:`@ident.v` and all other modules + Extraction of the Coq library :n:`@ident.v` and all other modules :n:`@ident.v` depends on. .. cmd:: Separate Extraction {+ @qualid } @@ -72,26 +72,26 @@ produce one monolithic file or one file per |Coq| library. Recursive extraction of all the mentioned objects and all their dependencies, just as :n:`Extraction @string {+ @qualid }`, but instead of producing one monolithic file, this command splits - the produced code in separate ML files, one per corresponding |Coq| + the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to :cmd:`Recursive Extraction Library`, except that only the needed - parts of |Coq| libraries are extracted instead of the whole. + parts of Coq libraries are extracted instead of the whole. The naming convention in case of name clash is the same one as :cmd:`Extraction Library`: identifiers are here renamed using prefixes ``coq_`` or ``Coq_``. The following command is meant to help automatic testing of the extraction, see for instance the ``test-suite`` directory -in the |Coq| sources. +in the Coq sources. .. cmd:: Extraction TestCompile {+ @qualid } All the mentioned objects and all their dependencies are extracted - to a temporary |OCaml| file, just as in ``Extraction "file"``. Then + to a temporary OCaml file, just as in ``Extraction "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. It fails - if the current target language of the extraction is not |OCaml|. + OCaml compiler used to built Coq. This command succeeds only + if the extraction and the OCaml compilation succeed. It fails + if the current target language of the extraction is not OCaml. Extraction Options ------------------- @@ -120,17 +120,17 @@ Setting the target language Inlining and optimizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since |OCaml| is a strict language, the extracted code has to +Since OCaml is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -wants to generate an |OCaml| program. The optimizations can be split in two +wants to generate an OCaml program. The optimizations can be split in two groups: the type-preserving ones (essentially constant inlining and reductions) and the non type-preserving ones (some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types). Therefore some constants may not appear in the -resulting monolithic |OCaml| program. In the case of modular extraction, +resulting monolithic OCaml program. In the case of modular extraction, even if some inlining is done, the inlined constants are nevertheless printed, to ensure session-independent programs. @@ -138,7 +138,7 @@ Concerning Haskell, type-preserving optimizations are less useful because of laziness. We still make some optimizations, for example in order to produce more readable code. -The type-preserving optimizations are controlled by the following |Coq| flags +The type-preserving optimizations are controlled by the following Coq flags and commands: .. flag:: Extraction Optimize @@ -146,7 +146,7 @@ and commands: Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this flag off if you want a - ML term as close as possible to the |Coq| term. + ML term as close as possible to the Coq term. .. flag:: Extraction Conservative Types @@ -199,7 +199,7 @@ The user can explicitly ask for a constant to be extracted by two means: * by mentioning it on the extraction command line - * by extracting the whole |Coq| module of this constant. + * by extracting the whole Coq module of this constant. In both cases, the declaration of this constant will be present in the produced file. But this same constant may or may not be inlined in @@ -321,7 +321,7 @@ Realizing inductive types The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML -native boolean type instead of the |Coq| one. The syntax is the following: +native boolean type instead of the Coq one. The syntax is the following: .. cmd:: Extract Inductive @qualid => {| @ident | @string } [ {* {| @ident | @string } } ] {? @string__match } @@ -350,7 +350,7 @@ native boolean type instead of the |Coq| one. The syntax is the following: arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional form ``(fun () -> bar)``. For instance, when extracting :g:`nat` - into |OCaml| ``int``, the code to be provided has type: + into OCaml ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. .. caution:: As for :cmd:`Extract Constant`, this command should be used with care: @@ -361,15 +361,15 @@ native boolean type instead of the |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern matching) will often **not** be fully rigorously - correct. For instance, when extracting ``nat`` to |OCaml| ``int``, + correct. For instance, when extracting ``nat`` to OCaml ``int``, it is theoretically possible to build ``nat`` values that are - larger than |OCaml| ``max_int``. It is the user's responsibility to + larger than OCaml ``max_int``. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. * Translating an inductive type to an arbitrary ML type does **not** magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting - ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic. + ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic. It might be interesting to associate this translation with some specific :cmd:`Extract Constant` when primitive counterparts exist. @@ -383,9 +383,9 @@ Typical examples are the following: .. note:: - When extracting to |OCaml|, if an inductive constructor or type has arity 2 and + When extracting to OCaml, if an inductive constructor or type has arity 2 and the corresponding string is enclosed by parentheses, and the string meets - |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is + OCaml's lexical criteria for an infix symbol, then the rest of the string is used as an infix constructor or type. .. coqtop:: in @@ -394,7 +394,7 @@ Typical examples are the following: Extract Inductive prod => "(*)" [ "(,)" ]. As an example of translation to a non-inductive datatype, let's turn -``nat`` into |OCaml| ``int`` (see caveat above): +``nat`` into OCaml ``int`` (see caveat above): .. coqtop:: in @@ -404,11 +404,11 @@ Avoiding conflicts with existing filenames ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When using :cmd:`Extraction Library`, the names of the extracted files -directly depend on the names of the |Coq| files. It may happen that +directly depend on the names of the Coq files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module ``List`` exists both in |Coq| and in |OCaml|. +For instance the module ``List`` exists both in Coq and in OCaml. It is possible to instruct the extraction not to use particular filenames. .. cmd:: Extraction Blacklist {+ @ident } @@ -424,7 +424,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. -For |OCaml|, a typical use of these commands is +For OCaml, a typical use of these commands is ``Extraction Blacklist String List``. Additional settings @@ -440,7 +440,7 @@ Additional settings Controls which optimizations are used during extraction, providing a finer-grained control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. - Keeping an option off keeps the extracted ML more similar to the |Coq| term. + Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: +-----+-------+----------------------------------------------------------------+ @@ -471,14 +471,14 @@ Additional settings .. flag:: Extraction TypeExpand - If set, fully expand |Coq| types in ML. See the |Coq| source code to learn more. + If set, fully expand Coq types in ML. See the Coq source code to learn more. -Differences between |Coq| and ML type systems +Differences between Coq and ML type systems ---------------------------------------------- -Due to differences between |Coq| and ML type systems, +Due to differences between Coq and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in |OCaml|) by adding +We now solve this problem (at least in OCaml) by adding when needed some unsafe casting ``Obj.magic``, which give a generic type ``'a`` to any term. @@ -492,7 +492,7 @@ function: Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). -In |OCaml|, for instance, the direct extracted term would be:: +In OCaml, for instance, the direct extracted term would be:: let dp x y f = Pair((f () x),(f () y)) @@ -506,7 +506,7 @@ We now produce the following correct version:: let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) -Secondly, some |Coq| definitions may have no counterpart in ML. This +Secondly, some Coq definitions may have no counterpart in ML. This happens when there is a quantification over types inside the type of a constructor; for example: @@ -515,29 +515,29 @@ of a constructor; for example: Inductive anything : Type := dummy : forall A:Set, A -> anything. which corresponds to the definition of an ML dynamic type. -In |OCaml|, we must cast any argument of the constructor dummy +In OCaml, we must cast any argument of the constructor dummy (no GADT are produced yet by the extraction). 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 inductive types will always +ill-typed to the OCaml type checker, it can't go wrong : it comes +from a Coq well-typed terms, so for example inductive types will always have the correct number of arguments, etc. Of course, when launching manually some extracted function, you should apply it to arguments -of the right shape (from the |Coq| point-of-view). +of the right shape (from the Coq point-of-view). More details about the correctness of the extracted programs can be found in :cite:`Let02`. We have to say, though, that in most "realistic" programs, these problems do not -occur. For example all the programs of |Coq| library are accepted by the |OCaml| +occur. For example all the programs of Coq library are accepted by the OCaml type checker without any ``Obj.magic`` (see examples below). Some examples ------------- We present here two examples of extraction, taken from the -|Coq| Standard Library. We choose |OCaml| as the target language, +Coq Standard Library. We choose OCaml as the target language, but everything, with slight modifications, can also be done in the other languages supported by extraction. We then indicate where to find other examples and tests of extraction. @@ -554,7 +554,7 @@ This module contains a theorem ``eucl_dev``, whose type is:: where ``diveucl`` is a type for the pair of the quotient and the modulo, plus some logical assertions that disappear during extraction. -We can now extract this program to |OCaml|: +We can now extract this program to OCaml: .. coqtop:: none @@ -570,11 +570,11 @@ We can now extract this program to |OCaml|: The inlining of ``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 ``euclid.ml`` or let -|Coq| do it for you with the following command:: +Coq do it for you with the following command:: Extraction "euclid" eucl_dev. -Let us play the resulting program (in an |OCaml| toplevel):: +Let us play the resulting program (in an OCaml toplevel):: #use "euclid.ml";; type nat = O | S of nat @@ -588,7 +588,7 @@ Let us play the resulting program (in an |OCaml| toplevel):: # eucl_dev (S (S O)) (S (S (S (S (S O)))));; - : diveucl = Divex (S (S O), S O) -It is easier to test on |OCaml| integers:: +It is easier to test on OCaml integers:: # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; val nat_of_int : int -> nat = <fun> @@ -614,12 +614,12 @@ Extraction's horror museum ~~~~~~~~~~~~~~~~~~~~~~~~~~ Some pathological examples of extraction are grouped in the file -``test-suite/success/extraction.v`` of the sources of |Coq|. +``test-suite/success/extraction.v`` of the sources of Coq. Users' Contributions ~~~~~~~~~~~~~~~~~~~~ -Several of the |Coq| Users' Contributions use extraction to produce +Several of the Coq Users' Contributions use extraction to produce certified programs. In particular the following ones have an automatic extraction test: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 407a38378f..27ae7cea3a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -35,7 +35,7 @@ the previous implementation in several ways: the new implementation, if one provides the proper morphisms. Again, most of the work is handled in the tactics. + First-class morphisms and signatures. Signatures and morphisms are - ordinary |Coq| terms, hence they can be manipulated inside |Coq|, put + ordinary Coq terms, hence they can be manipulated inside Coq, put inside structures and lemmas about them can be proved inside the system. Higher-order morphisms are also allowed. + Performance. The implementation is based on a depth-first search for @@ -103,7 +103,7 @@ argument. Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation instance :math:`R` if it is covariant on the same argument when the inverse -relation :math:`R^{−1}` (``inverse R`` in |Coq|) is considered. The special arrow ``-->`` +relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. Functions having arguments related by symmetric relations instances @@ -144,7 +144,7 @@ always the intended equality for a given structure. In the next section we will describe the commands to register terms as parametric relations and morphisms. Several tactics that deal with -equality in |Coq| can also work with the registered relations. The exact +equality in Coq can also work with the registered relations. The exact list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R`` is an instance of a registered reflexive relation. However, the diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index b81212ad0d..0f0ccd6a20 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -8,7 +8,7 @@ Implicit Coercions General Presentation --------------------- -This section describes the inheritance mechanism of |Coq|. In |Coq| with +This section describes the inheritance mechanism of Coq. In Coq with inheritance, we are not interested in adding any expressive power to our theory, but only convenience. Given a term, possibly not typable, we are interested in the problem of determining if it can be well diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 2c7b637a42..fb9965e43a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -260,7 +260,7 @@ proof by abstracting monomials by variables. that might miss a refutation. To illustrate the working of the tactic, consider we wish to prove the - following |Coq| goal: + following Coq goal: .. needs csdp .. coqdoc:: diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 3944a34cdc..7d30cae525 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,7 +1,7 @@ Program derivation ================== -|Coq| comes with an extension called ``Derive``, which supports program +Coq comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be required with ``Require Coq.derive.Derive``. When the extension is loaded, diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 5c08bc44df..2b10f5671d 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -9,7 +9,7 @@ Omega: a (deprecated) solver for arithmetic The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` tactic. The goal is to consolidate the arithmetic solving - capabilities of |Coq| into a single engine; moreover, :tacn:`lia` is + capabilities of Coq into a single engine; moreover, :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a complete Presburger arithmetic solver while :tacn:`omega` was known to be incomplete). @@ -143,7 +143,7 @@ Options .. deprecated:: 8.5 - This deprecated flag (on by default) is for compatibility with |Coq| pre 8.5. It + This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. .. flag:: Omega UseLocalDefs diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 7a50748c51..e824ae152d 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -6,8 +6,8 @@ Asynchronous and Parallel Proof Processing :Author: Enrico Tassi 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, it allows |Coq| to take +Coq. This feature improves the reactivity of the system when used in +interactive 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. @@ -20,13 +20,13 @@ This feature has some technical limitations that may make it unsuitable for some use cases. For example, in interactive mode, some errors coming from the kernel -of |Coq| are signaled late. The type of errors belonging to this +of Coq are signaled late. The type of errors belonging to this category are universe inconsistencies. At the time of writing, only opaque proofs (ending with ``Qed`` or ``Admitted``) can be processed asynchronously. -Finally, asynchronous processing is disabled when running |CoqIDE| in +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:`interactive-mode`, though doing so is not recommended. @@ -34,12 +34,12 @@ though doing so is not recommended. Proof annotations ---------------------- -To process a proof asynchronously |Coq| needs to know the precise +To process a proof asynchronously Coq needs to know the precise statement of the theorem without looking at the proof. This requires some annotations if the theorem is proved inside a Section (see Section :ref:`section-mechanism`). -When a section ends, |Coq| looks at the proof object to decide which +When a section ends, Coq looks at the proof object to decide which section variables are actually used and hence have to be quantified in the statement of the theorem. To avoid making the construction of proofs mandatory when ending a section, one can start each proof with @@ -58,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed`` +The :flag:`Suggest Proof Using` flag makes Coq suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. @@ -66,17 +66,17 @@ to modify the proof script accordingly. Proof blocks and error resilience -------------------------------------- -|Coq| 8.6 introduced a mechanism for error resilience: in interactive -mode |Coq| is able to completely check a document containing errors +Coq 8.6 introduced a mechanism for error resilience: 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 +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 +proof script (i.e. also looking at indentation). Coq comes with four kind of proof blocks, and an ML API to add new ones. :curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling` @@ -92,13 +92,13 @@ Caveats When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by the first error. Error resilience for vernacular commands can be switched off by passing ``-async-proofs-command-error-resilience off`` -to |CoqIDE|. +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 resilience can be turned off or selectively activated -for any set of block kind passing to |CoqIDE| one of the following +for any set of block kind passing to CoqIDE one of the following options: - ``-async-proofs-tactic-error-resilience off`` @@ -113,13 +113,13 @@ Interactive mode --------------------- At the time of writing the only user interface supporting asynchronous -proof processing is |CoqIDE|. +proof processing is CoqIDE. -When |CoqIDE| is started, two |Coq| processes are created. The master one +When CoqIDE is started, two Coq processes are created. The master one follows the user, giving feedback as soon as possible by skipping proofs, which are delegated to the worker process. The worker process, whose state can be seen by clicking on the button in the lower right -corner of the main |CoqIDE| window, asynchronously processes the proofs. +corner of the main CoqIDE window, asynchronously processes the proofs. If a proof contains an error, it is reported in red in the label of the very same button, that can also be used to see the list of errors and jump to the corresponding line. @@ -137,14 +137,14 @@ Only then all the universe constraints are checked. Caveats ``````` -The number of worker processes can be increased by passing |CoqIDE| +The number of worker processes can be increased by passing CoqIDE the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, since each worker requires the same amount of memory as 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 ``-async-proofs off`` flag to -|CoqIDE|. Conversely, on Windows, where the feature is disabled by +CoqIDE. Conversely, on Windows, where the feature is disabled by default, pass the ``-async-proofs on`` flag to enable it. Proofs that are known to take little time to process are not delegated @@ -166,9 +166,9 @@ Batch mode a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is assigned higher priority than the loading of a ``.vio`` file. -When |Coq| is used as a batch compiler by running ``coqc``, it produces +When Coq is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other -things, theorem statements and proofs. Hence to produce a .vo |Coq| +things, theorem statements and proofs. Hence to produce a .vo Coq need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a @@ -224,7 +224,7 @@ heavy use of the ``Type`` hierarchy. Limiting the number of parallel workers -------------------------------------------- -Many |Coq| processes may run on the same computer, and each of them may +Many Coq processes may run on the same computer, and each of them may start many additional worker processes. The ``coqworkmgr`` utility lets one limit the number of workers, globally. @@ -232,9 +232,9 @@ The utility accepts the ``-j`` argument to specify the maximum number of workers (defaults to 2). ``coqworkmgr`` automatically starts in the background and prints an environment variable assignment like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable -in all the shells from which |Coq| processes will be started. If one +in all the shells from which Coq processes will be started. If one uses just one terminal running the bash shell, then ``export ‘coqworkmgr -j 4‘`` will do the job. -After that, all |Coq| processes, e.g. ``coqide`` and ``coqc``, will respect the +After that, all Coq processes, e.g. ``coqide`` and ``coqc``, will respect the limit, globally. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 5da1ac3f46..298ea4b4ab 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -8,25 +8,25 @@ Program :Author: Matthieu Sozeau We present here the |Program| tactic commands, used to build -certified |Coq| programs, elaborating them from their algorithmic +certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification :cite:`sozeau06`. It can be thought of as a dual of :ref:`Extraction <extraction>`. The goal of |Program| is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the -specification using the whole |Coq| proof apparatus. This is done using +specification using the whole Coq proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of PVS :cite:`Rushby98`, which generates type checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a -complete |Coq| term. |Program| replaces the |Program| tactic by Catherine +complete Coq term. |Program| replaces the |Program| tactic by Catherine Parent :cite:`Parent95b` which had a similar goal but is no longer maintained. -The languages available as input are currently restricted to |Coq|’s -term language, but may be extended to |OCaml|, Haskell and -others in the future. We use the same syntax as |Coq| and permit to use +The languages available as input are currently restricted to Coq’s +term language, but may be extended to OCaml, Haskell and +others in the future. We use the same syntax as Coq and permit to use implicit arguments and the existing coercion mechanism. Input terms and types are typed in an extended system (Russell) and interpreted -into |Coq| terms. The interpretation process may produce some proof +into Coq terms. The interpretation process may produce some proof obligations which need to be resolved to create the final term. @@ -35,7 +35,7 @@ obligations which need to be resolved to create the final term. Elaborating programs -------------------- -The main difference from |Coq| is that an object in a type :g:`T : Set` can +The main difference from Coq is that an object in a type :g:`T : Set` can be considered as an object of type :g:`{x : T | P}` for any well-formed :g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property :g:`P`, we must prove that the object under consideration verifies it. Russell @@ -86,7 +86,7 @@ coercions. Controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm - of |Coq| (see :ref:`extendedpatternmatching`) when this flag is + of Coq (see :ref:`extendedpatternmatching`) when this flag is deactivated. .. flag:: Program Generalized Coercion @@ -116,7 +116,7 @@ Syntactic control over equalities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To give more control over the generation of equalities, the -type checker will fall back directly to |Coq|’s usual typing of dependent +type checker will fall back directly to Coq’s usual typing of dependent pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can @@ -161,13 +161,13 @@ Program Definition A :cmd:`Definition` command with the :attr:`program` attribute types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the -final |Coq| term to the name :n:`@ident` in the environment. +final Coq term to the name :n:`@ident` in the environment. :n:`Program Definition @ident : @type := @term` Interprets the type :n:`@type`, potentially generating proof -obligations to be resolved. Once done with them, we have a |Coq| -type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq| +obligations to be resolved. Once done with them, we have a Coq +type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a Coq term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the set of obligations generated during the interpretation of :n:`@term__0` @@ -342,7 +342,7 @@ Frequently Asked Questions .. exn:: Ill-formed recursive definition. This error can happen when one tries to define a function by structural - recursion on a subset object, which means the |Coq| function looks like: + recursion on a subset object, which means the Coq function looks like: :: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index abfffa0035..d46dea1f5d 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -99,7 +99,7 @@ Yes, building the variables map and doing the substitution after normalizing is automatically done by the tactic. So you can just forget this paragraph and use the tactic according to your intuition. -Concrete usage in |Coq| +Concrete usage in Coq -------------------------- .. tacn:: ring {? [ {+ @one_term } ] } @@ -429,10 +429,10 @@ How does it work? The code of ``ring`` is a good example of a tactic written using *reflection*. What is reflection? Basically, using it means that a part of a tactic is written -in Gallina, |Coq|'s language of terms, rather than |Ltac| or |OCaml|. From the +in Gallina, Coq's language of terms, rather than |Ltac| or OCaml. From the philosophical point of view, reflection is using the ability of the Calculus of Constructions to speak and reason about itself. For the ``ring`` tactic we used -|Coq| as a programming language and also as a proof environment to build a tactic +Coq as a programming language and also as a proof environment to build a tactic and to prove its correctness. The interested reader is strongly advised to have a look at the @@ -491,7 +491,7 @@ its correctness w.r.t interpretation, that is: So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little -piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an +piece of ML code guesses the type of `p`, the ring theory `T` to use, an abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`, using the main correctness theorem and we reduce it to a @@ -677,7 +677,7 @@ History of ring First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big -for |Coq|’s type checker. Let us see why: +for Coq’s type checker. Let us see why: .. coqtop:: all @@ -697,7 +697,7 @@ was rewritten by Patrick Loiseleur: the new tactic does not any more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote -some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. +some ML code for the ``Add Ring`` command that allows registering new rings dynamically. Proofs terms generated by ring are quite small, they are linear in the number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking @@ -740,12 +740,12 @@ tactics using reflection. Another idea suggested by Benjamin Werner: reflection could be used to couple an external tool (a rewriting program or a model checker) -with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and +with Coq. We define (in Coq) a type of terms, a type of *traces*, and prove a correctness theorem that states that *replaying traces* is safe with respect to some interpretation. Then we let the external tool do every computation (using side-effects, backtracking, exception, or others features that are not available in pure lambda calculus) to produce -the trace. Now we can check in |Coq| that the trace has the expected +the trace. Now we can check in Coq that the trace has the expected semantics by applying the correctness theorem. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 6c62ff3116..2b1f343e14 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -10,13 +10,13 @@ SProp (proof irrelevant propositions) In particular, conversion checking through bytecode or native code compilation currently does not understand proof irrelevance. -This section describes the extension of |Coq| with definitionally +This section describes the extension of Coq with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also known as strict propositions) as described in :cite:`Gilbert:POPL2019`. Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the -|Coq| program or by turning the :flag:`Allow StrictProp` flag off. +Coq program or by turning the :flag:`Allow StrictProp` flag off. .. flag:: Allow StrictProp :name: Allow StrictProp diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7638fce010..cdd31fcb86 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -13,7 +13,7 @@ Class and Instance declarations ------------------------------- The syntax for class and instance declarations is the same as the record -syntax of |Coq|: +syntax of Coq: .. coqdoc:: @@ -61,7 +61,7 @@ Note that if you finish the proof with :cmd:`Qed` the entire instance will be opaque, including the fields given in the initial term. Alternatively, in :flag:`Program Mode` if one does not give all the -members in the Instance declaration, |Coq| generates obligations for the +members in the Instance declaration, Coq generates obligations for the remaining fields, e.g.: .. coqtop:: in @@ -242,7 +242,7 @@ binders. For example: Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). The ``!`` modifier switches the way a binder is parsed back to the usual -interpretation of |Coq|. In particular, it uses the implicit arguments +interpretation of Coq. In particular, it uses the implicit arguments mechanism if available, as shown in the example. Substructures @@ -513,7 +513,7 @@ Settings This flag (off by default) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before - the dependent ones previously (|Coq| 8.5 and below). This can result in + the dependent ones previously (Coq 8.5 and below). This can result in quite different performance behaviors of proof search. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index dd26534ec7..1fb337b30a 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -12,7 +12,7 @@ General Presentation The status of Universe Polymorphism is experimental. -This section describes the universe polymorphic extension of |Coq|. +This section describes the universe polymorphic extension of Coq. Universe polymorphism makes it possible to write generic definitions making use of universes and reuse them at different and sometimes incompatible universe levels. @@ -231,7 +231,7 @@ constraints by prefixing the level names with symbols. Because inductive subtypings are only produced by comparing inductives to themselves with universes changed, they amount to variance information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in |Coq|), +irrelevant (there are no contravariant subtypings in Coq), respectively represented by the symbols `=`, `+` and `*`. Here we see that :g:`list` binds an irrelevant universe, so any two @@ -474,7 +474,7 @@ mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one can use :cmd:`Show Universes` to display the current context of universes. -It is possible to provide only some universe levels and let |Coq| infer the others +It is possible to provide only some universe levels and let Coq infer the others by adding a :g:`+` in the list of bound universe levels: .. coqtop:: all |