diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 139 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 88 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 156 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 69 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 53 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 383 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 445 |
13 files changed, 921 insertions, 495 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 64d4eddf04..c4f0147728 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -46,7 +46,7 @@ the expressiveness of the theory remains the same. Once the stage of parsing has finished only simple patterns remain. Re-nesting of pattern is performed at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing -(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print` +(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print` if the term is a constant, or using the command :cmd:`Check`. The extended ``match`` still accepts an optional *elimination predicate* @@ -75,7 +75,7 @@ by: Multiple patterns ----------------- -Using multiple patterns in the definition of max lets us write: +Using multiple patterns in the definition of ``max`` lets us write: .. coqtop:: in undo @@ -273,7 +273,7 @@ This option (off by default) removes parameters from constructors in patterns: match l with | nil => nil | cons _ l' => l' - end) + end). Unset Asymmetric Patterns. Implicit arguments in patterns @@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11). end). +.. _matching-dependent: + Matching objects of dependent types ----------------------------------- @@ -414,6 +416,7 @@ length, by writing I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. +.. _match-in-patterns: Patterns in ``in`` ~~~~~~~~~~~~~~~~~~ @@ -427,7 +430,7 @@ become impossible branches. In an impossible branch, you can answer anything but False_rect unit has the advantage to be subterm of anything. -To be concrete: the tail function can be written: +To be concrete: the ``tail`` function can be written: .. coqtop:: in @@ -588,24 +591,24 @@ generated expression and the original. Here is a summary of the error messages corresponding to each situation: -.. exn:: The constructor @ident expects @num arguments +.. exn:: The constructor @ident expects @num arguments. The variable ident is bound several times in pattern termFound a constructor of inductive type term while a constructor of term is expectedPatterns are incorrect (because constructors are not applied to the correct number of the arguments, because they are not linear or they are wrongly typed). -.. exn:: Non exhaustive pattern-matching +.. exn:: Non exhaustive pattern-matching. The pattern matching is not exhaustive. .. exn:: The elimination predicate term should be of arity @num (for non \ - dependent case) or @num (for dependent case) + dependent case) or @num (for dependent case). The elimination predicate provided to match has not the expected arity. .. exn:: Unable to infer a match predicate - Either there is a type incompatibility or the problem involves dependencies + Either there is a type incompatibility or the problem involves dependencies. There is a type mismatch between the different branches. The user should provide an elimination predicate. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d7f97edab1..cb93d48a41 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,16 +1,16 @@ -.. _extraction: - .. include:: ../replaces.rst -Extraction of programs in OCaml and Haskell -============================================ +.. _extraction: + +Extraction of programs in |OCaml| and Haskell +============================================= :Authors: Jean-Christophe Filliâtre and Pierre Letouzey 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 +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. @@ -37,11 +37,11 @@ Generating ML Code The next two commands are meant to be used for rapid preview of extraction. They both display extracted term(s) inside |Coq|. -.. cmd:: Extraction @qualid. +.. cmd:: Extraction @qualid Extraction of the mentioned object in the |Coq| toplevel. -.. cmd:: Recursive Extraction @qualid ... @qualid. +.. cmd:: Recursive Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies in the |Coq| toplevel. @@ -49,7 +49,7 @@ extraction. They both display extracted term(s) inside |Coq|. All the following commands produce real ML files. User can choose to produce one monolithic file or one file per |Coq| library. -.. cmd:: Extraction "@file" @qualid ... @qualid. +.. cmd:: Extraction "@file" {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies in one monolithic `file`. @@ -57,43 +57,43 @@ produce one monolithic file or one file per |Coq| library. language to fulfill its syntactic conventions, keeping original names as much as possible. -.. cmd:: Extraction Library @ident. +.. cmd:: Extraction Library @ident Extraction of the whole |Coq| library ``ident.v`` to an ML module ``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. +.. cmd:: Recursive Extraction Library @ident Extraction of the |Coq| library ``ident.v`` and all other modules ``ident.v`` depends on. -.. cmd:: Separate Extraction @qualid ... @qualid. +.. cmd:: Separate Extraction {+ @qualid } Recursive extraction of all the mentioned objects and all their dependencies, just as ``Extraction "file"``, but instead of producing one monolithic file, this command splits the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to - ``Recursive Extraction Library``, except that only the needed + :cmd:`Recursive Extraction Library`, except that only the needed parts of Coq libraries are extracted instead of the whole. The naming convention in case of name clash is the same one as - ``Extraction Library``: identifiers are here renamed using prefixes + :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. -.. cmd:: Extraction TestCompile @qualid ... @qualid. +.. 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 ------------------- @@ -102,26 +102,26 @@ Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ The ability to fix target language is the first and more important -of the extraction options. Default is ``Ocaml``. +of the extraction options. Default is ``OCaml``. -.. cmd:: Extraction Language Ocaml. -.. cmd:: Extraction Language Haskell. -.. cmd:: Extraction Language Scheme. +.. cmd:: Extraction Language OCaml +.. cmd:: Extraction Language Haskell +.. cmd:: Extraction Language Scheme 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 -want to generate OCaml programs. The optimizations can be split in two +want to generate |OCaml| programs. 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 constant are nevertheless printed, to ensure session-independent programs. @@ -131,14 +131,14 @@ order to produce more readable code. The type-preserving optimizations are controlled by the following |Coq| options: -.. opt:: Extraction Optimize. +.. opt:: Extraction Optimize 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 option off if you want a ML term as close as possible to the Coq term. -.. opt:: Extraction Conservative Types. +.. opt:: Extraction Conservative Types Default is off. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -146,7 +146,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. -.. opt:: Extraction KeepSingleton. +.. opt:: Extraction KeepSingleton Default is off. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -155,7 +155,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: The typical example is ``sig``. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -.. opt:: Extraction AutoInline. +.. opt:: Extraction AutoInline Default is on. The extraction mechanism inlines the bodies of some defined constants, according to some heuristics @@ -163,22 +163,22 @@ The type-preserving optimizations are controlled by the following |Coq| options: Those heuristics are not always perfect; if you want to disable this feature, turn this option off. -.. cmd:: Extraction Inline @qualid ... @qualid. +.. cmd:: Extraction Inline {+ @qualid } In addition to the automatic inline feature, the constants mentionned by this command will always be inlined during extraction. -.. cmd:: Extraction NoInline @qualid ... @qualid. +.. cmd:: Extraction NoInline {+ @qualid } Conversely, the constants mentionned by this command will never be inlined during extraction. -.. cmd:: Print Extraction Inline. +.. cmd:: Print Extraction Inline Prints the current state of the table recording the custom inlinings declared by the two previous commands. -.. cmd:: Reset Extraction Inline. +.. cmd:: Reset Extraction Inline Empties the table recording the custom inlinings (see the previous commands). @@ -213,7 +213,7 @@ code elimination performed during extraction, in a way which is independent but complementary to the main elimination principles of extraction (logical parts and types). -.. cmd:: Extraction Implicit @qualid [ @ident ... @ident ]. +.. cmd:: Extraction Implicit @qualid [ {+ @ident } ] This experimental command allows declaring some arguments of `qualid` as implicit, i.e. useless in extracted code and hence to @@ -223,11 +223,11 @@ principles of extraction (logical parts and types). by a number indicating its position, starting from 1. When an actual extraction takes place, an error is normally raised if the -``Extraction Implicit`` declarations cannot be honored, that is +:cmd:`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 via the following option: -.. opt:: Extraction SafeImplicits. +.. opt:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted instead of an error if some implicited variables still occur in the @@ -253,21 +253,20 @@ a closed term, and of course the system cannot guess the program which realizes an axiom. Therefore, it is possible to tell the system what ML term corresponds to a given axiom. -.. cmd:: Extract Constant @qualid => @string. +.. cmd:: Extract Constant @qualid => @string Give an ML extraction for the given constant. The `string` may be an identifier or a quoted string. -.. cmd:: Extract Inlined Constant @qualid => @string. +.. cmd:: Extract Inlined Constant @qualid => @string Same as the previous one, except that the given ML terms will be inlined everywhere instead of being declared via a ``let``. .. note:: - - This command is sugar for an ``Extract Constant`` followed - by a ``Extraction Inline``. Hence a ``Reset Extraction Inline`` - will have an effect on the realized and inlined axiom. + This command is sugar for an :cmd:`Extract Constant` followed + by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline` + will have an effect on the realized and inlined axiom. .. caution:: It is the responsibility of the user to ensure that the ML terms given to realize the axioms do have the expected types. In @@ -286,7 +285,7 @@ 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 (as quoted strings). The syntax is then: -.. cmdv:: Extract Constant @qualid @string ... @string => @string. +.. cmdv:: Extract Constant @qualid @string ... @string => @string The number of type variables is checked by the system. For example: @@ -295,7 +294,7 @@ The number of type variables is checked by the system. For example: Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a * 'b ". -Realizing an axiom via ``Extract Constant`` is only useful in the +Realizing an axiom via :cmd:`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 @@ -315,7 +314,7 @@ 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 |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ]. +.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify extractions for the type itself (first `string`) and all its @@ -323,7 +322,7 @@ native boolean type instead of |Coq| one. The syntax is the following: the ML extraction must be an ML inductive datatype, and the native pattern-matching of the language will be used. -.. cmdv:: Extract Inductive @qualid => @string [ @string ... @string ] @string. +.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra `string` that indicates how to perform pattern-matching over this inductive type. In this form, @@ -336,10 +335,10 @@ native boolean type instead of |Coq| one. The syntax is the following: argument 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 ``nat`` - into OCaml ``int``, the code to provide has type: + into |OCaml| ``int``, the code to provide has type: ``(unit->'a)->(int->'a)->int->'a``. -.. caution:: As for ``Extract Constant``, this command should be used with care: +.. caution:: As for :cmd:`Extract Constant`, this command should be used with care: * The ML code provided by the user is currently **not** checked at all by extraction, even for syntax errors. @@ -347,17 +346,17 @@ native boolean type instead of |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 ``Extract Constant`` when primitive counterparts exist. + some specific :cmd:`Extract Constant` when primitive counterparts exist. Typical examples are the following: @@ -369,9 +368,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 infix constructor or type. .. coqtop:: in @@ -380,7 +379,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 @@ -389,28 +388,28 @@ As an example of translation to a non-inductive datatype, let's turn Avoiding conflicts with existing filenames ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When using ``Extraction Library``, the names of the extracted files +When using :cmd:`Extraction Library`, the names of the extracted files directly depends from 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 ... @ident. +.. cmd:: Extraction Blacklist {+ @ident } Instruct the extraction to avoid using these names as filenames for extracted code. -.. cmd:: Print Extraction Blacklist. +.. cmd:: Print Extraction Blacklist Show the current list of filenames the extraction should avoid. -.. cmd:: Reset Extraction Blacklist. +.. cmd:: Reset Extraction Blacklist 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``. Differences between |Coq| and ML type systems @@ -418,7 +417,7 @@ 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. @@ -432,7 +431,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)) @@ -455,12 +454,12 @@ 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 +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 @@ -470,14 +469,14 @@ 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 extractions, taken from the -|Coq| Standard Library. We choose OCaml as target language, +|Coq| Standard Library. We choose |OCaml| as target language, but all can be done in the other dialects with slight modifications. We then indicate where to find other examples and tests of extraction. @@ -493,7 +492,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 @@ -513,7 +512,7 @@ You can then copy-paste the output to a file ``euclid.ml`` or let 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 @@ -527,7 +526,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> diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index da9e97e6fa..e10e16c107 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,14 +1,12 @@ -.. _generalizedrewriting: - ------------------------ - Generalized rewriting ------------------------ +.. include:: ../preamble.rst +.. include:: ../replaces.rst -:Author: Matthieu Sozeau +.. _generalizedrewriting: Generalized rewriting ===================== +:Author: Matthieu Sozeau This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are @@ -181,7 +179,7 @@ A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be declared with the following command: -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident. +.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident after having required the ``Setoid`` module with the ``Require Setoid`` command. @@ -220,15 +218,15 @@ For Leibniz equality, we may declare: [reflexivity proved by @refl_equal A] ... -Some tactics (``reflexivity``, ``symmetry``, ``transitivity``) work only on +Some tactics (:tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`) work only on relations that respect the expected properties. The remaining tactics -(``replace``, ``rewrite`` and derived tactics such as ``autorewrite``) do not +(`replace`, :tacn:`rewrite` and derived tactics such as :tacn:`autorewrite`) do not require any properties over the relation. However, they are able to replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident. +.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident The command declares ``f`` as a parametric morphism of signature ``sig``. The identifier ``id`` gives a unique name to the morphism and it is used as @@ -319,7 +317,7 @@ instance mechanism. The behavior on section close is to generalize the instances by the variables of the section (and possibly hypotheses used in the proofs of instance declarations) but not to export them in the rest of the development for proof search. One can use the -``Existing Instance`` command to do so outside the section, using the name of the +cmd:`Existing Instance` command to do so outside the section, using the name of the declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier for the corresponding class instance declaration (see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at @@ -429,7 +427,7 @@ equality over ordered lists) ``set_eq ==> set_eq ==> set_eq`` ``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq`` being the equality over unordered lists). -To declare multiple signatures for a morphism, repeat the ``Add Morphism`` +To declare multiple signatures for a morphism, repeat the :cmd:`Add Morphism` command. When morphisms have multiple signatures it can be the case that a @@ -479,7 +477,7 @@ The declaration itself amounts to the definition of an object of the record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added to the ``typeclass_instances`` hint database. Morphism declarations are also instances of a type class defined in ``Classes.Morphisms``. See the -documentation on type classes :ref:`TODO-chapter-20-type-classes` +documentation on type classes :ref:`typeclasses` and the theories files in Classes for further explanations. One can inform the rewrite tactic about morphisms and relations just @@ -532,21 +530,26 @@ Tactics enabled on user provided relations The following tactics, all prefixed by ``setoid_``, deal with arbitrary registered relations and morphisms. Moreover, all the corresponding -unprefixed tactics (i.e. ``reflexivity``, ``symmetry``, ``transitivity``, -``replace``, ``rewrite``) have been extended to fall back to their prefixed +unprefixed tactics (i.e. :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`, +:tacn:`replace`, :tacn:`rewrite`) have been extended to fall back to their prefixed counterparts when the relation involved is not Leibniz equality. Notice, however, that using the prefixed tactics it is possible to pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity + :name: setoid_reflexivity .. tacv:: setoid_symmetry [in @ident] + :name: setoid_symmetry .. tacv:: setoid_transitivity + :name: setoid_transitivity .. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident] + :name: setoid_rewrite .. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic] + :name: setoid_replace The ``using relation`` arguments cannot be passed to the unprefixed form. @@ -561,21 +564,23 @@ on a given type. Every derived tactic that is based on the unprefixed forms of the tactics considered above will also work up to user defined relations. -For instance, it is possible to register hints for ``autorewrite`` that +For instance, it is possible to register hints for :tacn:`autorewrite` that are not proof of Leibniz equalities. In particular it is possible to -exploit ``autorewrite`` to simulate normalization in a term rewriting +exploit :tacn:`autorewrite` to simulate normalization in a term rewriting system up to user defined equalities. Printing relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The ``Print Instances`` command can be used to show the list of currently +.. cmd:: Print Instances + +This command can be used to show the list of currently registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric`` or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms (implemented as ``Proper`` instances). When the rewriting tactics refuse to replace a term in a context because the latter is not a composition -of morphisms, the ``Print Instances`` commands can be useful to understand +of morphisms, the :cmd:`Print Instances` command can be useful to understand what additional morphisms should be registered. @@ -585,7 +590,7 @@ Deprecated syntax and backward incompatibilities Due to backward compatibility reasons, the following syntax for the declaration of setoids and morphisms is also accepted. -.. tacv:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @A @Aeq @ST as @ident where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record @@ -593,7 +598,8 @@ packing together the reflexivity, symmetry and transitivity lemmas). Notice that the syntax is not completely backward compatible since the identifier was not required. -.. cmd:: Add Morphism f : @ident. +.. cmd:: Add Morphism f : @ident + :name: Add Morphism The latter command also is restricted to the declaration of morphisms without parameters. It is not fully backward compatible since the @@ -607,11 +613,11 @@ Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. Moreover, it is now also possible to declare several morphisms having -the same signature. Finally, the replace and rewrite tactics can be +the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can be used to replace terms in contexts that were refused by the old implementation. As discussed in the next section, the semantics of the -new ``setoid_rewrite`` command differs slightly from the old one and -``rewrite``. +new :tacn:`setoid_rewrite` tactic differs slightly from the old one and +:tacn:`rewrite`. Extensions @@ -621,8 +627,9 @@ Extensions Rewriting under binders ~~~~~~~~~~~~~~~~~~~~~~~ -warning:: Due to compatibility issues, this feature is enabled only -when calling the ``setoid_rewrite`` tactics directly and not ``rewrite``. +.. warning:: + Due to compatibility issues, this feature is enabled only + when calling the :tacn:`setoid_rewrite` tactic directly and not :tacn:`rewrite`. To be able to rewrite under binding constructs, one must declare morphisms with respect to pointwise (setoid) equivalence of functions. @@ -669,12 +676,12 @@ where ``list_equiv`` implements an equivalence on lists parameterized by an equivalence on the elements. Note that when one does rewriting with a lemma under a binder using -``setoid_rewrite``, the application of the lemma may capture the bound +:tacn:`setoid_rewrite`, the application of the lemma may capture the bound variable, as the semantics are different from rewrite where the lemma -is first matched on the whole term. With the new ``setoid_rewrite``, +is first matched on the whole term. With the new :tacn:`setoid_rewrite`, matching is done on each subterm separately and in its local environment, and all matches are rewritten *simultaneously* by -default. The semantics of the previous ``setoid_rewrite`` implementation +default. The semantics of the previous :tacn:`setoid_rewrite` implementation can almost be recovered using the ``at 1`` modifier. @@ -707,22 +714,20 @@ defined constants as transparent by default. This may slow down the resolution due to a lot of unifications (all the declared ``Proper`` instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command -``Typeclasses Opaque`` (see :ref:`TODO-20.6.7-typeclasses-transparency`). - +:cmd:`Typeclasses Opaque`. Strategies for rewriting ------------------------ - Definitions ~~~~~~~~~~~ -The generalized rewriting tactic is based on a set of strategies that -can be combined to obtain custom rewriting procedures. Its set of -strategies is based on Elan’s rewriting strategies :ref:`TODO-102-biblio`. Rewriting +The generalized rewriting tactic is based on a set of strategies that can be +combined to obtain custom rewriting procedures. Its set of strategies is based +on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a -strategy expression. Strategies are defined inductively as described -by the following grammar: +strategy expression. Strategies are defined inductively as described by the +following grammar: .. productionlist:: rewriting s, t, u : `strategy` @@ -808,11 +813,11 @@ strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. -Hint databases created for ``autorewrite`` can also be used -by ``rewrite_strat`` using the ``hints`` strategy that applies any of the +Hint databases created for :tacn:`autorewrite` can also be used +by :tacn:`rewrite_strat` using the ``hints`` strategy that applies any of the lemmas at the current subterm. The ``terms`` strategy takes the lemma names directly as arguments. The ``eval`` strategy expects a reduction -expression (see :ref:`TODO-8.7-performing-computations`) and succeeds +expression (see :ref:`performingcomputations`) and succeeds if it reduces the subterm under consideration. The ``fold`` strategy takes a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` on success, it is stronger than the tactic ``fold``. @@ -822,7 +827,8 @@ Usage ~~~~~ -.. tacv:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s [in @ident] + :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index f5ca5be44a..09faa06765 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,7 +1,7 @@ -.. _implicitcoercions: - .. include:: ../replaces.rst +.. _implicitcoercions: + Implicit Coercions ==================== @@ -65,7 +65,7 @@ conditions holds: We then write :g:`f : C >-> D`. The restriction on the type of coercions is called *the uniform inheritance condition*. -.. note:: The abstract classe ``Sortclass`` can be used as a source class, but +.. note:: The abstract class ``Sortclass`` can be used as a source class, but the abstract class ``Funclass`` cannot. To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to @@ -124,49 +124,49 @@ term consists of the successive application of its coercions. Declaration of Coercions ------------------------- -.. cmd:: Coercion @qualid : @class >-> @class. +.. cmd:: Coercion @qualid : @class >-> @class Declares the construction denoted by `qualid` as a coercion between the two given classes. - .. exn:: @qualid not declared - .. exn:: @qualid is already a coercion - .. exn:: Funclass cannot be a source class - .. exn:: @qualid is not a function - .. exn:: Cannot find the source class of @qualid - .. exn:: Cannot recognize @class as a source class of @qualid - .. exn:: @qualid does not respect the uniform inheritance condition + .. exn:: @qualid not declared. + .. exn:: @qualid is already a coercion. + .. exn:: Funclass cannot be a source class. + .. exn:: @qualid is not a function. + .. exn:: Cannot find the source class of @qualid. + .. exn:: Cannot recognize @class as a source class of @qualid. + .. exn:: @qualid does not respect the uniform inheritance condition. .. exn:: Found target class ... instead of ... - .. warn:: Ambigous path: + .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. - .. cmdv:: Local Coercion @qualid : @class >-> @class. + .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. - .. cmdv:: Coercion @ident := @term. + .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. - .. cmdv:: Coercion @ident := @term : @type. + .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. - .. cmdv:: Local Coercion @ident := @term. + .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from -Figure :ref:`TODO-1.3-sentences-syntax` as follows: +Figure :ref:`vernacular` as follows: .. FIXME: @@ -186,7 +186,7 @@ assumptions are declared as coercions. Similarly, constructors of inductive types can be declared as coercions at definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follows: +grammar of inductive types from Figure :ref:`vernacular` as follows: .. FIXME: @@ -202,7 +202,7 @@ grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follo Especially, if the extra ``>`` is present in a constructor declaration, this constructor is declared as a coercion. -.. cmd:: Identity Coercion @ident : @class >-> @class. +.. cmd:: Identity Coercion @ident : @class >-> @class If ``C`` is the source `class` and ``D`` the destination, we check that ``C`` is a constant with a body of the form @@ -211,13 +211,14 @@ declaration, this constructor is declared as a coercion. function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, and we declare it as an identity coercion between ``C`` and ``D``. - .. exn:: @class must be a transparent constant + .. exn:: @class must be a transparent constant. - .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident. + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident Idem but locally to the current section. - .. cmdv:: SubClass @ident := @type. + .. cmdv:: SubClass @ident := @type + :name: SubClass If `type` is a class `ident'` applied to some arguments then `ident` is defined and an identity coercion of name @@ -228,7 +229,7 @@ declaration, this constructor is declared as a coercion. ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`. - .. cmdv:: Local SubClass @ident := @type. + .. cmdv:: Local SubClass @ident := @type Same as before but locally to the current section. @@ -236,67 +237,67 @@ declaration, this constructor is declared as a coercion. Displaying Available Coercions ------------------------------- -.. cmd:: Print Classes. +.. cmd:: Print Classes Print the list of declared classes in the current context. -.. cmd:: Print Coercions. +.. cmd:: Print Coercions Print the list of declared coercions in the current context. -.. cmd:: Print Graph. +.. cmd:: Print Graph Print the list of valid coercion paths in the current context. -.. cmd:: Print Coercion Paths @class @class. +.. cmd:: Print Coercion Paths @class @class Print the list of valid coercion paths between the two given classes. Activating the Printing of Coercions ------------------------------------- -.. cmd:: Set Printing Coercions. +.. opt:: Printing Coercions + + When on, this option forces all the coercions to be printed. + By default, coercions are not printed. + +.. cmd:: Add Printing Coercion @qualid - This command forces all the coercions to be printed. - Conversely, to skip the printing of coercions, use - ``Unset Printing Coercions``. By default, coercions are not printed. + This command forces coercion denoted by :n:`@qualid` to be printed. + By default, a coercion is never printed. -.. cmd:: Add Printing Coercion @qualid. +.. cmd:: Remove Printing Coercion @qualid - This command forces coercion denoted by `qualid` to be printed. - To skip the printing of coercion `qualid`, use - ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + Use this command, to skip the printing of coercion :n:`@qualid`. +.. _coercions-classes-as-records: Classes as Records ------------------ -We allow the definition of *Structures with Inheritance* (or -classes as records) by extending the existing ``Record`` macro -(see Section :ref:`TODO-2.1-Record`). Its new syntax is: +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: -.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` - are their respective types. If ``:>`` is used instead of ``:`` in - the declaration of a field, then the name of this field is automatically - declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform - inheritance condition. If the optional ``>`` is given before the - record name, then the constructor name is automatically declared as - a coercion from the class of the last field type to the record name - (this may fail if the uniform inheritance condition is not - satisfied). + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `term` + are their respective types. If ``:>`` is used instead of ``:`` in + the declaration of a field, then the name of this field is automatically + declared as a coercion from the record name to the class of this + field type. Remark that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). -.. note:: +.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } + :name: Structure - The keyword ``Structure`` is a synonym of ``Record``. - -.. - FIXME: \comindex{Structure} + This is a synonym of :cmd:`Record`. Coercions and Sections @@ -312,20 +313,17 @@ coercions which do not verify the uniform inheritance condition any longer are also forgotten. Coercions and Modules ---------------------= - -From |Coq| version 8.3, the coercions present in a module are activated -only when the module is explicitly imported. Formerly, the coercions -were activated as soon as the module was required, whatever it was -imported or not. - -To recover the behavior of the versions of |Coq| prior to 8.3, use the -following command: +--------------------- -.. cmd:: Set Automatic Coercions Import. +.. opt:: Automatic Coercions Import -To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + Since |Coq| version 8.3, the coercions present in a module are activated + only when the module is explicitly imported. Formerly, the coercions + were activated as soon as the module was required, whatever it was + imported or not. + This option makes it possible to recover the behavior of the versions of + |Coq| prior to 8.3. Examples -------- diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e850587c8a..0e9c23b9bb 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -13,20 +13,19 @@ tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}` It also possible to get the tactics for integers by a ``Require Import Lia``, rationals ``Require Import Lqa`` and reals ``Require Import Lra``. -+ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`); -+ ``nia`` is an incomplete proof procedure for integer non-linear - arithmetic (see Section :ref:`nia <nia>`); -+ ``lra`` is a decision procedure for linear (real or rational) arithmetic - (see Section :ref:`lra <lra>`); -+ ``nra`` is an incomplete proof procedure for non-linear (real or - rational) arithmetic (see Section :ref:`nra <nra>`); -+ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ++ :tacn:`lia` is a decision procedure for linear integer arithmetic; ++ :tacn:`nia` is an incomplete proof procedure for integer non-linear + arithmetic; ++ :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic; ++ :tacn:`nra` is an incomplete proof procedure for non-linear (real or + rational) arithmetic; ++ :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ``n`` is an optional integer limiting the proof search depth is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light driver to the external prover `csdp` [#]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts - even without `csdp` (see Section :ref:`psatz <psatz>`). + even without `csdp`. The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. @@ -91,12 +90,13 @@ For each conjunct :math:`C_i`, the tactic calls a oracle which searches for expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. -.. _lra: - `lra`: a decision procedure for linear real and rational arithmetic ------------------------------------------------------------------- -The `lra` tactic is searching for *linear* refutations using Fourier +.. tacn:: lra + :name: lra + +This tactic is searching for *linear* refutations using Fourier elimination [#]_. As a result, this tactic explores a subset of the *Cone* defined as @@ -107,16 +107,17 @@ The deductive power of `lra` is the combined deductive power of tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. -.. _lia: - `lia`: a tactic for linear integer arithmetic --------------------------------------------- -The tactic lia offers an alternative to the omega and romega tactic -(see :ref:`omega`). Roughly speaking, the deductive power of lia is -the combined deductive power of `ring_simplify` and `omega`. However, it -solves linear goals that `omega` and `romega` do not solve, such as the -following so-called *omega nightmare* :cite:`TheOmegaPaper`. +.. tacn:: lia + :name: lia + +This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` +tactics. Roughly speaking, the deductive power of lia is the combined deductive +power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear +goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following +so-called *omega nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +125,8 @@ following so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of `lia` *vs* `omega` and `romega` -is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and +:tacn:`romega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -149,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce @@ -182,12 +184,13 @@ Our current oracle tries to find an expression :math:`e` with a small range with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for a proof. -.. _nra: - `nra`: a proof procedure for non-linear arithmetic -------------------------------------------------- -The `nra` tactic is an *experimental* proof procedure for non-linear +.. tacn:: nra + :name: nra + +This tactic is an *experimental* proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear reasoning before running the linear prover of `lra`. This pre-processing does the following: @@ -202,21 +205,23 @@ does the following: After this pre-processing, the linear prover of `lra` searches for a proof by abstracting monomials by variables. -.. _nia: - `nia`: a proof procedure for non-linear integer arithmetic ---------------------------------------------------------- -The `nia` tactic is a proof procedure for non-linear integer arithmetic. +.. tacn:: nia + :name: nia + +This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to `nra`. The obtained goal is solved using the linear integer prover `lia`. -.. _psatz: - `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- -The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the +.. tacn:: psatz + :name: psatz + +This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the depth parameter :math:`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 diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b0343a8f01..b6c35d8fa7 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -3,23 +3,15 @@ .. _miscellaneousextensions: Miscellaneous extensions -======================= - -:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html -:Converted by: Paul Steckler - -.. contents:: - :local: - :depth: 1 ----- +======================== Program derivation ------------------ +------------------ |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, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident @@ -28,7 +20,7 @@ The first `ident` can appear in `term`. This command opens a new proof presenting the user with a goal for term in which the name `ident` is bound to an existential variable `?x` (formally, there are other goals standing for the existential variables but they are shelved, as -described in Section :ref:`TODO-8.17.4`). +described in :tacn:`shelve`). When the proof ends two constants are defined: diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ef9b3505d4..387d614956 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -19,7 +19,7 @@ where :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is domain, i.e. a commutative ring with no zero divisor. For example, :math:`A` can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. Note that the equality :math:`=` used in these goals can be -any setoid equality (see :ref:`TODO-27.2.2`) , not only Leibnitz equality. +any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality. It also proves formulas diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 20e40c5507..80ce016200 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -12,24 +12,29 @@ This tactic does not need any parameter: .. tacn:: omega -``omega`` solves a goal in Presburger arithmetic, i.e. a universally +:tacn:`omega` solves a goal in Presburger arithmetic, i.e. a universally quantified formula made of equations and inequations. Equations may be specified either on the type ``nat`` of natural numbers or on the type ``Z`` of binary-encoded integer numbers. Formulas on ``nat`` are automatically injected into ``Z``. The procedure may use any hypothesis of the current proof session to solve the goal. -Multiplication is handled by ``omega`` but only goals where at +Multiplication is handled by :tacn:`omega` but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meant by "Presburger arithmetic". If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. +.. tacv:: romega + :name: romega + + To be documented. + Arithmetical goals recognized by ``omega`` ------------------------------------------ -``omega`` applied only to quantifier-free formulas built from the +:tacn:`omega` applied only to quantifier-free formulas built from the connectors:: /\ \/ ~ -> @@ -38,11 +43,11 @@ on atomic formulas. Atomic formulas are built from the predicates:: = < <= > >= -on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes:: +on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: + - * S O pred -and in expressions of type ``Z``, ``omega`` recognizes numeral constants and:: +and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: + - * Z.succ Z.pred @@ -53,32 +58,32 @@ were arbitrary variables of type ``nat`` or ``Z``. Messages from ``omega`` ----------------------- -When ``omega`` does not solve the goal, one of the following errors +When :tacn:`omega` does not solve the goal, one of the following errors is generated: -.. exn:: omega can't solve this system +.. exn:: omega can't solve this system. This may happen if your goal is not quantifier-free (if it is - universally quantified, try ``intros`` first; if it contains - existentials quantifiers too, ``omega`` is not strong enough to solve your + universally quantified, try :tacn:`intros` first; if it contains + existentials quantifiers too, :tacn:`omega` is not strong enough to solve your goal). This may happen also if your goal contains arithmetical - operators unknown from ``omega``. Finally, your goal may be really + operators unknown from :tacn:`omega`. Finally, your goal may be really wrong! -.. exn:: omega: Not a quantifier-free goal +.. exn:: omega: Not a quantifier-free goal. If your goal is universally quantified, you should first apply - ``intro`` as many time as needed. + :tacn:`intro` as many times as needed. -.. exn:: omega: Unrecognized predicate or connective: @ident +.. exn:: omega: Unrecognized predicate or connective: @ident. .. exn:: omega: Unrecognized atomic proposition: ... -.. exn:: omega: Can't solve a goal with proposition variables +.. exn:: omega: Can't solve a goal with proposition variables. -.. exn:: omega: Unrecognized proposition +.. exn:: omega: Unrecognized proposition. -.. exn:: omega: Can't solve a goal with non-linear products +.. exn:: omega: Can't solve a goal with non-linear products. .. exn:: omega: Can't solve a goal with equality on type ... @@ -115,21 +120,23 @@ Options .. opt:: Stable Omega -This deprecated option (on by default) is for compatibility with Coq pre 8.5. It -resets internal name counters to make executions of ``omega`` independent. + .. deprecated:: 8.5 + + This deprecated option (on by default) is for compatibility with Coq pre 8.5. It + resets internal name counters to make executions of :tacn:`omega` independent. .. opt:: Omega UseLocalDefs -This option (on by default) allows ``omega`` to use the bodies of local -variables. + This option (on by default) allows :tacn:`omega` to use the bodies of local + variables. .. opt:: Omega System -This option (off by default) activate the printing of debug information + This option (off by default) activate the printing of debug information .. opt:: Omega Action -This option (off by default) activate the printing of debug information + This option (off by default) activate the printing of debug information Technical data -------------- @@ -149,7 +156,7 @@ Overview of the tactic Overview of the OMEGA decision procedure ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The OMEGA decision procedure involved in the ``omega`` tactic uses +The OMEGA decision procedure involved in the :tacn:`omega` tactic uses a small subset of the decision procedure presented in :cite:`TheOmegaPaper` Here is an overview, look at the original paper for more information. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8c1b9d152b..edb8676a5b 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -39,14 +39,14 @@ Proof annotations 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:`TODO-2.4`). +Section :ref:`section-mechanism`). 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 -the ``Proof using`` command (Section :ref:`TODO-7.1.5`) that declares which section -variables the theorem uses. +the ``Proof using`` command (Section :ref:`proof-editing-mode`) that +declares which section variables the theorem uses. The presence of ``Proof`` using is needed to process proofs asynchronously in interactive mode. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index eb50e52dc7..b685e68e43 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,7 +135,7 @@ support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts -Definition (see Section `TODO-1.3.2-Definition`_) and Fixpoint (see Section `TODO-1.3.4-Fixpoint`_) +:cmd:`Definition` and :cmd:`Fixpoint` in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -145,13 +145,14 @@ prove some goals to construct the final definitions. Program Definition ~~~~~~~~~~~~~~~~~~ -.. cmd:: Program Definition @ident := @term. +.. cmd:: Program Definition @ident := @term This command 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 ``ident`` in the environment. - .. exn:: ident already exists + .. exn:: @ident already exists. + :name: @ident already exists. (Program Definition) .. cmdv:: Program Definition @ident : @type := @term @@ -166,7 +167,7 @@ Program Definition .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... - .. cmdv:: Program Definition @ident @binders : @type := @term. + .. cmdv:: Program Definition @ident @binders : @type := @term This is equivalent to: @@ -174,14 +175,14 @@ Program Definition .. TODO refer to production in alias -See also: Sections `TODO-6.10.1-Opaque`_, `TODO-6.10.2-Transparent`_, `TODO-8.7.5-unfold`_ +See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term. +.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term The optional order annotation follows the grammar: @@ -196,7 +197,7 @@ The optional order annotation follows the grammar: + :g:`wf R x` which is equivalent to :g:`measure x (R)`. The structural fixpoint operator behaves just like the one of |Coq| (see -Section `TODO-1.3.4-Fixpoint`_), except it may also generate obligations. It works +:cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. .. coqtop:: reset none @@ -254,7 +255,7 @@ using the syntax: Program Lemma ~~~~~~~~~~~~~ -.. cmd:: Program Lemma @ident : @type. +.. cmd:: Program Lemma @ident : @type The Russell language can also be used to type statements of logical properties. It will generate obligations, try to solve them @@ -276,6 +277,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: {? Local|Global} Obligation Tactic := @tactic + :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, @@ -348,7 +350,7 @@ Frequently Asked Questions --------------------------- -.. exn:: Ill-formed recursive definition +.. 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: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index b861892cbb..47d3a7d7cd 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -171,21 +171,21 @@ performs the simplification in the hypothesis named :n:`@ident`. Error messages: -.. exn:: not a valid ring equation +.. exn:: Not a valid ring equation. The conclusion of the goal is not provable in the corresponding ring theory. -.. exn:: arguments of ring_simplify do not have all the same type +.. exn:: Arguments of ring_simplify do not have all the same type. ``ring_simplify`` cannot simplify terms of several rings at the same time. Invoke the tactic once per ring structure. -.. exn:: cannot find a declared ring structure over @term +.. exn:: Cannot find a declared ring structure over @term. No ring has been declared for the type of the terms to be simplified. Use ``Add Ring`` first. -.. exn:: cannot find a declared ring structure for equality @term +.. exn:: Cannot find a declared ring structure for equality @term. Same as above is the case of the ``ring`` tactic. @@ -303,7 +303,7 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}. +.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} The :n:`@ident` is not relevant. It is just used for error messages. The :n:`@term` is a proof that the ring signature satisfies the (semi-)ring @@ -396,18 +396,18 @@ div :n:`@term` Error messages: -.. exn:: bad ring structure +.. exn:: Bad ring structure. The proof of the ring structure provided is not of the expected type. -.. exn:: bad lemma for decidability of equality +.. exn:: Bad lemma for decidability of equality. The equality function provided in the case of a computational ring has not the expected type. -.. exn:: ring operation should be declared as a morphism +.. exn:: Ring operation should be declared as a morphism. A setoid associated to the carrier of the ring structure has been found, but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. @@ -656,7 +656,7 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}. +.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} The :n:`@ident` is not relevant. It is just used for error messages. :n:`@term` is a proof that the field signature satisfies the @@ -701,7 +701,7 @@ for |Coq|’s type-checker. Let us see why: At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote -it using reflection (see his article in TACS’97 [Bou97]_). Later, it +it using reflection (see :cite:`Bou97`). Later, it 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 diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index becebb421b..6c7258f9c5 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -5,9 +5,6 @@ Type Classes ============ -:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html -:Author: Matthieu Sozeau - 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 @@ -71,8 +68,8 @@ the remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the ``Instance`` proof. One can use -alternatively the ``Program Instance`` variant which has richer facilities +determined by the transparency of the :cmd:`Instance` proof. One can use +alternatively the :cmd:`Program Instance` variant which has richer facilities for dealing with obligations. @@ -151,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, we provide a new +way to introduce variables into section contexts, compatible with the implicit +argument mechanism. The new command works similarly to the :cmd:`Variables` +vernacular, except it accepts any binding context as argument. For example: .. coqtop:: all @@ -273,12 +269,9 @@ the Existing Instance command to achieve the same effect. Summary of the commands ----------------------- +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } -.. _Class: - -.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }. - - The ``Class`` command is used to declare a type class with parameters + The :cmd:`Class` command is used to declare a type class with parameters ``binders`` and fields the declared record fields. Variants: @@ -303,12 +296,10 @@ Variants: This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined. -.. _Instance: - .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } -The ``Instance`` command is used to declare a type class instance named -``ident`` of the class ``Class`` with parameters ``t1`` to ``tn`` and +The :cmd:`Instance` command is used to declare a type class instance named +``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and fields ``b1`` to ``bi``, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode. @@ -318,233 +309,235 @@ optional priority can be declared, 0 being the highest priority as for auto hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. -Variants: - - -.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term +.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type ``forall binders, Class t1 … tn``. One need not even mention the unique field name for singleton classes. -.. cmd:: Global Instance +.. cmdv:: Global Instance One can use the ``Global`` modifier on instances declared in a section so that their generalization is automatically redeclared after the section is closed. -.. cmd:: Program Instance +.. cmdv:: Program Instance + :name: Program Instance - Switches the type-checking to Program (chapter :ref:`program`) and + Switches the type-checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. -.. cmd:: Declare Instance +.. cmdv:: Declare Instance + :name: Declare Instance In a Module Type, this command states that a corresponding concrete - instance should exist in any implementation of thisModule Type. This - is similar to the distinction betweenParameter vs. Definition, or - between Declare Module and Module. + instance should exist in any implementation of this Module Type. This + is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or + between :cmd:`Declare Module` and :cmd:`Module`. -Besides the ``Class`` and ``Instance`` vernacular commands, there are a +Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to type classes. -.. _ExistingInstance: - -Existing Instance -~~~~~~~~~~~~~~~~~ - .. cmd:: Existing Instance {+ @ident} [| priority] -This commands adds an arbitrary list of constants whose type ends with -an applied type class to the instance database with an optional -priority. It can be used for redeclaring instances at the end of -sections, or declaring structure projections as instances. This is -equivalent to ``Hint Resolve ident : typeclass_instances``, except it -registers instances for ``Print Instances``. - -.. _Context: - -Context -~~~~~~~ + This commands adds an arbitrary list of constants whose type ends with + an applied type class to the instance database with an optional + priority. It can be used for redeclaring instances at the end of + sections, or declaring structure projections as instances. This is + equivalent to ``Hint Resolve ident : typeclass_instances``, except it + registers instances for :cmd:`Print Instances`. .. cmd:: Context @binders -Declares variables according to the given binding context, which might -use :ref:`implicit-generalization`. + Declares variables according to the given binding context, which might + use :ref:`implicit-generalization`. + +.. tacn:: typeclasses eauto + :name: typeclasses eauto + + This tactic uses a different resolution engine than :tacn:`eauto` and + :tacn:`auto`. The main differences are the following: + + + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in + the new proof engine (as of Coq 8.6), meaning that backtracking is + available among dependent subgoals, and shelving goals is supported. + typeclasses eauto is a multi-goal tactic. It analyses the dependencies + between subgoals to avoid backtracking on subgoals that are entirely + independent. + + + When called with no arguments, typeclasses eauto uses + the ``typeclass_instances`` database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior of Coq 8.5). + + .. note:: + As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully + mimicks what happens during typeclass resolution when it is called + during refinement/type-inference, except that *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 ``all:typeclasses eauto`` in future versions when the + refinement engine will be able to backtrack. + + + When called with specific databases (e.g. with), typeclasses eauto + allows shelved goals to remain at any point during search and treat + typeclasses goals like any other. + + + 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 :cmd:`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. + + + .. cmdv:: typeclasses eauto @num + + .. warning:: + The semantics for the limit :n:`@num` + is different than for auto. By default, if no limit is given the + search is unbounded. Contrary to auto, introduction steps (intro) are + counted, which might result in larger limits being necessary when + searching with typeclasses eauto than auto. + + .. cmdv:: typeclasses eauto with {+ @ident} + + 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). + +.. tacn:: autoapply @term with @ident + :name: autoapply + + The tactic autoapply applies a term using the transparency information + of the hint database ident, and does *no* typeclass resolution. This can + be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint + database ``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. +.. _TypeclassesTransparent: -.. _typeclasses-eauto: - -``typeclasses eauto`` -~~~~~~~~~~~~~~~~~~~~~ - -The ``typeclasses eauto`` tactic uses a different resolution engine than -eauto and auto. The main differences are the following: - -+ Contrary to ``eauto`` and ``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. - typeclasses eauto is a multi-goal tactic. It analyses the dependencies - between subgoals to avoid backtracking on subgoals that are entirely - independent. - -+ When called with no arguments, typeclasses eauto uses - thetypeclass_instances database by default (instead of core). - Dependent subgoals are automatically shelved, and shelved goals can - remain after resolution ends (following the behavior ofCoq 8.5). - *Note: * As of Coq 8.6, all:once (typeclasses eauto) faithfully - mimicks what happens during typeclass resolution when it is called - during refinement/type-inference, except that *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 ``all:typeclasses eauto`` in future versions when the - refinement engine will be able to backtrack. - -+ When called with specific databases (e.g. with), typeclasses eauto - allows shelved goals to remain at any point during search and treat - typeclasses goals like any other. - -+ 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 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. - - -Variants: - -#. ``typeclasses eauto [num]`` +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - *Warning:* The semantics for the limit num - is different than for auto. By default, if no limit is given the - search is unbounded. Contrary to auto, introduction steps (intro) are - counted, which might result in larger limits being necessary when - searching with typeclasses eauto than auto. +.. cmd:: Typeclasses Transparent {+ @ident} -#. ``typeclasses eauto with {+ @ident}`` + This command defines makes the identifiers transparent during type class + resolution. - 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). +.. cmd:: Typeclasses Opaque {+ @ident} -.. _autoapply: + Make the identifiers opaque for typeclass search. It is useful when some + constants prevent some unifications and make resolution fail. It is also + useful to declare constants which should never be unfolded during + proof-search, like fixpoints or anything which does not look like an + abbreviation. This can additionally speed up proof search as the typeclass + map can be indexed by such rigid constants (see + :ref:`thehintsdatabasesforautoandeauto`). -``autoapply term with ident`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +By default, all constants and local variables are considered transparent. One +should take care not to make opaque any constant that is used to abbreviate a +type, like: -The tactic autoapply applies a term using the transparency information -of the hint database ident, and does *no* typeclass resolution. This can -be used in ``Hint Extern``’s for typeclass instances (in the hint -database ``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. +:: -.. _TypeclassesTransparent: + relation A := A -> A -> Prop. -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} - This commands defines the transparency of the given identifiers - during type class resolution. It is useful when some constants - prevent some unifications and make resolution fail. It is also useful - to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the - typeclass map can be indexed by such rigid constants (see - :ref:`thehintsdatabasesforautoandeauto`). By default, all constants - and local variables are considered transparent. One should take care - not to make opaque any constant that is used to abbreviate a type, - like: +Options +~~~~~~~ -:: +.. opt:: Typeclasses Dependency Order - relation A := A -> A -> Prop. + 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 8.5 and below). This can result in + quite different performance behaviors of proof search. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. +.. opt:: Typeclasses Filtered Unification -Set Typeclasses Dependency Order -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + 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 *matches* syntactically the + inferred or specified pattern of the hint, and only then try to + *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. -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. +.. opt:: Typeclasses Limit Intros -Set Typeclasses Filtered Unification -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + 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 introduction. + *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). -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 *matches* syntactically the -inferred or specified pattern of the hint, and only then try to -*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. +.. opt:: Typeclass Resolution For Conversion -Set Typeclasses Limit Intros -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + 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. -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 introduction. -*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). +.. opt:: 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. -Set Typeclass 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. +.. opt:: 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. -Set 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. +.. opt:: 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. -Set Typeclasses Unique Solutions -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Debug {? Verbosity @num} -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. + These options allow to see the resolution steps of typeclasses that are + performed during search. The ``Debug`` option is synonymous to ``Debug + Verbosity 1``, and ``Debug Verbosity 2`` provides more information + (tried tactics, shelving of goals, etc…). +.. opt:: Refine Instance Mode -Set Typeclasses Unique Instances -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option allows to switch the behavior of instance declarations made through + the Instance command. -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. + + When it is on (the default), instances that have unsolved holes in + their proof-term silently open the proof mode with the remaining + obligations to prove. + + When it is off, they fail with an error instead. Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ @@ -561,27 +554,3 @@ Typeclasses eauto `:=` default) or breadth-first search. + ``depth`` This sets the depth limit of the search. - - -Set Typeclasses Debug -~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Set Typeclasses Debug {? Verbosity @num} - -These options allow to see the resolution steps of typeclasses that are -performed during search. The ``Debug`` option is synonymous to ``Debug -Verbosity 1``, and ``Debug Verbosity 2`` provides more information -(tried tactics, shelving of goals, etc…). - - -Set Refine Instance Mode -~~~~~~~~~~~~~~~~~~~~~~~~ - -The option Refine Instance Mode allows to switch the behavior of -instance declarations made through the Instance command. - -+ When it is on (the default), instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - -+ When it is off, they fail with an error instead. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst new file mode 100644 index 0000000000..6e7ccba63c --- /dev/null +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -0,0 +1,445 @@ +.. include:: ../replaces.rst + +.. _polymorphicuniverses: + +Polymorphic Universes +====================== + +:Author: Matthieu Sozeau + +General Presentation +--------------------- + +.. warning:: + + The status of Universe Polymorphism is experimental. + +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. + +A standard example of the difference between universe *polymorphic* +and *monomorphic* definitions is given by the identity function: + +.. coqtop:: in + + Definition identity {A : Type} (a : A) := a. + +By default, constant declarations are monomorphic, hence the identity +function declares a global universe (say ``Top.1``) for its domain. +Subsequently, if we try to self-apply the identity, we will get an +error: + +.. coqtop:: all + + Fail Definition selfid := identity (@identity). + +Indeed, the global level ``Top.1`` would have to be strictly smaller than +itself for this self-application to typecheck, as the type of +:g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself +:g:`Type@{Top.1+1}`. + +A universe polymorphic identity function binds its domain universe +level at the definition level instead of making it global. + +.. coqtop:: in + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + +.. coqtop:: all + + About pidentity. + +It is then possible to reuse the constant at different levels, like +so: + +.. coqtop:: in + + Definition selfpid := pidentity (@pidentity). + +Of course, the two instances of :g:`pidentity` in this definition are +different. This can be seen when the :opt:`Printing Universes` option is on: + +.. coqtop:: none + + Set Printing Universes. + +.. coqtop:: all + + Print selfpid. + +Now :g:`pidentity` is used at two different levels: at the head of the +application it is instantiated at ``Top.3`` while in the argument position +it is instantiated at ``Top.4``. This definition is only valid as long as +``Top.4`` is strictly smaller than ``Top.3``, as show by the constraints. Note +that this definition is monomorphic (not universe polymorphic), so the +two universes (in this case ``Top.3`` and ``Top.4``) are actually global +levels. + +When printing :g:`pidentity`, we can see the universes it binds in +the annotation :g:`@{Top.2}`. Additionally, when +:opt:`Printing Universes` is on we print the "universe context" of +:g:`pidentity` consisting of the bound universes and the +constraints they must verify (for :g:`pidentity` there are no constraints). + +Inductive types can also be declared universes polymorphic on +universes appearing in their parameters or fields. A typical example +is given by monoids: + +.. coqtop:: in + + Polymorphic Record Monoid := { mon_car :> Type; mon_unit : mon_car; + mon_op : mon_car -> mon_car -> mon_car }. + +.. coqtop:: in + + Print Monoid. + +The Monoid's carrier universe is polymorphic, hence it is possible to +instantiate it for example with :g:`Monoid` itself. First we build the +trivial unit monoid in :g:`Set`: + +.. coqtop:: in + + Definition unit_monoid : Monoid := + {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}. + +From this we can build a definition for the monoid of :g:`Set`\-monoids +(where multiplication would be given by the product of monoids). + +.. coqtop:: in + + Polymorphic Definition monoid_monoid : Monoid. + refine (@Build_Monoid Monoid unit_monoid (fun x y => x)). + Defined. + +.. coqtop:: all + + Print monoid_monoid. + +As one can see from the constraints, this monoid is “large”, it lives +in a universe strictly higher than :g:`Set`. + +Polymorphic, Monomorphic +------------------------- + +.. cmd:: Polymorphic @definition + + As shown in the examples, polymorphic definitions and inductives can be + declared using the ``Polymorphic`` prefix. + +.. opt:: Universe Polymorphism + + Once enabled, this option will implicitly prepend ``Polymorphic`` to any + definition of the user. + +.. cmd:: Monomorphic @definition + + When the :opt:`Universe Polymorphism` option is set, to make a definition + producing global universe constraints, one can use the ``Monomorphic`` prefix. + +Many other commands support the ``Polymorphic`` flag, including: + +.. TODO add links on each of these? + +- ``Lemma``, ``Axiom``, and all the other “definition” keywords support + polymorphism. + +- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support + polymorphism. This means that the universe variables (and associated + constraints) are discharged polymorphically over definitions that use + them. In other words, two definitions in the section sharing a common + variable will both get parameterized by the universes produced by the + variable declaration. This is in contrast to a “mononorphic” variable + which introduces global universes and constraints, making the two + definitions depend on the *same* global universes associated to the + variable. + +- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint + polymorphically, not at a single instance. + +Cumulative, NonCumulative +------------------------- + +Polymorphic inductive types, coinductive types, variants and records can be +declared cumulative using the :g:`Cumulative` prefix. + +.. cmd:: Cumulative @inductive + + Declares the inductive as cumulative + +Alternatively, there is an option :opt:`Polymorphic Inductive +Cumulativity` which when set, makes all subsequent *polymorphic* +inductive definitions cumulative. When set, inductive types and the +like can be enforced to be non-cumulative using the :g:`NonCumulative` +prefix. + +.. cmd:: NonCumulative @inductive + + Declares the inductive as non-cumulative + +.. opt:: Polymorphic Inductive Cumulativity + + When this option is on, it sets all following polymorphic inductive + types as cumulative (it is off by default). + +Consider the examples below. + +.. coqtop:: in + + Polymorphic Cumulative Inductive list {A : Type} := + | nil : list + | cons : A -> list -> list. + +.. coqtop:: all + + Print list. + +When printing :g:`list`, the universe context indicates the subtyping +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), +respectively represented by the symbols `=`, `+` and `*`. + +Here we see that :g:`list` binds an irrelevant universe, so any two +instances of :g:`list` are convertible: :math:`E[Γ] ⊢ \mathsf{list}@\{i\}~A +=_{βδιζη} \mathsf{list}@\{j\}~B` whenever :math:`E[Γ] ⊢ A =_{βδιζη} B` and +this applies also to their corresponding constructors, when +they are comparable at the same type. + +See :ref:`Conversion-rules` for more details on convertibility and subtyping. +The following is an example of a record with non-trivial subtyping relation: + +.. coqtop:: all + + Polymorphic Cumulative Record packType := {pk : Type}. + +:g:`packType` binds a covariant universe, i.e. + +.. math:: + + E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} + \mathsf{packType}@\{j\}~\mbox{ whenever }~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 :g:`Cumulative` or +:g:`NonCumulative` prefix in a monomorphic context. +Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`. +That is, this option, when set, makes all subsequent *polymorphic* +inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) +but has no effect on *monomorphic* inductive declarations. + +Consider the following examples. + +.. coqtop:: all reset + + Monomorphic Cumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Monomorphic NonCumulative Inductive Unit := unit. + +.. coqtop:: all reset + + Set Polymorphic Inductive Cumulativity. + Inductive Unit := unit. + +An example of a proof using cumulativity +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. coqtop:: in + + 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 down. + +Cumulativity Weak Constraints +----------------------------- + +.. opt:: Cumulativity Weak Constraints + +This option, on by default, causes "weak" constraints to be produced +when comparing universes in an irrelevant position. Processing weak +constraints is delayed until minimization time. A weak constraint +between `u` and `v` when neither is smaller than the other and +one is flexible causes them to be unified. Otherwise the constraint is +silently discarded. + +This heuristic is experimental and may change in future versions. +Disabling weak constraints is more predictable but may produce +arbitrary numbers of universes. + + +Global and local universes +--------------------------- + +Each universe is declared in a global or local environment before it +can be used. To ensure compatibility, every *global* universe is set +to be strictly greater than :g:`Set` when it is introduced, while every +*local* (i.e. polymorphically quantified) universe is introduced as +greater or equal to :g:`Set`. + + +Conversion and unification +--------------------------- + +The semantics of conversion and unification have to be modified a +little to account for the new universe instance arguments to +polymorphic references. The semantics respect the fact that +definitions are transparent, so indistinguishable from their bodies +during conversion. + +This is accomplished by changing one rule of unification, the first- +order approximation rule, which applies when two applicative terms +with the same head are compared. It tries to short-cut unfolding by +comparing the arguments directly. In case the constant is universe +polymorphic, we allow this rule to fire only when unifying the +universes results in instantiating a so-called flexible universe +variables (not given by the user). Similarly for conversion, if such +an equation of applicative terms fail due to a universe comparison not +being satisfied, the terms are unfolded. This change implies that +conversion and unification can have different unfolding behaviors on +the same development with universe polymorphism switched on or off. + + +Minimization +------------- + +Universe polymorphism with cumulativity tends to generate many useless +inclusion constraints in general. Typically at each application of a +polymorphic constant :g:`f`, if an argument has expected type :g:`Type@{i}` +and is given a term of type :g:`Type@{j}`, a :math:`j ≤ i` constraint will be +generated. It is however often the case that an equation :math:`j = i` would +be more appropriate, when :g:`f`\'s universes are fresh for example. +Consider the following example: + +.. coqtop:: none + + Polymorphic Definition pidentity {A : Type} (a : A) := a. + Set Printing Universes. + +.. coqtop:: in + + Definition id0 := @pidentity nat 0. + +.. coqtop:: all + + Print id0. + +This definition is elaborated by minimizing the universe of :g:`id0` to +level :g:`Set` while the more general definition would keep the fresh level +:g:`i` generated at the application of :g:`id` and a constraint that :g:`Set` :math:`≤ i`. +This minimization process is applied only to fresh universe variables. +It simply adds an equation between the variable and its lower bound if +it is an atomic universe (i.e. not an algebraic max() universe). + +.. opt:: Universe Minimization ToSet + + Turning this option off (it is on by default) disallows minimization + to the sort :g:`Set` and only collapses floating universes between + themselves. + + +Explicit Universes +------------------- + +The syntax has been extended to allow users to explicitly bind names +to universes and explicitly instantiate polymorphic definitions. + +.. cmd:: Universe @ident + + In the monorphic case, this command declares a new global universe + named :g:`ident`, which can be referred to using its qualified name + as well. Global universe names live in a separate namespace. The + command supports the polymorphic flag only in sections, meaning the + universe quantification will be discharged on each section definition + independently. One cannot mix polymorphic and monomorphic + declarations in the same section. + + +.. cmd:: Constraint @ident @ord @ident + + This command declares a new constraint between named universes. The + order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint + is then enforced in the global environment. Like ``Universe``, it can be + used with the ``Polymorphic`` prefix in sections only to declare + constraints discharged at section closing time. One cannot declare a + global constraint on polymorphic universes. + + .. exn:: Undeclared universe @ident. + + .. exn:: Universe inconsistency. + + +Polymorphic definitions +~~~~~~~~~~~~~~~~~~~~~~~ + +For polymorphic definitions, the declaration of (all) universe levels +introduced by a definition uses the following syntax: + +.. coqtop:: in + + Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. + +.. coqtop:: all + + Print le. + +During refinement we find that :g:`j` must be larger or equal than :g:`i`, as we +are using :g:`A : Type@{i} <= Type@{j}`, hence the generated constraint. At the +end of a definition or proof, we check that the only remaining +universes are the ones declared. In the term and in general in proof +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. + +Definitions can also be instantiated explicitly, giving their full +instance: + +.. coqtop:: all + + Check (pidentity@{Set}). + Monomorphic Universes k l. + Check (le@{k l}). + +User-named universes and the anonymous universe implicitly attached to +an explicit :g:`Type` are considered rigid for unification and are never +minimized. Flexible anonymous universes can be produced with an +underscore or by omitting the annotation to a polymorphic definition. + +.. coqtop:: all + + Check (fun x => x) : Type -> Type. + Check (fun x => x) : Type -> Type@{_}. + + Check le@{k _}. + Check le. + +.. opt:: Strict Universe Declaration. + + Turning this option off allows one to freely use + identifiers for universes without declaring them first, with the + semantics that the first use declares it. In this mode, the universe + names are not associated with the definition or proof once it has been + defined. This is meant mainly for debugging purposes. |