diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_static/diffs-show-proof.png | bin | 0 -> 13641 bytes | |||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/primitive.rst | 19 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 43 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 53 |
10 files changed, 99 insertions, 47 deletions
diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png Binary files differnew file mode 100644 index 0000000000..62bd9cccd0 --- /dev/null +++ b/doc/sphinx/_static/diffs-show-proof.png diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index ba5bac6489..b3a33ffeea 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -283,14 +283,19 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. 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. + This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. + Additional support is provided by the following modules: + + + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`. + + For comparison operators (e.g., :g:`Z.compare`), require the module :g:`ZifyComparison`. + + For native 63 bit integers, require the module :g:`ZifyInt63`. + :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are respectively run in the first and the last steps of :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``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 479fa674f5..cda8a1b679 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -387,8 +387,8 @@ The syntax for adding a new ring is interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` if not a constant coefficient (i.e. |L_tac| is the inverse function of - ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` - and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic + ``Cp_phi``). See files ``plugins/ring/ZArithRing.v`` + and ``plugins/ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. :n:`sign @one_term` @@ -396,7 +396,7 @@ The syntax for adding a new ring is outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See - ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. + ``plugins/ring/InitialRing.v`` for examples of sign function. :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with @@ -405,7 +405,7 @@ The syntax for adding a new ring is euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See - ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + ``plugins/ring/InitialRing.v`` for examples of div function. :n:`closed [ {+ @qualid } ]` to be documented @@ -538,7 +538,7 @@ Dealing with fields The tactic must be loaded by ``Require Import Field``. New field structures can be declared to the system with the ``Add Field`` command (see below). The field of real numbers is defined in module ``RealField`` - (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so + (in ``plugins/ring``). It is exported by module ``Rbase``, so that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on real numbers. Rational numbers in canonical form are also declared as a field in the module ``Qcanon``. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index fe10e345cd..41e1c30f0d 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -138,7 +138,7 @@ has type :n:`@type`. | {| Variable | Variables } assumpt ::= {+ @ident_decl } @of_type ident_decl ::= @ident {? @univ_decl } - of_type ::= {| : | :> | :>> } @type + of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4cdfba146a..39b154de8d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -13,7 +13,7 @@ Inductive types .. prodn:: inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } - | {? @ident } %{ {*; @record_field } %} + | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } This command defines one or more diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 727177b23a..48647deeff 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -133,7 +133,7 @@ follows: Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. -The complete set of such operators can be obtained looking at the :g:`PArray` module. +The rest of these operators can be found in the :g:`PArray` module. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command. @@ -150,7 +150,16 @@ extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq (see ``kernel/parray.ml``). -Primitive arrays expose a functional interface, but they are internally -implemented using a persistent data structure :cite:`ConchonFilliatre07wml`. -Update and access to an element in the most recent copy of an array are -constant time operations. +Coq's primitive arrays are persistent data structures. Semantically, a set operation +``t.[i <- a]`` represents a new array that has the same values as ``t``, except +at position ``i`` where its value is ``a``. The array ``t`` still exists, can +still be used and its values were not modified. Operationally, the implementation +of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not +copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`. +In short, the implementation keeps one version of ``t`` as an OCaml native array and +other versions as lists of modifications to ``t``. Accesses to the native array +version are constant time operations. However, accesses to versions where all the cells of +the array are modified have O(n) access time, the same as a list. The version that is kept as the native array +changes dynamically upon each get and set call: the current list of modifications +is applied to the native array and the lists of modifications of the other versions +are updated so that they still represent the same values. diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index cd44d06e67..b2099b8636 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term - term_record ::= %{%| {* @field_def } %|%} + term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f90ebadb3a..edd93f2266 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -590,11 +590,11 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. - Experimental: Specifying “Diffs” highlights the difference between the + Specifying “Diffs” highlights the difference between the current and previous proof step. By default, the command shows the output once with additions highlighted. Including “removed” shows the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -675,12 +675,9 @@ Requesting information Showing differences between proof steps --------------------------------------- - Coq can automatically highlight the differences between successive proof steps -and between values in some error messages. Also, as an experimental feature, -Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` -command, but only, for now, when using coqtop and Proof General. - +and between values in some error messages. Coq can also highlight differences +in the proof term. For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added @@ -826,14 +823,37 @@ the split because it has not changed. .. image:: ../_static/diffs-coqide-multigoal.png :alt: coqide with Set Diffs on with multiple goals -This is how diffs may appear after applying a :tacn:`intro` tactic that results -in compacted hypotheses: +Diffs may appear like this after applying a :tacn:`intro` tactic that results +in a compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png :alt: coqide with Set Diffs on with compacted hypotheses +.. _showing_proof_diffs: + +"Show Proof" differences +```````````````````````` + +To show differences in the proof term: + +- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. + +- In CoqIDE, position the cursor on or just after a tactic to compare the proof term + after the tactic with the proof term before the tactic, then select + `View / Show Proof` from the menu or enter the associated key binding. + Differences will be shown applying the current `Show Diffs` setting + from the `View` menu. If the current setting is `Don't show diffs`, diffs + will not be shown. + + Output with the "added and removed" option looks like this: + + .. + + .. image:: ../_static/diffs-show-proof.png + :alt: coqide with Set Diffs on with compacted hypotheses + Controlling the effect of proof editing commands ------------------------------------------------ @@ -858,6 +878,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e276a0edcb..4b1f312105 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4726,7 +4726,7 @@ Automating .. seealso:: - File plugins/setoid_ring/RealField.v for an example of instantiation, + File plugins/ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field. Non-logical tactics diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6ba53b581b..d6db305300 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -57,15 +57,14 @@ to represent :g:`(and A B)`: Notations must be in double quotes, except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`. The notation consists of *tokens* separated by -spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters* +spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters* of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as ``/\``) are the *symbols*. -Substrings enclosed in single quotes are treated as literals. This is necessary -for substrings that would otherwise be interpreted as :n:`@ident`\s. Similarly, -every symbol of at least 3 characters and starting with a simple quote -must be quoted (then it starts by two single quotes). Here is an -example. +Identifiers enclosed in single quotes are treated as symbols and thus +lose their role of parameters. In the same vein, every symbol of at +least 3 characters and starting with a simple quote must be quoted +(then it starts with two single quotes). Here is an example. .. coqtop:: in @@ -82,7 +81,8 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments <ImplicitArguments>` and other notations are resolved at the - time of the declaration of the notation. + time of the declaration of the notation. The right-hand side is + currently typed only at use time but this may change in the future. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. -.. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s - in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be - used to declare that a notation should only be used for printing and - should not declare a parsing rule. In particular, such notations do - not modify the parser. +.. note:: + + The default for a notation is to be used both for parsing and + printing. It is possible to declare a notation only for parsing by + adding the option ``only parsing`` to the list of + :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the + ``only printing`` :n:`@syntax_modifier` can be used to declare that + a notation should only be used for printing. + + If a notation to be used both for parsing and printing is + overriden, both the parsing and printing are invalided, even if the + overriding rule is only parsing. + + If a given notation string occurs only in ``only printing`` rules, + the parser is not modified at all. + + To a given notation string and scope can be attached at most one + notation with both parsing and printing or with only + parsing. Contrastingly, an arbitrary number of ``only printing`` + notations differing in their right-hand sides but only a unique + right-hand side can be attached to a given string and + scope. Obviously, expressions printed by means of such extra + printing rules will not be reparsed to the same form. The Infix command ~~~~~~~~~~~~~~~~~~ @@ -429,10 +446,6 @@ Displaying information about notations productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` and `tactic_then_gen` which are not shown and can't be printed. - The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify - what part of the grammar a nonterminal is from. If you examine nonterminal definitions - in the source code, they are identified only by the name following the colon. - Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the source code, edits it and inserts it into the documentation files. While the @@ -467,11 +480,11 @@ Displaying information about notations `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic:tactic_expr is + Entry tactic_expr is [ "5" RIGHTA - [ tactic:binder_tactic ] + [ binder_tactic ] | "4" LEFTA - [ SELF; ";"; tactic:binder_tactic + [ SELF; ";"; binder_tactic | SELF; ";"; SELF | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA |
