diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 107 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 31 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 81 |
11 files changed, 195 insertions, 92 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index b568160356..45b3f6f161 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -192,7 +192,7 @@ Disjunctive patterns -------------------- Multiple patterns that share the same right-hand-side can be -factorized using the notation :n:`{+| @mult_pattern}`. For +factorized using the notation :n:`{+| @patterns_comma}`. For instance, :g:`max` can be rewritten as follows: .. coqtop:: in reset diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3dc8707a34..7136cc28d1 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -127,20 +127,21 @@ Concerning Haskell, type-preserving optimizations are less useful because of laziness. We still make some optimizations, for example in order to produce more readable code. -The type-preserving optimizations are controlled by the following |Coq| options: +The type-preserving optimizations are controlled by the following |Coq| flags +and commands: .. flag:: 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 + simplifications on Cases, etc). Turn this flag off if you want a ML term as close as possible to the Coq term. .. flag:: 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 - types). Turn this option on to make sure that ``e:t`` + types). Turn this flag on to make sure that ``e:t`` implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted code of ``e`` and ``t`` respectively. @@ -150,7 +151,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: produces a singleton type (i.e. a type with only one constructor, and only one argument to this constructor), the inductive structure is removed and this type is seen as an alias to the inner type. - The typical example is ``sig``. This option allows disabling this + The typical example is ``sig``. This flag allows disabling this optimization when one wishes to preserve the inductive structure of types. .. flag:: Extraction AutoInline @@ -159,7 +160,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: some defined constants, according to some heuristics like size of bodies, uselessness of some arguments, etc. Those heuristics are not always perfect; if you want to disable - this feature, turn this option off. + this feature, turn this flag off. .. cmd:: Extraction Inline {+ @qualid } @@ -223,11 +224,11 @@ principles of extraction (logical parts and types). When an actual extraction takes place, an error is normally raised if the :cmd:`Extraction Implicit` declarations cannot be honored, that is if any of the implicit arguments still occurs in the final code. -This behavior can be relaxed via the following option: +This behavior can be relaxed via the following flag: .. flag:: Extraction SafeImplicits - Default is on. When this option is off, a warning is emitted + Default is on. When this flag is off, a warning is emitted instead of an error if some implicit arguments still occur in the final code of an extraction. This way, the extracted code may be obtained nonetheless and reviewed manually to locate the source of the issue @@ -282,7 +283,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 :undocumented: The number of type variables is checked by the system. For example: @@ -529,7 +530,7 @@ A detailed example: Euclidean division ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The file ``Euclid`` contains the proof of Euclidean division. -The natural numbers used here are unary, represented by the type``nat``, +The natural numbers used here are unary, represented by the type ``nat``, which is defined by two constructors ``O`` and ``S``. This module contains a theorem ``eucl_dev``, whose type is:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 2ea0861e47..ca5b5e54a7 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. example:: Morphisms Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` - perform the union of two sets by appending one list to the other. ``union` is a binary + perform the union of two sets by appending one list to the other. ``union`` is a binary morphism parametric over ``A`` that respects the relation instance ``(set_eq A)``. The latter condition is proved by showing: @@ -714,8 +714,10 @@ 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 :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a +on the programmable rewriting strategies with generic traversals by Visser et al. +:cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of +the Stratego transformation language :cite:`Visser01`. Rewriting strategies +are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a strategy expression. Strategies are defined inductively as described by the following grammar: @@ -739,7 +741,7 @@ following grammar: : topdown `strategy` (top-down) : hints `ident` (apply hints from hint database) : terms `term` ... `term` (any of the terms) - : eval `redexpr` (apply reduction) + : eval `red_expr` (apply reduction) : fold `term` (unify) : ( `strategy` ) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 7fee62179b..c3b197288f 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -274,7 +274,7 @@ Activating the Printing of Coercions .. flag:: Printing Coercions - When on, this option forces all the coercions to be printed. + When on, this flag forces all the coercions to be printed. By default, coercions are not printed. .. table:: Printing Coercion @qualid diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e56b36caad..cc19c8b6a9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -9,9 +9,11 @@ Short description of the tactics -------------------------------- The Psatz module (``Require Import Psatz.``) gives access to several -tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. -It also possible to get the tactics for integers by a ``Require Import Lia``, -rationals ``Require Import Lqa`` and reals ``Require Import Lra``. +tactics for solving arithmetic goals over :math:`\mathbb{Q}`, +:math:`\mathbb{R}`, and :math:`\mathbb{Z}` but also :g:`nat` and +:g:`N`. It also possible to get the tactics for integers by a +``Require Import Lia``, rationals ``Require Import Lqa`` and reals +``Require Import Lra``. + :tacn:`lia` is a decision procedure for linear integer arithmetic; + :tacn:`nia` is an incomplete proof procedure for integer non-linear @@ -23,16 +25,28 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. ``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 + driver to the external prover `csdp` [#csdp]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts even without `csdp`. .. flag:: Simplex - This option (set by default) instructs the decision procedures to + This flag (set by default) instructs the decision procedures to use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. flag:: Lia Cache + + This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` + +.. flag:: Nia Cache + + This flag (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache` + +.. flag:: Nra Cache + + This flag (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache` + The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. @@ -78,7 +92,7 @@ closed under the following rules: \end{array}` The following theorem provides a proof principle for checking that a -set of polynomial inequalities does not have solutions [#]_. +set of polynomial inequalities does not have solutions [#fnpsatz]_. .. _psatz_thm: @@ -111,32 +125,21 @@ and checked to be :math:`-1`. The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. - `lia`: a tactic for linear integer arithmetic --------------------------------------------- .. tacn:: lia :name: lia - This tactic offers an alternative to the :tacn:`omega` tactic. 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` does not solve, such as the following so-called *omega - nightmare* :cite:`TheOmegaPaper`. + This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. + :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. -.. coqdoc:: - - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. - -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof -principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this @@ -249,21 +252,55 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. -.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with - the ``zify`` tactic. -.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by - pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may - need to manually run ``zify`` first). -.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing - the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually - run ``zify`` first). -.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and - :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the - ``Z.to_euclidean_division_equations`` tactic (you may need to manually run - ``zify`` first). -.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp -.. [#] Variants deal with equalities and strict inequalities. -.. [#] In practice, the oracle might fail to produce such a refutation. +`zify`: pre-processing of arithmetic goals +------------------------------------------ + +.. tacn:: zify + :name: zify + + This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. + By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`. + + + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + +.. cmd:: Show Zify InjTyp + :name: Show Zify InjTyp + + This command shows the list of types that can be injected into :g:`Z`. + +.. cmd:: Show Zify BinOp + :name: Show Zify BinOp + + This command shows the list of binary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify BinRel + :name: Show Zify BinRel + + This command shows the list of binary relations processed by :tacn:`zify`. + + +.. cmd:: Show Zify UnOp + :name: Show Zify UnOp + + This command shows the list of unary operators processed by :tacn:`zify`. + +.. cmd:: Show Zify CstOp + :name: Show Zify CstOp + + This command shows the list of constants processed by :tacn:`zify`. + +.. cmd:: Show Zify Spec + :name: Show Zify Spec + + This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`. + +.. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#fnpsatz] Variants deal with equalities and strict inequalities. +.. [#mayfail] In practice, the oracle might fail to produce such a refutation. .. comment in original TeX: .. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index b008508bbc..650a444a16 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -119,21 +119,21 @@ Options .. deprecated:: 8.5 - This deprecated option (on by default) is for compatibility with Coq pre 8.5. It + This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. .. flag:: Omega UseLocalDefs - This option (on by default) allows :tacn:`omega` to use the bodies of local + This flag (on by default) allows :tacn:`omega` to use the bodies of local variables. .. flag:: Omega System - This option (off by default) activate the printing of debug information + This flag (off by default) activate the printing of debug information .. flag:: Omega Action - This option (off by default) activate the printing of debug information + This flag (off by default) activate the printing of debug information Technical data -------------- diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 903ee115c9..35729d852d 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -58,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed`` +The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed`` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. @@ -162,7 +162,7 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the generation and checking of the proof objects. The ``-quick`` flag can be -passed to ``coqc`` or ``coqtop`` to produce, quickly, ``.vio`` files. +passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, the ``quick`` target can be used to compile all files using the ``-quick`` flag. @@ -182,7 +182,7 @@ running ``coqc`` as usual. Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All .vio files can be processed in parallel, hence this alternative might -be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +be faster. The command ``coqc -schedule-vio2vo 2 a b c`` can be used to obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and ``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target can be used for that purpose. Variable ``J`` should be set to the number @@ -197,7 +197,7 @@ There is an extra, possibly even faster, alternative: just check the proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This is possibly faster because all the proof tasks are independent, hence one can further partition the job to be done between workers. The -``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +``coqc -schedule-vio-checking 6 a b c`` command can be used to obtain a good scheduling for 6 workers to check all the proof tasks of ``a.vio``, ``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 45c74ab02a..a17dca1693 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -78,7 +78,7 @@ operation (see :ref:`extendedpatternmatching`). also works with the previous mechanism. -There are options to control the generation of equalities and +There are flags to control the generation of equalities and coercions. .. flag:: Program Cases @@ -86,13 +86,13 @@ coercions. This controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm - of |Coq| (see :ref:`extendedpatternmatching`) when this option is + of |Coq| (see :ref:`extendedpatternmatching`) when this flag is deactivated. .. flag:: Program Generalized Coercion This controls the coercion of general inductive types when using |Program| - (the option is on by default). Coercion of subset types and pairs is still + (the flag is on by default). Coercion of subset types and pairs is still active in this case. .. flag:: Program Mode @@ -341,9 +341,9 @@ optional tactic is replaced by the default one if not specified. .. flag:: Shrink Obligations - *Deprecated since 8.7* + .. deprecated:: 8.7 - This option (on by default) controls whether obligations should have + This flag (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 8935ba27e3..9acdd18b89 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -9,15 +9,18 @@ SProp (proof irrelevant propositions) This section describes the extension of |Coq| with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also -known as strict propositions). To use :math:`\SProp` you must pass -``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`. +known as strict propositions) as described in +:cite:`Gilbert:POPL2019`. + +Using :math:`\SProp` may be prevented by passing ``-disallow-sprop`` +to the |Coq| program or using :flag:`Allow StrictProp`. .. flag:: Allow StrictProp :name: Allow StrictProp Allows using :math:`\SProp` when set and forbids it when unset. The initial value depends on whether you used the command line - ``-allow-sprop``. + ``-disallow-sprop`` and ``-allow-sprop``. .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. :undocumented: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index db3e20a9c6..661aa88082 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using :cmd:`Program Instance`, if one does not give all the members in -the Instance declaration, Coq generates obligations for the remaining -fields, e.g.: +Using the attribute ``refine``, if the term is not sufficient to +finish the definition (e.g. due to a missing field or non-inferable +hole) it must be finished in proof mode. If it is sufficient a trivial +proof mode with no open goals is started. + +.. coqtop:: in + + #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }. + Proof. intros [] [];reflexivity. Defined. + +Note that if you finish the proof with :cmd:`Qed` the entire instance +will be opaque, including the fields given in the initial term. + +Alternatively, in :flag:`Program Mode` if one does not give all the +members in the Instance declaration, Coq generates obligations for the +remaining fields, e.g.: .. coqtop:: in @@ -560,8 +573,16 @@ Settings Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this - option to 0 turns that option off. + of goals. Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this + option to 0 turns that flag off. + +.. flag:: Typeclasses Axioms Are Instances + + .. deprecated:: 8.10 + + This flag (off by default since 8.8) automatically declares axioms + whose type is a typeclass at declaration time as instances of that + class. Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e698bfb66..7adb25cbd6 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -129,12 +129,12 @@ Polymorphic, Monomorphic .. flag:: Universe Polymorphism - Once enabled, this option will implicitly prepend ``Polymorphic`` to any + Once enabled, this flag will implicitly prepend ``Polymorphic`` to any definition of the user. .. cmd:: Monomorphic @definition - When the :flag:`Universe Polymorphism` option is set, to make a definition + When the :flag:`Universe Polymorphism` flag is set, to make a definition producing global universe constraints, one can use the ``Monomorphic`` prefix. Many other commands support the ``Polymorphic`` flag, including: @@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including: - :cmd:`Section` will locally set the polymorphism flag inside the section. - ``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. + polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint polymorphically, not at a single instance. @@ -169,8 +162,8 @@ declared cumulative using the :g:`Cumulative` prefix. Declares the inductive as cumulative -Alternatively, there is a flag :flag:`Polymorphic Inductive -Cumulativity` which when set, makes all subsequent *polymorphic* +Alternatively, there is a :flag:`Polymorphic Inductive +Cumulativity` flag 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. @@ -181,7 +174,7 @@ prefix. .. flag:: Polymorphic Inductive Cumulativity - When this option is on, it sets all following polymorphic inductive + When this flag is on, it sets all following polymorphic inductive types as cumulative (it is off by default). Consider the examples below. @@ -229,8 +222,8 @@ Cumulative inductive types, coinductive 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 :flag:`Polymorphic Inductive Cumulativity`. -That is, this option, when set, makes all subsequent *polymorphic* +Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag. +That is, this flag, 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. @@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions. 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. - + independently. .. cmd:: Constraint @universe_constraint Polymorphic Constraint @universe_constraint @@ -448,7 +439,7 @@ underscore or by omitting the annotation to a polymorphic definition. .. flag:: Strict Universe Declaration - Turning this option off allows one to freely use + Turning this flag 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 @@ -456,7 +447,7 @@ underscore or by omitting the annotation to a polymorphic definition. .. flag:: Private Polymorphic Universes - This option, on by default, removes universes which appear only in + This flag, on by default, removes universes which appear only in the body of an opaque polymorphic definition from the definition's universe arguments. As such, no value needs to be provided for these universes when instantiating the definition. Universe @@ -489,7 +480,7 @@ underscore or by omitting the annotation to a polymorphic definition. About foo. To recover the same behaviour with regard to universes as - :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + :g:`Defined`, the :flag:`Private Polymorphic Universes` flag may be unset: .. coqtop:: all @@ -510,3 +501,51 @@ underscore or by omitting the annotation to a polymorphic definition. Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. About baz. + +.. _universe-polymorphism-in-sections: + +Universe polymorphism and sections +---------------------------------- + +:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and +:cmd:`Constraint` in a section support polymorphism. This means that +the universe variables and their 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. + +It is possible to mix universe polymorphism and monomorphism in +sections, except in the following ways: + +- no monomorphic constraint may refer to a polymorphic universe: + + .. coqtop:: all reset + + Section Foo. + + Polymorphic Universe i. + Fail Constraint i = i. + + This includes constraints implictly declared by commands such as + :cmd:`Variable`, which may as a such need to be used with universe + polymorphism activated (locally by attribute or globally by option): + + .. coqtop:: all + + Fail Variable A : (Type@{i} : Type). + Polymorphic Variable A : (Type@{i} : Type). + + (in the above example the anonymous :g:`Type` constrains polymorphic + universe :g:`i` to be strictly smaller.) + +- no monomorphic constant or inductive may be declared if polymorphic + universes or universe constraints are present. + +These restrictions are required in order to produce a sensible result +when closing the section (the requirement on constants and inductives +is stricter than the one on constraints, because constants and +inductives are abstracted by *all* the section's polymorphic universes +and constraints). |