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/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 2 | ||||
| -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/user-extensions/syntax-extensions.rst | 43 |
7 files changed, 76 insertions, 29 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/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/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/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5148fa84c9..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 ~~~~~~~~~~~~~~~~~~ |
