diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 56 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 66 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 5 |
5 files changed, 102 insertions, 52 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1d0b732e7d..905068e316 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -507,17 +507,45 @@ underscore or by omitting the annotation to a polymorphic definition. Universe polymorphism and sections ---------------------------------- -The universe polymorphic or monomorphic status is -attached to each individual section, and all term or universe declarations -contained inside must respect it, as described below. It is possible to nest a -polymorphic section inside a monomorphic one, but the converse is not allowed. - -: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. +: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). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 38b3c34209..0148925247 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -718,6 +718,14 @@ Changes in 8.10+beta3 follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, which added ``uncons`` in 8.10+beta1). +Changes in 8.10.0 +~~~~~~~~~~~~~~~~~ + +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). + Version 8.9 ----------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index dc4f91e66b..2d047a1058 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -638,7 +638,11 @@ the induction principle to easily reason about the function. than like this: - .. coqtop:: reset all + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all Function plus (n m : nat) {struct n} : nat := match n with @@ -649,17 +653,22 @@ the induction principle to easily reason about the function. *Limitations* -|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`) +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of :g:`wrong` in the body of :g:`wrong`: -.. coqtop:: all +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail - Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). For now, dependent cases are not treated for non structurally terminating functions. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa6d62ffa2..c910136406 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`. flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` and ``cofix``. The ``delta`` flag itself can be refined into - :n:`delta {+ @qualid}` or :n:`delta -{+ @qualid}`, restricting in the first + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first case the constants to unfold to the constants listed, and restricting in the second case the constant to unfold to all but the ones explicitly mentioned. Notice that the ``delta`` flag does not apply to variables bound by a let-in @@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. -.. tacv:: compute {+ @qualid} - cbv {+ @qualid} +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. -.. tacv:: compute -{+ @qualid} - cbv -{+ @qualid} +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. -.. tacv:: lazy {+ @qualid} - lazy -{+ @qualid} +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. This algorithm is dramatically more efficient than the algorithm used for the - ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. @@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be - typically two to five times faster than ``vm_compute``. Note however that the + typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this option makes - it possible to profile ``native_compute`` evaluations. + it possible to profile :tacn:`native_compute` evaluations. .. opt:: NativeCompute Profile Filename @string :name: NativeCompute Profile Filename @@ -3097,7 +3097,7 @@ the conversion in hypotheses :n:`{+ @ident}`. will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means you can individually profile multiple uses of - ``native_compute`` in a script. From the Linux command line, run ``perf report`` + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` on the profile file to see the results. Consult the ``perf`` documentation for more details. @@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The ``cbn`` tactic is claimed to be a more principled, faster and more - predictable replacement for ``simpl``. + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. - The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The - behavior of both ``simpl`` and ``cbn`` can be tuned using the - Arguments vernacular command as follows: + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the Arguments vernacular command as follows: - + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: + + A constant can be marked to be never unfolded by :tacn:`cbn` or + :tacn:`simpl`: .. example:: @@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus n m : simpl never. After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics ``cbn`` and ``simpl``. + untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the @@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by - ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. + :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. The same mechanism can be used to make a constant volatile, i.e. always unfolded. @@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus !n !m. After that command, the expression :g:`(minus (S x) y)` is left untouched - by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + A special heuristic to determine if a constant has to be unfolded can be activated with the following command: @@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` even if an extra simplification is possible. - In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it + In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`- reduction. But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on + :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on :g:`(plus n O) = n` changes nothing. Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by ``simpl``. For instance a + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a constant defined by :g:`plus' := plus` is possibly unfolded and reused in the recursive calls, but a constant such as :g:`succ := plus (S O)` is - never unfolded. This is the main difference between ``simpl`` and ``cbn``. - The tactic ``cbn`` reduces whenever it will be able to reuse it or not: + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: :g:`succ t` is reduced to :g:`S t`. -.. tacv:: cbn {+ @qualid} - cbn -{+ @qualid} +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] - These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` - and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). .. tacv:: simpl @pattern @@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3265,7 +3266,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @qualid at {+ @num} simpl @string at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM @@ -3960,6 +3961,9 @@ At Coq startup, only the core database is nonempty and can be used. :fset: internal database for the implementation of the ``FSets`` library. +:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), + mainly used in the ``FSets`` and ``FMaps`` libraries. + You are advised not to put your own hints in the core database, but use one or several databases specific to your development. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 2885d6dc33..843459b723 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1012,8 +1012,9 @@ Controlling display .. flag:: Printing Dependent Evars Line - This option controls the printing of the “(dependent evars: …)” line when - ``-emacs`` is passed. + This option controls the printing of the “(dependent evars: …)” information + after each tactic. The information is used by the Prooftree tool in Proof + General. (https://askra.de/software/prooftree) .. _vernac-controlling-the-reduction-strategies: |