diff options
Diffstat (limited to 'doc')
40 files changed, 3416 insertions, 3053 deletions
diff --git a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst deleted file mode 100644 index 1bf62de3fd..0000000000 --- a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** Incompleteness of conversion checking on problems - involving :ref:`eta-expansion` and :ref:`cumulative universe - polymorphic inductive types <cumulative>` (`#12738 - <https://github.com/coq/coq/pull/12738>`_, fixes `#7015 - <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst new file mode 100644 index 0000000000..e9b02aed6d --- /dev/null +++ b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst @@ -0,0 +1,4 @@ +- **Changed:** + Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) + (`#12099 <https://github.com/coq/coq/pull/12099>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst new file mode 100644 index 0000000000..5ea37e7494 --- /dev/null +++ b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst @@ -0,0 +1,19 @@ +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. +- **Added:** + :ref:`Number Notation <number-notations>` and :ref:`String Notation + <string-notations>` commands now + support parameterized inductive and non inductive types + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst deleted file mode 100644 index 95a9093272..0000000000 --- a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Undetected collision between a lonely notation and a notation in - scope at printing time - (`#12946 <https://github.com/coq/coq/pull/12946>`_, - fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst b/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst deleted file mode 100644 index 42b62eed75..0000000000 --- a/doc/changelog/03-notations/13026-master+fix-printing-custom-no-level-8.2.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Fixing printing of notations in custom entries with - variables not mentioning an explicit level - (`#13026 <https://github.com/coq/coq/pull/13026>`_, - fixes `#12775 <https://github.com/coq/coq/issues/12775>`_ - and `#13018 <https://github.com/coq/coq/issues/13018>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst b/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst deleted file mode 100644 index 50aa4a9052..0000000000 --- a/doc/changelog/03-notations/13067-master+fix-display-parentheses-default-coqide.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Repairing option :g:`Display parentheses` in CoqIDE - (`#12794 <https://github.com/coq/coq/pull/12794>`_ and `#13067 <https://github.com/coq/coq/pull/13067>`_, - fixes `#12793 <https://github.com/coq/coq/issues/12793>`_, - by Jean-Christophe Léchenet and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst deleted file mode 100644 index 289d17167d..0000000000 --- a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Anomaly with :tacn:`injection` involving artificial - dependencies disappearing by reduction - (`#12816 <https://github.com/coq/coq/pull/12816>`_, - fixes `#12787 <https://github.com/coq/coq/issues/12787>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst deleted file mode 100644 index b444a2f436..0000000000 --- a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - :tacn:`replace` and :tacn:`inversion` support registration of a - :g:`core.identity`-like equality in :g:`Type`, such as HoTT's :g:`path` - (`#12847 <https://github.com/coq/coq/pull/12847>`_, - partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_, - by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst new file mode 100644 index 0000000000..d105561a23 --- /dev/null +++ b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst @@ -0,0 +1,5 @@ +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 <https://github.com/coq/coq/pull/13232>`_, + fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst deleted file mode 100644 index 1eb8ef5a2a..0000000000 --- a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Miscellaneous issues with locating tactic errors - (`#13247 <https://github.com/coq/coq/pull/13247>`_, - fixes `#12773 <https://github.com/coq/coq/issues/12773>`_ - and `#12992 <https://github.com/coq/coq/issues/12992>`_, - by Hugo Herbelin). diff --git a/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst b/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst deleted file mode 100644 index 4350fd0238..0000000000 --- a/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - Regression in error reporting after :tacn:`case <case (ssreflect)>`. - A generic error message "Could not fill dependent hole in apply" was - reported for any error following :tacn:`case <case (ssreflect)>` or - :tacn:`elim <elim (ssreflect)>` - (`#12857 <https://github.com/coq/coq/pull/12857>`_, - fixes `#12837 <https://github.com/coq/coq/issues/12837>`_, - by Enrico Tassi). diff --git a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst deleted file mode 100644 index a05829b720..0000000000 --- a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Special symbols now escaped in the index produced by coqdoc, - avoiding collision with the syntax of the output format - (`#12754 <https://github.com/coq/coq/pull/12754>`_, - fixes `#12752 <https://github.com/coq/coq/issues/12752>`_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst deleted file mode 100644 index 67ee061285..0000000000 --- a/doc/changelog/08-tools/12772-fix-details.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - The `details` environment added in the 8.12 release can now be used - as advertised in the reference manual - (`#12772 <https://github.com/coq/coq/pull/12772>`_, - by Thomas Letan). diff --git a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst b/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst deleted file mode 100644 index 75b1e26248..0000000000 --- a/doc/changelog/08-tools/13063-fix-no-output-sync-make-file.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Targets such as ``print-pretty-timed`` in ``coq_makefile``-made - ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not - passed to make and the timing output gets interleaved in just the wrong way - (`#13063 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062 - <https://github.com/coq/coq/issues/13062>`_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst deleted file mode 100644 index c754826e62..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``make approve-output`` in the test-suite now correctly handles - ``output-coqtop`` and ``output-coqchk`` tests (`#12864 - <https://github.com/coq/coq/pull/12864>`_, fixes `#12863 - <https://github.com/coq/coq/issues/12863>`_, by Jason Gross). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst deleted file mode 100644 index 855aa360f1..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Coq is now tested against OCaml 4.11.1 - (`#12972 <https://github.com/coq/coq/pull/12972>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst deleted file mode 100644 index d17a2dff6b..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - The reference manual can now build with Sphinx 3 - (`#13011 <https://github.com/coq/coq/pull/13011>`_, - fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, - by Théo Zimmermann and Jim Fehrle). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 0942a82d6f..2c7b637a42 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -1,6 +1,6 @@ .. _micromega: -Micromega: tactics for solving arithmetic goals over ordered rings +Micromega: solvers for arithmetic goals over ordered rings ================================================================== :Authors: Frédéric Besson and Evgeny Makarov diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 85e0cb9536..7a2be3dcef 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,6 +1,6 @@ .. _nsatz_chapter: -Nsatz: tactics for proving equalities in integral domains +Nsatz: a solver for equalities in integral domains =========================================================== :Author: Loïc Pottier diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 35f087d47d..5c08bc44df 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -1,6 +1,6 @@ .. _omega_chapter: -Omega: a solver for quantifier-free problems in Presburger Arithmetic +Omega: a (deprecated) solver for arithmetic ===================================================================== :Author: Pierre Crégut diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index da1a393b4a..027db9f47a 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -10,8 +10,8 @@ .. _theringandfieldtacticfamilies: -The ring and field tactic families -==================================== +ring and field: solvers for polynomial and rational equations +============================================================= :Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5bc229954f..79f00a4a5a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -1141,9 +1141,6 @@ Infrastructure and dependencies Changes in 8.12.0 ~~~~~~~~~~~~~~~~~~~~~ -.. contents:: - :local: - **Notations** - **Added:** @@ -1216,6 +1213,116 @@ Changes in 8.12.0 modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_, fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross). +Changes in 8.12.1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Fixed:** Incompleteness of conversion checking on problems + involving :ref:`eta-expansion` and :ref:`cumulative universe + polymorphic inductive types <cumulative>` (`#12738 + <https://github.com/coq/coq/pull/12738>`_, fixes `#7015 + <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert). + +**Notations** + +- **Fixed:** + Undetected collision between a lonely notation and a notation in + scope at printing time + (`#12946 <https://github.com/coq/coq/pull/12946>`_, + fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). +- **Fixed:** + Printing of notations in custom entries with + variables not mentioning an explicit level + (`#13026 <https://github.com/coq/coq/pull/13026>`_, + fixes `#12775 <https://github.com/coq/coq/issues/12775>`_ + and `#13018 <https://github.com/coq/coq/issues/13018>`_, + by Hugo Herbelin). + +**Tactics** + +- **Added:** + :tacn:`replace` and :tacn:`inversion` support registration of a + :g:`core.identity`\-like equality in :g:`Type`, such as HoTT's :g:`path` + (`#12847 <https://github.com/coq/coq/pull/12847>`_, + partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_, + by Hugo Herbelin). +- **Fixed:** + Anomaly with :tacn:`injection` involving artificial + dependencies disappearing by reduction + (`#12816 <https://github.com/coq/coq/pull/12816>`_, + fixes `#12787 <https://github.com/coq/coq/issues/12787>`_, + by Hugo Herbelin). + +**Tactic language** + +- **Fixed:** + Miscellaneous issues with locating tactic errors + (`#13247 <https://github.com/coq/coq/pull/13247>`_, + fixes `#12773 <https://github.com/coq/coq/issues/12773>`_ + and `#12992 <https://github.com/coq/coq/issues/12992>`_, + by Hugo Herbelin). + +**SSReflect** + +- **Fixed:** + Regression in error reporting after :tacn:`case <case (ssreflect)>`. + A generic error message "Could not fill dependent hole in apply" was + reported for any error following :tacn:`case <case (ssreflect)>` or + :tacn:`elim <elim (ssreflect)>` + (`#12857 <https://github.com/coq/coq/pull/12857>`_, + fixes `#12837 <https://github.com/coq/coq/issues/12837>`_, + by Enrico Tassi). + +**Commands and options** + +- **Fixed:** + Failures of :cmd:`Search` in the presence of primitive projections + (`#13301 <https://github.com/coq/coq/pull/13301>`_, + fixes `#13298 <https://github.com/coq/coq/issues/13298>`_, + by Hugo Herbelin). + +**Tools** + +- **Fixed:** + Special symbols now escaped in the index produced by coqdoc, + avoiding collision with the syntax of the output format + (`#12754 <https://github.com/coq/coq/pull/12754>`_, + fixes `#12752 <https://github.com/coq/coq/issues/12752>`_, + by Hugo Herbelin). +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 <https://github.com/coq/coq/pull/12772>`_, + by Thomas Letan). +- **Fixed:** + Targets such as ``print-pretty-timed`` in ``coq_makefile``\-made + ``Makefile``\s no longer error in rare cases where ``--output-sync`` is not + passed to make and the timing output gets interleaved in just the wrong way + (`#13063 <https://github.com/coq/coq/pull/13063>`_, fixes `#13062 + <https://github.com/coq/coq/issues/13062>`_, by Jason Gross). + +**CoqIDE** + +- **Fixed:** + View menu "Display parentheses" + (`#12794 <https://github.com/coq/coq/pull/12794>`_ and `#13067 <https://github.com/coq/coq/pull/13067>`_, + fixes `#12793 <https://github.com/coq/coq/issues/12793>`_, + by Jean-Christophe Léchenet and Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Added:** + Coq is now tested against OCaml 4.11.1 + (`#12972 <https://github.com/coq/coq/pull/12972>`_, + by Emilio Jesus Gallego Arias). +- **Fixed:** + The reference manual can now build with Sphinx 3 + (`#13011 <https://github.com/coq/coq/pull/13011>`_, + fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, + by Théo Zimmermann and Jim Fehrle). + Version 8.11 ------------ diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 29a2b40162..dfa2aaf8ff 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -113,7 +113,7 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part - and exponent, optionally preceded by a minus sign. Hexadecimal numerals + and exponent, optionally preceded by a minus sign. Hexadecimal numbers start with ``0x`` or ``0X``. :n:`@bigint` are integers; numbers without fractional nor exponent parts. :n:`@bignat` are non-negative integers. Underscores embedded in the digits are ignored, for example diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 64fc1133f0..41f376c43d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -38,7 +38,6 @@ Current limitations include: - Printing functions are limited and awkward to use. Only a few data types are printable. - Deep pattern matching and matching on tuples don't work. - - If statements on Ltac2 boolean values - A convenient way to build terms with casts through the low-level API. Because the cast type is opaque, building terms with casts currently requires an awkward construction like the following, which also incurs extra overhead to repeat typechecking for each @@ -345,12 +344,10 @@ Ltac2 Definitions .. coqtop:: all - Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. - Ltac2 Set f := fun b => - match b with true => 1 | _ => f true end. + Ltac2 mutable rec f b := if b then 0 else f true. + Ltac2 Set f := fun b => if b then 1 else f true. Ltac2 Eval (f false). - Ltac2 Set f as oldf := fun b => - match b with true => 2 | _ => oldf false end. + Ltac2 Set f as oldf := fun b => if b then 2 else oldf false. Ltac2 Eval (f false). In the definition, the `f` in the body is resolved statically @@ -1149,6 +1146,13 @@ Match on values | @tac2pat1 , {*, @tac2pat1 } | @tac2pat1 +.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else + :name: if-then-else (Ltac2) + + Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value. If the + :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then` + is evaluated. Otherwise :n:`@ltac2_expr5__else` is evaluated. + .. note:: For now, deep pattern matching is not implemented. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f4aef8f879..7f5aacbfdb 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,927 +1,5 @@ -.. _proofhandling: +:orphan: -------------------- - Proof handling -------------------- +.. raw:: html -In |Coq|’s proof editing mode all top-level commands documented in -Chapter :ref:`vernacularcommands` remain available and the user has access to specialized -commands dealing with proof development pragmas documented in this -section. They can also use some other specialized commands called -*tactics*. They are the very tools allowing the user to deal with -logical reasoning. They are documented in Chapter :ref:`tactics`. - -|Coq| user interfaces usually have a way of marking whether the user has -switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into -:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. - -At each stage of a proof development, one has a list of goals to -prove. Initially, the list consists only in the theorem itself. After -having applied some tactics, the list of goals contains the subgoals -generated by the tactics. - -To each subgoal is associated a number of hypotheses called the *local context* -of the goal. Initially, the local context contains the local variables and -hypotheses of the current section (see Section :ref:`gallina-assumptions`) and -the local variables and hypotheses of the theorem statement. It is enriched by -the use of certain tactics (see e.g. :tacn:`intro`). - -When a proof is completed, the message ``Proof completed`` is displayed. -One can then register this proof as a defined constant in the -environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those -terms are called *proof terms*. - - -.. exn:: No focused proof. - - |Coq| raises this error message when one attempts to use a proof editing command - out of the proof editing mode. - -.. _proof-editing-mode: - -Entering and leaving proof editing mode ---------------------------------------- - -The proof editing mode is entered by asserting a statement, which typically is -the assertion of a theorem using an assertion command like :cmd:`Theorem`. The -list of assertion commands is given in :ref:`Assertions`. The command -:cmd:`Goal` can also be used. - -.. cmd:: Goal @type - - This is intended for quick assertion of statements, without knowing in - advance which name to give to the assertion, typically for quick - testing of the provability of a statement. If the proof of the - statement is eventually completed and validated, the statement is then - bound to the name ``Unnamed_thm`` (or a variant of this name not already - used for another statement). - -.. cmd:: Qed - - This command is available in interactive editing proof mode when the - proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to |Coq| top-level and attaches the extracted - proof term to the declared name of the original goal. The name is - added to the environment as an opaque constant. - - .. exn:: Attempt to save an incomplete proof. - :undocumented: - - .. note:: - - Sometimes an error occurs when building the proof term, because - tactics do not enforce completely the term construction - constraints. - - The user should also be aware of the fact that since the - proof term is completely rechecked at this point, one may have to wait - a while when the proof is large. In some exceptional cases one may - even incur a memory overflow. - -.. cmd:: Save @ident - :name: Save - - Saves a completed proof with the name :token:`ident`, which - overrides any name provided by the :cmd:`Theorem` command or - its variants. - -.. cmd:: Defined {? @ident } - - Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means - that its content can be explicitly used for type checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). If :token:`ident` is specified, - the proof is defined with the given name, which overrides any name - provided by the :cmd:`Theorem` command or its variants. - -.. cmd:: Admitted - - This command is available in interactive editing mode to give up - the current proof and declare the initial goal as an axiom. - -.. cmd:: Abort {? {| All | @ident } } - - Cancels the current proof development, switching back to - the previous proof development, or to the |Coq| toplevel if no other - proof was being edited. - - :n:`@ident` - Aborts editing the proof named :n:`@ident` for use when you have - nested proofs. See also :flag:`Nested Proofs Allowed`. - - :n:`All` - Aborts all current proofs. - - .. exn:: No focused proof (No proof-editing in progress). - :undocumented: - -.. cmd:: Proof @term - :name: Proof `term` - - This command applies in proof editing mode. It is equivalent to - :n:`exact @term. Qed.` - That is, you have to give the full proof in one gulp, as a - proof term (see Section :ref:`applyingtheorems`). - - .. warning:: - - Use of this command is discouraged. In particular, it - doesn't work in Proof General because it must - immediately follow the command that opened proof mode, but - Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see - `Proof General issue #498 - <https://github.com/ProofGeneral/PG/issues/498>`_). - -.. cmd:: Proof - - Is a no-op which is useful to delimit the sequence of tactic commands - which start a proof, after a :cmd:`Theorem` command. It is a good practice to - use :cmd:`Proof` as an opening parenthesis, closed in the script with a - closing :cmd:`Qed`. - - .. seealso:: :cmd:`Proof with` - -.. cmd:: Proof using @section_var_expr {? with @ltac_expr } - - .. insertprodn section_var_expr starred_ident_ref - - .. prodn:: - section_var_expr ::= {* @starred_ident_ref } - | {? - } @section_var_expr50 - section_var_expr50 ::= @section_var_expr0 - @section_var_expr0 - | @section_var_expr0 + @section_var_expr0 - | @section_var_expr0 - section_var_expr0 ::= @starred_ident_ref - | ( @section_var_expr ) {? * } - starred_ident_ref ::= @ident {? * } - | Type {? * } - | All - - Opens proof editing mode, declaring the set of - section variables (see :ref:`gallina-assumptions`) used by the proof. - At :cmd:`Qed` time, the - system verifies that the set of section variables used in - the proof is a subset of the declared one. - - The set of declared variables is closed under type dependency. For - example, if ``T`` is a variable and ``a`` is a variable of type - ``T``, then the commands ``Proof using a`` and ``Proof using T a`` - are equivalent. - - The set of declared variables always includes the variables used by - the statement. In other words ``Proof using e`` is equivalent to - ``Proof using Type + e`` for any declaration expression ``e``. - - :n:`- @section_var_expr50` - Use all section variables except those specified by :n:`@section_var_expr50` - - :n:`@section_var_expr0 + @section_var_expr0` - Use section variables from the union of both collections. - See :ref:`nameaset` to see how to form a named collection. - - :n:`@section_var_expr0 - @section_var_expr0` - Use section variables which are in the first collection but not in the - second one. - - :n:`{? * }` - Use the transitive closure of the specified collection. - - :n:`Type` - Use only section variables occurring in the statement. Specifying :n:`*` - uses the forward transitive closure of all the section variables occurring - in the statement. For example, if the variable ``H`` has type ``p < 5`` then - ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``. - - :n:`All` - Use all section variables. - - .. seealso:: :ref:`tactics-implicit-automation` - -.. attr:: using - - This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`, - :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and - its variants. It takes - a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to - specifying the same :n:`@section_var_expr` in - :cmd:`Proof using`. - - .. example:: - - .. coqtop:: all - - Section Test. - Variable n : nat. - Hypothesis Hn : n <> 0. - - #[using="Hn"] - Lemma example : 0 < n. - - .. coqtop:: in - - Abort. - End Test. - - -Proof using options -``````````````````` - -The following options modify the behavior of ``Proof using``. - - -.. opt:: Default Proof Using "@section_var_expr" - :name: Default Proof Using - - Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default - Proof Using "a b"`` will complete all ``Proof`` commands not followed by a - ``using`` part with ``using a b``. - - -.. flag:: Suggest Proof Using - - When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not - provide one. - -.. _`nameaset`: - -Name a set of section hypotheses for ``Proof using`` -```````````````````````````````````````````````````` - -.. cmd:: Collection @ident := @section_var_expr - - This can be used to name a set of section - hypotheses, with the purpose of making ``Proof using`` annotations more - compact. - - .. example:: - - Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: - - Collection Some := x y z. - - Define the collection named ``Fewer`` containing only ``x`` and ``y``:: - - Collection Fewer := Some - z - - Define the collection named ``Many`` containing the set union or set - difference of ``Fewer`` and ``Some``:: - - Collection Many := Fewer + Some - Collection Many := Fewer - Some - - Define the collection named ``Many`` containing the set difference of - ``Fewer`` and the unnamed collection ``x y``:: - - Collection Many := Fewer - (x y) - - - -.. cmd:: Existential @natural {? : @type } := @term - - This command instantiates an existential variable. :token:`natural` is an index in - the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. - - This command is intended to be used to instantiate existential - variables when the proof is completed but some uninstantiated - existential variables remain. To instantiate existential variables - during proof edition, you should use the tactic :tacn:`instantiate`. - -.. cmd:: Grab Existential Variables - - This command can be run when a proof has no more goal to be solved but - has remaining uninstantiated existential variables. It takes every - uninstantiated existential variable and turns it into a goal. - -Proof modes -``````````` - -When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, -|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes -shipped in the standard |Coq| installation, and furthermore some plugins define -their own proof modes. The default proof mode used when opening a proof can -be changed using the following option. - -.. opt:: Default Proof Mode @string - - Select the proof mode to use when starting a proof. Depending on the proof - mode, various syntactic constructs are allowed when writing an interactive - proof. All proof modes support vernacular commands; the proof mode determines - which tactic language and set of tactic definitions are available. The - possible option values are: - - `"Classic"` - Activates the |Ltac| language and the tactics with the syntax documented - in this manual. - Some tactics are not available until the associated plugin is loaded, - such as `SSR` or `micromega`. - This proof mode is set when the :term:`prelude` is loaded. - - `"Noedit"` - No tactic - language is activated at all. This is the default when the :term:`prelude` - is not loaded, e.g. through the `-noinit` option for `coqc`. - - `"Ltac2"` - Activates the Ltac2 language and the Ltac2-specific variants of the documented - tactics. - This value is only available after :cmd:`Requiring <Require>` Ltac2. - :cmd:`Importing <Import>` Ltac2 sets this mode. - - Some external plugins also define their own proof mode, which can be - activated with this command. - -Navigation in the proof tree --------------------------------- - -.. cmd:: Undo {? {? To } @natural } - - Cancels the effect of the last :token:`natural` commands or tactics. - The :n:`To @natural` form goes back to the specified state number. - If :token:`natural` is not specified, the command goes back one command or tactic. - -.. cmd:: Restart - - Restores the proof editing process to the original goal. - - .. exn:: No focused proof to restart. - :undocumented: - -.. cmd:: Focus {? @natural } - - Focuses the attention on the first subgoal to prove or, if :token:`natural` is - specified, the :token:`natural`\-th. The - printing of the other subgoals is suspended until the focused subgoal - is solved or unfocused. - - .. deprecated:: 8.8 - - Prefer the use of bullets or focusing brackets with a goal selector (see below). - -.. cmd:: Unfocus - - This command restores to focus the goal that were suspended by the - last :cmd:`Focus` command. - - .. deprecated:: 8.8 - -.. cmd:: Unfocused - - Succeeds if the proof is fully unfocused, fails if there are some - goals out of focus. - -.. _curly-braces: - -.. index:: { - } - -.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, - hence the verbose names - -.. tacn:: {? {| @natural | [ @ident ] } : } %{ - %} - - .. todo - See https://github.com/coq/coq/issues/12004 and - https://github.com/coq/coq/issues/12825. - - ``{`` (without a terminating period) focuses on the first - goal. The subproof can only be - unfocused when it has been fully solved (*i.e.*, when there is no - focused goal left). Unfocusing is then handled by ``}`` (again, without a - terminating period). See also an example in the next section. - - Note that when a focused goal is proved a message is displayed - together with a suggestion about the right bullet or ``}`` to unfocus it - or focus the next one. - - :n:`@natural:` - Focuses on the :token:`natural`\-th subgoal to prove. - - :n:`[ @ident ]: %{` - Focuses on the named goal :token:`ident`. - - .. note:: - - Goals are just existential variables and existential variables do not - get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. - You may also wrap this in an Ltac-definition like: - - .. coqtop:: in - - Ltac name_goal name := refine ?[name]. - - .. seealso:: :ref:`existential-variables` - - .. example:: - - This first example uses the Ltac definition above, and the named goals - only serve for documentation. - - .. coqtop:: all - - Goal forall n, n + 0 = n. - Proof. - induction n; [ name_goal base | name_goal step ]. - [base]: { - - .. coqtop:: all - - reflexivity. - - .. coqtop:: in - - } - - .. coqtop:: all - - [step]: { - - .. coqtop:: all - - simpl. - f_equal. - assumption. - } - Qed. - - This can also be a way of focusing on a shelved goal, for instance: - - .. coqtop:: all - - Goal exists n : nat, n = n. - eexists ?[x]. - reflexivity. - [x]: exact 0. - Qed. - - .. exn:: This proof is focused, but cannot be unfocused this way. - - You are trying to use ``}`` but the current subproof has not been fully solved. - - .. exn:: No such goal (@natural). - :undocumented: - - .. exn:: No such goal (@ident). - :undocumented: - - .. exn:: Brackets do not support multi-goal selectors. - - Brackets are used to focus on a single goal given either by its position - or by its name if it has one. - - .. seealso:: The error messages for bullets below. - -.. _bullets: - -Bullets -``````` - -Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The -use of a bullet ``b`` for the first time focuses on the first goal ``g``, the -same bullet cannot be used again until the proof of ``g`` is completed, -then it is mandatory to focus the next goal with ``b``. The consequence is -that ``g`` and all goals present when ``g`` was focused are focused with the -same bullet ``b``. See the example below. - -Different bullets can be used to nest levels. The scope of bullet does -not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further -nesting levels provided they are delimited by these. Bullets are made of -repeated ``-``, ``+`` or ``*`` symbols: - -.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } - -Note again that when a focused goal is proved a message is displayed -together with a suggestion about the right bullet or ``}`` to unfocus it -or focus the next one. - -.. note:: - - In Proof General (``Emacs`` interface to |Coq|), you must use - bullets with the priority ordering shown above to have a correct - indentation. For example ``-`` must be the outer bullet and ``**`` the inner - one in the example below. - -The following example script illustrates all these features: - -.. example:: - - .. coqtop:: all - - Goal (((True /\ True) /\ True) /\ True) /\ True. - Proof. - split. - - split. - + split. - ** { split. - - trivial. - - trivial. - } - ** trivial. - + trivial. - - assert True. - { trivial. } - assumption. - Qed. - -.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished. - - Before using bullet :n:`@bullet__1` again, you should first finish proving - the current focused goal. - Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same. - -.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here. - - You must put :n:`@bullet__2` to focus on the next goal. No other bullet is - allowed here. - -.. exn:: No such goal. Focus next goal with bullet @bullet. - - You tried to apply a tactic but no goals were under focus. - Using :n:`@bullet` is mandatory here. - -.. FIXME: the :noindex: below works around a Sphinx issue. - (https://github.com/sphinx-doc/sphinx/issues/4979) - It should be removed once that issue is fixed. - -.. exn:: No such goal. Try unfocusing with %}. - :noindex: - - You just finished a goal focused by ``{``, you must unfocus it with ``}``. - -Mandatory Bullets -````````````````` - -Using :opt:`Default Goal Selector` with the ``!`` selector forces -tactic scripts to keep focus to exactly one goal (e.g. using bullets) -or use explicit goal selectors. - -Set Bullet Behavior -``````````````````` -.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } - :name: Bullet Behavior - - This option controls the bullet behavior and can take two possible values: - - - "None": this makes bullets inactive. - - "Strict Subproofs": this makes bullets active (this is the default behavior). - -.. _requestinginformation: - -Requesting information ----------------------- - - -.. cmd:: Show {? {| @ident | @natural } } - - Displays the current goals. - - :n:`@natural` - Display only the :token:`natural`\-th subgoal. - - :n:`@ident` - Displays the named goal :token:`ident`. This is useful in - particular to display a shelved goal but only works if the - corresponding existential variable has been named by the user - (see :ref:`existential-variables`) as in the following example. - - .. example:: - - .. coqtop:: all abort - - Goal exists n, n = 0. - eexists ?[n]. - Show n. - - .. exn:: No focused proof. - :undocumented: - - .. exn:: No such goal. - :undocumented: - -.. cmd:: Show Proof {? Diffs {? removed } } - - Displays the proof term generated by the tactics - that have been applied so far. If the proof is incomplete, the term - will contain holes, which correspond to subterms which are still to be - constructed. Each hole is an existential variable, which appears as a - question mark followed by an identifier. - - 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_proof_diffs`. - -.. cmd:: Show Conjectures - - Prints the names of all the - theorems that are currently being proved. As it is possible to start - proving a previous lemma during the proof of a theorem, there may - be multiple names. - -.. cmd:: Show Intro - - If the current goal begins by at least one product, - prints the name of the first product as it would be - generated by an anonymous :tacn:`intro`. The aim of this command is to ease - the writing of more robust scripts. For example, with an appropriate - Proof General macro, it is possible to transform any anonymous :tacn:`intro` - into a qualified one such as ``intro y13``. In the case of a non-product - goal, it prints nothing. - -.. cmd:: Show Intros - - Similar to the previous command. - Simulates the naming process of :tacn:`intros`. - -.. cmd:: Show Existentials - - Displays all open goals / existential variables in the current proof - along with the type and the context of each variable. - -.. cmd:: Show Match @qualid - - Displays a template of the Gallina :token:`match<term_match>` - construct with a branch for each constructor of the type - :token:`qualid`. This is used internally by - `company-coq <https://github.com/cpitclaudel/company-coq>`_. - - .. example:: - - .. coqtop:: all - - Show Match nat. - - .. exn:: Unknown inductive type. - :undocumented: - -.. cmd:: Show Universes - - Displays the set of all universe constraints and - its normalized form at the current stage of the proof, useful for - debugging universe inconsistencies. - -.. cmd:: Show Goal @natural at @natural - - Available in coqtop. Displays a goal at a - proof state using the goal ID number and the proof state ID number. - It is primarily for use by tools such as Prooftree that need to fetch - goal history in this way. Prooftree is a tool for visualizing a proof - as a tree that runs in Proof General. - -.. cmd:: Guarded - - Some tactics (e.g. :tacn:`refine`) allow to build proofs using - fixpoint or co-fixpoint constructions. Due to the incremental nature - of interactive proof construction, the check of the termination (or - guardedness) of the recursive calls in the fixpoint or cofixpoint - constructions is postponed to the time of the completion of the proof. - - The command :cmd:`Guarded` allows checking if the guard condition for - fixpoint and cofixpoint is violated at some time of the construction - of the proof without having to wait the completion of the proof. - -.. _showing_diffs: - -Showing differences between proof steps ---------------------------------------- - -|Coq| can automatically highlight the differences between successive proof steps -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 -to it. The second screenshot uses the "removed" option, so it shows the conclusion a -second time with the old text, with deletions marked in red. Also, since the hypotheses are -new, no line of old text is shown for them. - -.. comment screenshot produced with: - Inductive ev : nat -> Prop := - | ev_0 : ev 0 - | ev_SS : forall n : nat, ev n -> ev (S (S n)). - - Fixpoint double (n:nat) := - match n with - | O => O - | S n' => S (S (double n')) - end. - - Goal forall n, ev n -> exists k, n = double k. - intros n E. - -.. - - .. image:: ../_static/diffs-coqide-on.png - :alt: |CoqIDE| with Set Diffs on - -.. - - .. image:: ../_static/diffs-coqide-removed.png - :alt: |CoqIDE| with Set Diffs removed - -.. - - .. image:: ../_static/diffs-coqtop-on3.png - :alt: coqtop with Set Diffs on - -This image shows an error message with diff highlighting in |CoqIDE|: - -.. - - .. image:: ../_static/diffs-error-message.png - :alt: |CoqIDE| error message with diffs - -How to enable diffs -``````````````````` - -.. opt:: Diffs {| "on" | "off" | "removed" } - :name: Diffs - - The “on” setting highlights added tokens in green, while the “removed” setting - additionally reprints items with removed tokens in red. Unchanged tokens in - modified items are shown with pale green or red. Diffs in error messages - use red and green for the compared values; they appear regardless of the setting. - (Colors are user-configurable.) - -For coqtop, showing diffs can be enabled when starting coqtop with the -``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option -within |Coq|. You will need to provide the ``-color on|auto`` command-line option when -you start coqtop in either case. - -Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment -variable. See section :ref:`customization-by-environment-variables`. Diffs -use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. - -In |CoqIDE|, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` -command in |CoqIDE|. You can change the background colors shown for diffs from the -``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, -``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also -lets you control other attributes of the highlights, such as the foreground -color, bold, italic, underline and strikeout. - -Proof General can also display |Coq|-generated proof diffs automatically. -Please see the PG documentation section -"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) -for details. - -How diffs are calculated -```````````````````````` - -Diffs are calculated as follows: - -1. Select the old proof state to compare to, which is the proof state before - the last tactic that changed the proof. Changes that only affect the view - of the proof, such as ``all: swap 1 2``, are ignored. - -2. For each goal in the new proof state, determine what old goal to compare - it to—the one it is derived from or is the same as. Match the hypotheses by - name (order is ignored), handling compacted items specially. - -3. For each hypothesis and conclusion (the “items”) in each goal, pass - them as strings to the lexer to break them into tokens. Then apply the - Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. - -Notes: - -* Aside from the highlights, output for the "on" option should be identical - to the undiffed output. -* Goals completed in the last proof step will not be shown even with the - "removed" setting. - -.. comment The following screenshots show diffs working with multiple goals and with compacted - hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at - all after the split because it has not changed. - - .. todo: Use this script and remove the screenshots when COQ_COLORS - works for coqtop in sphinx - .. coqtop:: none - - Set Diffs "on". - Parameter P : nat -> Prop. - Goal P 1 /\ P 2 /\ P 3. - - .. coqtop:: out - - split. - - .. coqtop:: all abort - - 2: split. - - .. - - .. coqtop:: none - - Set Diffs "on". - Goal forall n m : nat, n + m = m + n. - Set Diffs "on". - - .. coqtop:: out - - intros n. - - .. coqtop:: all abort - - intros m. - -This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal -with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after -the split because it has not changed. - -.. - - .. image:: ../_static/diffs-coqide-multigoal.png - :alt: coqide with Set Diffs on with multiple goals - -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 ------------------------------------------------- - - -.. opt:: Hyps Limit @natural - :name: Hyps Limit - - This option controls the maximum number of hypotheses displayed in goals - after the application of a tactic. All the hypotheses remain usable - in the proof development. - When unset, it goes back to the default mode which is to print all - available hypotheses. - - -.. flag:: Nested Proofs Allowed - - When turned on (it is off by default), this flag enables support for nested - proofs: a new assertion command can be inserted before the current proof is - finished, in which case |Coq| will temporarily switch to the proof of this - *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` - or :cmd:`Defined`), its statement will be made available (as if it had been - 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 ------------------------- - -.. cmd:: Print Debug GC - - Prints heap usage statistics, which are values from the `stat` type of the `Gc` module - described - `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ - in the |OCaml| documentation. - The `live_words`, `heap_words` and `top_heap_words` values give the basic information. - Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. - -When experiencing high memory usage the following commands can be used -to force |Coq| to optimize some of its internal data structures. - -.. cmd:: Optimize Proof - - Shrink the data structure used to represent the current proof. - - -.. cmd:: Optimize Heap - - Perform a heap compaction. This is generally an expensive operation. - See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ - There is also an analogous tactic :tacn:`optimize_heap`. - -Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` -environment variable. + <meta http-equiv="refresh" content="0;URL=../proofs/writing-proofs/proof-mode.html"> diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fe9a31e220..c665026500 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2663,1760 +2663,6 @@ and an explanation of the underlying technique. simultaneously proved are respectively :g:`forall binder ... binder, type` The identifiers :n:`@ident` are the names of the coinduction hypotheses. -.. _rewritingexpressions: - -Rewriting expressions ---------------------- - -These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in -file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is -simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. - -.. tacn:: rewrite @term - :name: rewrite - - This tactic applies to any goal. The type of :token:`term` must have the form - - ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` - - where :g:`eq` is the Leibniz equality or a registered setoid equality. - - Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, - resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then - replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. - Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, - and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new - subgoals. - - .. exn:: The @term provided does not end with an equation. - :undocumented: - - .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. - :undocumented: - - .. tacv:: rewrite -> @term - - Is equivalent to :n:`rewrite @term` - - .. tacv:: rewrite <- @term - - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left - - .. tacv:: rewrite @term in @goal_occurrences - - Analogous to :n:`rewrite @term` but rewriting is done following - the clause :token:`goal_occurrences`. For instance: - - + :n:`rewrite H in H'` will rewrite `H` in the hypothesis - ``H'`` instead of the current goal. - + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means - :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` - In particular a failure will happen if any of these three simpler tactics - fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses - :g:`H'` different from :g:`H`. - A success will happen as soon as at least one of these simpler tactics succeeds. - + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` - that succeeds if at least one of these two tactics succeeds. - - Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. - - .. tacv:: rewrite @term at @occurrences - - Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. - - .. tacv:: rewrite @term by @tactic - - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. - - .. tacv:: rewrite {+, @orientation @term} {? in @ident } - - Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. An :production:`orientation` - ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. - - In all forms of rewrite described above, a :token:`term` to rewrite can be - immediately prefixed by one of the following modifiers: - - + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many - times as possible (perhaps zero time). This form never fails. - + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. - + `!` : works as `?`, except that at least one rewrite should succeed, otherwise - the tactic fails. - + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, - leading to failure if these :token:`natural` rewrites are not possible. - - .. tacv:: erewrite @term - :name: erewrite - - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. - - .. flag:: Keyed Unification - - Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive - unification. The subterms, considered as rewriting candidates, must start with - the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments - are then unified up to full reduction. - -.. tacn:: replace @term with @term’ - :name: replace - - This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` - as a subgoal. This equality is automatically solved if it occurs among - the assumptions, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. - - .. exn:: Terms do not have convertible types. - :undocumented: - - .. tacv:: replace @term with @term’ by @tactic - - This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated - subgoal :n:`@term = @term’`. - - .. tacv:: replace @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. - - .. tacv:: replace -> @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` - - .. tacv:: replace <- @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` - - .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} - replace -> @term in @goal_occurrences - replace <- @term in @goal_occurrences - - Acts as before but the replacements take place in the specified clauses - (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not - only in the conclusion of the goal. The clause argument must not contain - any ``type of`` nor ``value of``. - -.. tacn:: subst @ident - :name: subst - - This tactic applies to a goal that has :n:`@ident` in its context and (at - least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` - with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by - :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and - clears :n:`@ident` and :g:`H` from the context. - - If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also - unfolded and cleared. - - If :n:`@ident` is a section variable it is expected to have no - indirect occurrences in the goal, i.e. that no global declarations - implicitly depending on the section variable must be present in the - goal. - - .. note:: - + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. - - + If :g:`H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. - - .. tacv:: subst {+ @ident} - - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - - .. tacv:: subst - - This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in - ``t`` and :n:`@ident` not a section variable with indirect - dependencies in the goal. - - .. flag:: Regular Subst Tactic - - This flag controls the behavior of :tacn:`subst`. When it is - activated (it is by default), :tacn:`subst` also deals with the following corner cases: - - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the flag, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or - `t′` respectively. - + The presence of a recursive equation which without the flag would - be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - flag would be a cause of failure of :tacn:`subst`. - - Additionally, it prevents a local definition such as :n:`@ident := t` to be - unfolded which otherwise it would exceptionally unfold in configurations - containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` - with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the flag it may break. - default. - - .. exn:: Cannot find any non-recursive equality over :n:`@ident`. - :undocumented: - - .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. - Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. - - Raised when the variable is a section variable with indirect - dependencies in the goal. - - -.. tacn:: stepl @term - :name: stepl - - This tactic is for chaining rewriting steps. It assumes a goal of the - form :n:`R @term @term` where ``R`` is a binary relation and relies on a - database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` - where `eq` is typically a setoid equality. The application of :n:`stepl @term` - then replaces the goal by :n:`R @term @term` and adds a new goal stating - :n:`eq @term @term`. - - .. cmd:: Declare Left Step @term - - Adds :n:`@term` to the database used by :tacn:`stepl`. - - This tactic is especially useful for parametric setoids which are not accepted - as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see - :ref:`Generalizedrewriting`). - - .. tacv:: stepl @term by @tactic - - This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - - .. tacv:: stepr @term by @tactic - :name: stepr - - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form - :g:`forall x y z, R x y -> eq y z -> R x z`. - - .. cmd:: Declare Right Step @term - - Adds :n:`@term` to the database used by :tacn:`stepr`. - - -.. tacn:: change @term - :name: change - - This tactic applies to any goal. It implements the rule ``Conv`` given in - :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` - with `U` providing that `U` is well-formed and that `T` and `U` are - convertible. - - .. exn:: Not convertible. - :undocumented: - - .. tacv:: change @term with @term’ - - This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. - The term :n:`@term` and :n:`@term’` must be convertible. - - .. tacv:: change @term at {+ @natural} with @term’ - - This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` - in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. - - .. exn:: Too few occurrences. - :undocumented: - - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident - - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. - - .. tacv:: now_show @term - - This is a synonym of :n:`change @term`. It can be used to - make some proof steps explicit when refactoring a proof script - to make it readable. - - .. seealso:: :ref:`Performing computations <performingcomputations>` - -.. _performingcomputations: - -Performing computations ---------------------------- - -.. insertprodn red_expr pattern_occ - -.. prodn:: - red_expr ::= red - | hnf - | simpl {? @delta_flag } {? @ref_or_pattern_occ } - | cbv {? @strategy_flag } - | cbn {? @strategy_flag } - | lazy {? @strategy_flag } - | compute {? @delta_flag } - | vm_compute {? @ref_or_pattern_occ } - | native_compute {? @ref_or_pattern_occ } - | unfold {+, @unfold_occ } - | fold {+ @one_term } - | pattern {+, @pattern_occ } - | @ident - delta_flag ::= {? - } [ {+ @reference } ] - strategy_flag ::= {+ @red_flag } - | @delta_flag - red_flag ::= beta - | iota - | match - | fix - | cofix - | zeta - | delta {? @delta_flag } - ref_or_pattern_occ ::= @reference {? at @occs_nums } - | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } - int_or_var ::= @integer - | @ident - unfold_occ ::= @reference {? at @occs_nums } - pattern_occ ::= @one_term {? at @occs_nums } - -This set of tactics implements different specialized usages of the -tactic :tacn:`change`. - -All conversion tactics (including :tacn:`change`) can be parameterized by the -parts of the goal where the conversion can occur. This is done using -*goal clauses* which consists in a list of hypotheses and, optionally, -of a reference to the conclusion of the goal. For defined hypothesis -it is possible to specify if the conversion should occur on the type -part, the body part or both (default). - -Goal clauses are written after a conversion tactic (tactics :tacn:`set`, -:tacn:`rewrite`, :tacn:`replace` and :tacn:`autorewrite` also use goal -clauses) and are introduced by the keyword `in`. If no goal clause is -provided, the default is to perform the conversion only in the -conclusion. - -The syntax and description of the various goal clauses is the -following: - -+ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` -+ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the - conclusion -+ :n:`in * |-` in every hypothesis -+ :n:`in *` (equivalent to in :n:`* |- *`) everywhere -+ :n:`in (type of @ident) (value of @ident) ... |-` in type part of - :n:`@ident`, in the value part of :n:`@ident`, etc. - -For backward compatibility, the notation :n:`in {+ @ident}` performs -the conversion in hypotheses :n:`{+ @ident}`. - -.. tacn:: cbv {? @strategy_flag } - lazy {? @strategy_flag } - :name: cbv; lazy - - These parameterized reduction tactics apply to any goal and perform - the normalization of the goal according to the specified flags. In - correspondence with the kinds of reduction considered in |Coq| namely - :math:`\beta` (reduction of functional application), :math:`\delta` - (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), - :math:`\iota` (reduction of - pattern matching over a constructed term, and unfolding of :g:`fix` and - :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the - 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 - 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 - construction inside the :n:`@term` itself (use here the ``zeta`` flag). In - any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). - - Normalization according to the flags is done by first evaluating the - head of the expression into a *weak-head* normal form, i.e. until the - evaluation is blocked by a variable (or an opaque constant, or an - axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or - :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a - :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a - product type, a sort), or is a redex that the flags prevent to reduce. Once a - weak-head normal form is obtained, subterms are recursively reduced using the - same strategy. - - Reduction to weak-head normal form can be done using two strategies: - *lazy* (``lazy`` tactic), or *call-by-value* (``cbv`` tactic). The lazy - strategy is a call-by-need strategy, with sharing of reductions: the - arguments of a function call are weakly evaluated only when necessary, - and if an argument is used several times then it is weakly computed - only once. This reduction is efficient for reducing expressions with - dead code. For instance, the proofs of a proposition :g:`exists x. P(x)` - reduce to a pair of a witness :g:`t`, and a proof that :g:`t` satisfies the - predicate :g:`P`. Most of the time, :g:`t` may be computed without computing - the proof of :g:`P(t)`, thanks to the lazy strategy. - - The call-by-value strategy is the one used in ML languages: the - arguments of a function call are systematically weakly evaluated - first. Despite the lazy strategy always performs fewer reductions than - the call-by-value strategy, the latter is generally more efficient for - evaluating purely computational expressions (i.e. with little dead code). - -.. tacv:: compute - cbv - :name: compute; _ - - These are synonyms for ``cbv beta delta iota zeta``. - -.. tacv:: lazy - - This is a synonym for ``lazy beta delta iota zeta``. - -.. tacv:: compute [ {+ @qualid} ] - cbv [ {+ @qualid} ] - - These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. - -.. tacv:: compute - [ {+ @qualid} ] - cbv - [ {+ @qualid} ] - - These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. - -.. 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`. - -.. tacv:: vm_compute - :name: vm_compute - - 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 - :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. - -.. tacv:: native_compute - :name: native_compute - - 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 :tacn:`vm_compute`. Note however that the - compilation cost is higher, so it is worth using only for intensive - computations. - - .. flag:: NativeCompute Timing - - This flag causes all calls to the native compiler to print - timing information for the conversion to native code, - compilation, execution, and reification phases of native - compilation. Timing is printed in units of seconds of - wall-clock time. - - .. flag:: NativeCompute Profiling - - On Linux, if you have the ``perf`` profiler installed, this flag makes - it possible to profile :tacn:`native_compute` evaluations. - - .. opt:: NativeCompute Profile Filename @string - :name: NativeCompute Profile Filename - - This option specifies the profile output; the default is - ``native_compute_profile.data``. The actual filename used - 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 - :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. - -.. flag:: Debug Cbv - - This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print - information about the constants it encounters and the unfolding decisions it - makes. - -.. tacn:: red - :name: red - - This tactic applies to a goal that has the form:: - - forall (x:T1) ... (xk:Tk), T - - with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a - constant. If :g:`c` is transparent then it replaces :g:`c` with its - definition (say :g:`t`) and then reduces - :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. - -.. exn:: Not reducible. - :undocumented: - -.. exn:: No head constant to reduce. - :undocumented: - -.. tacn:: hnf - :name: hnf - - This tactic applies to any goal. It replaces the current goal with its - head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it - reduces the head of the goal until it becomes a product or an - irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. - The behavior of both :tacn:`hnf` can be tuned using the :cmd:`Arguments` command. - - Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. - -.. note:: - The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` - on transparency and opacity). - -.. tacn:: cbn - simpl - :name: cbn; simpl - - These tactics apply to any goal. They try to reduce a term to - something still readable instead of fully normalizing it. They perform - a sort of strong normalization with two key differences: - - + They unfold a constant if and only if it leads to a :math:`\iota`-reduction, - i.e. reducing a match or unfolding a fixpoint. - + While reducing a constant unfolding to (co)fixpoints, the tactics - use the name of the constant the (co)fixpoint comes from instead of - the (co)fixpoint definition in recursive calls. - - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more - predictable replacement for :tacn:`simpl`. - - 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 :cmd:`Arguments` command. - - .. todo add "See <subsection about controlling the behavior of reduction strategies>" - to TBA section - - Notice that only transparent constants whose name can be reused in the - 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 :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} ] - - 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 - - This applies :tacn:`simpl` only to the subterms matching - :n:`@pattern` in the current goal. - -.. tacv:: simpl @pattern at {+ @natural} - - This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms - matching :n:`@pattern` in the current goal. - - .. exn:: Too few occurrences. - :undocumented: - -.. tacv:: simpl @qualid - simpl @string - - This applies :tacn:`simpl` only to the applicative subterms whose head occurrence - is the unfoldable constant :n:`@qualid` (the constant can be referred to by - its notation using :n:`@string` if such a notation exists). - -.. tacv:: simpl @qualid at {+ @natural} - simpl @string at {+ @natural} - - This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose - head occurrence is :n:`@qualid` (or :n:`@string`). - -.. flag:: Debug RAKAM - - This flag makes :tacn:`cbn` print various debugging information. - ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. - -.. tacn:: unfold @qualid - :name: unfold - - This tactic applies to any goal. The argument qualid must denote a - defined transparent constant or local definition (see - :ref:`gallina-definitions` and - :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence - of the constant to which :n:`@qualid` refers in the current goal - and then replaces it with its :math:`\beta\iota\zeta`-normal form. - Use the general reduction tactics if you want to avoid this final - reduction, for instance :n:`cbv delta [@qualid]`. - - .. exn:: Cannot coerce @qualid to an evaluable reference. - - This error is frequent when trying to unfold something that has - defined as an inductive type (or constructor) and not as a - definition. - - .. example:: - - .. coqtop:: abort all fail - - Goal 0 <= 1. - unfold le. - - This error can also be raised if you are trying to unfold - something that has been marked as opaque. - - .. example:: - - .. coqtop:: abort all fail - - Opaque Nat.add. - Goal 1 + 0 = 1. - unfold Nat.add. - - .. tacv:: unfold @qualid in @goal_occurrences - - Replaces :n:`@qualid` in hypothesis (or hypotheses) designated - by :token:`goal_occurrences` with its definition and replaces - the hypothesis with its :math:`\beta`:math:`\iota` normal form. - - .. tacv:: unfold {+, @qualid} - - Replaces :n:`{+, @qualid}` with their definitions and replaces - the current goal with its :math:`\beta`:math:`\iota` normal - form. - - .. tacv:: unfold {+, @qualid at @occurrences } - - The list :token:`occurrences` specify the occurrences of - :n:`@qualid` to be unfolded. Occurrences are located from left - to right. - - .. exn:: Bad occurrence number of @qualid. - :undocumented: - - .. exn:: @qualid does not occur. - :undocumented: - - .. tacv:: unfold @string - - If :n:`@string` denotes the discriminating symbol of a notation - (e.g. "+") or an expression defining a notation (e.g. `"_ + - _"`), and this notation denotes an application whose head symbol - is an unfoldable constant, then the tactic unfolds it. - - .. tacv:: unfold @string%@ident - - This is variant of :n:`unfold @string` where :n:`@string` gets - its interpretation from the scope bound to the delimiting key - :token:`ident` instead of its default interpretation (see - :ref:`Localinterpretationrulesfornotations`). - - .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } - - This is the most general form. - -.. tacn:: fold @term - :name: fold - - This tactic applies to any goal. The term :n:`@term` is reduced using the - :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint - definition has been wrongfully unfolded, making the goal very hard to read. - On the other hand, when an unfolded function applied to its argument has been - reduced, the :tacn:`fold` tactic won't do anything. - - .. example:: - - .. coqtop:: all abort - - Goal ~0=0. - unfold not. - Fail progress fold not. - pattern (0 = 0). - fold not. - - .. tacv:: fold {+ @term} - - Equivalent to :n:`fold @term ; ... ; fold @term`. - -.. tacn:: pattern @term - :name: pattern - - This command applies to any goal. The argument :n:`@term` must be a free - subterm of the current goal. The command pattern performs :math:`\beta`-expansion - (the inverse of :math:`\beta`-reduction) of the current goal (say :g:`T`) by - - + replacing all occurrences of :n:`@term` in :g:`T` with a fresh variable - + abstracting this variable - + applying the abstracted goal to :n:`@term` - - For instance, if the current goal :g:`T` is expressible as - :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` - in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into - :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for - instance, when the tactic ``apply`` fails on matching. - -.. tacv:: pattern @term at {+ @natural} - - Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for - :math:`\beta`-expansion. Occurrences are located from left to right. - -.. tacv:: pattern @term at - {+ @natural} - - All occurrences except the occurrences of indexes :n:`{+ @natural }` - of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from - left to right. - -.. tacv:: pattern {+, @term} - - Starting from a goal :math:`\varphi`:g:`(t`:sub:`1` :g:`... t`:sub:`m`:g:`)`, - the tactic :n:`pattern t`:sub:`1`:n:`, ..., t`:sub:`m` generates the - equivalent goal - :g:`(fun (x`:sub:`1`:g:`:A`:sub:`1`:g:`) ... (x`:sub:`m` :g:`:A`:sub:`m` :g:`) =>`:math:`\varphi`:g:`(x`:sub:`1` :g:`... x`:sub:`m` :g:`)) t`:sub:`1` :g:`... t`:sub:`m`. - If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these - occurrences will also be considered and possibly abstracted. - -.. tacv:: pattern {+, @term at {+ @natural}} - - This behaves as above but processing only the occurrences :n:`{+ @natural}` of - :n:`@term` starting from :n:`@term`. - -.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} - - This is the most general syntax that combines the different variants. - -.. tacn:: with_strategy @strategy_level_or_var [ {+ @reference } ] @ltac_expr3 - :name: with_strategy - - Executes :token:`ltac_expr3`, applying the alternate unfolding - behavior that the :cmd:`Strategy` command controls, but only for - :token:`ltac_expr3`. This can be useful for guarding calls to - reduction in tactic automation to ensure that certain constants are - never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to - ensure that unfolding does not fail. - - .. example:: - - .. coqtop:: all reset abort - - Opaque id. - Goal id 10 = 10. - Fail unfold id. - with_strategy transparent [id] unfold id. - - .. warning:: - - Use this tactic with care, as effects do not persist past the - end of the proof script. Notably, this fine-tuning of the - conversion strategy is not in effect during :cmd:`Qed` nor - :cmd:`Defined`, so this tactic is most useful either in - combination with :tacn:`abstract`, which will check the proof - early while the fine-tuning is still in effect, or to guard - calls to conversion in tactic automation to ensure that, e.g., - :tacn:`unfold` does not fail just because the user made a - constant :cmd:`Opaque`. - - This can be illustrated with the following example involving the - factorial function. - - .. coqtop:: in reset - - Fixpoint fact (n : nat) : nat := - match n with - | 0 => 1 - | S n' => n * fact n' - end. - - Suppose now that, for whatever reason, we want in general to - unfold the :g:`id` function very late during conversion: - - .. coqtop:: in - - Strategy 1000 [id]. - - If we try to prove :g:`id (fact n) = fact n` by - :tacn:`reflexivity`, it will now take time proportional to - :math:`n!`, because |Coq| will keep unfolding :g:`fact` and - :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full - computation of :g:`fact n` (in unary, because we are using - :g:`nat`), which takes time :math:`n!`. We can see this cross - the relevant threshold at around :math:`n = 9`: - - .. coqtop:: all abort - - Goal True. - Time assert (id (fact 8) = fact 8) by reflexivity. - Time assert (id (fact 9) = fact 9) by reflexivity. - - Note that behavior will be the same if you mark :g:`id` as - :g:`Opaque` because while most reduction tactics refuse to - unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as - merely a hint to unfold this constant last. - - We can get around this issue by using :tacn:`with_strategy`: - - .. coqtop:: all - - Goal True. - Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. - Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. - - However, when we go to close the proof, we will run into - trouble, because the reduction strategy changes are local to the - tactic passed to :tacn:`with_strategy`. - - .. coqtop:: all abort fail - - exact I. - Timeout 1 Defined. - - We can fix this issue by using :tacn:`abstract`: - - .. coqtop:: all - - Goal True. - Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. - exact I. - Time Defined. - - On small examples this sort of behavior doesn't matter, but - because |Coq| is a super-linear performance domain in so many - places, unless great care is taken, tactic automation using - :tacn:`with_strategy` may not be robustly performant when - scaling the size of the input. - - .. warning:: - - In much the same way this tactic does not play well with - :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as - an intermediary, this tactic does not play well with ``coqchk``, - even when used with :tacn:`abstract`, due to the inability of - tactics to persist information about conversion hints in the - proof term. See `#12200 - <https://github.com/coq/coq/issues/12200>`_ for more details. - -Conversion tactics applied to hypotheses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. tacn:: @tactic in {+, @ident} - - Applies :token:`tactic` (any of the conversion tactics listed in this - section) to the hypotheses :n:`{+ @ident}`. - - If :token:`ident` is a local definition, then :token:`ident` can be replaced by - :n:`type of @ident` to address not the body but the type of the local - definition. - - Example: :n:`unfold not in (type of H1) (type of H3)`. - -.. exn:: No such hypothesis: @ident. - :undocumented: - - -.. _automation: - -Automation ----------- - -.. tacn:: auto - :name: auto - - This tactic implements a Prolog-like resolution procedure to solve the - current goal. It first tries to solve the goal using the :tacn:`assumption` - tactic, then it reduces the goal to an atomic one using :tacn:`intros` and - introduces the newly generated hypotheses as hints. Then it looks at - the list of tactics associated to the head symbol of the goal and - tries to apply one of them (starting from the tactics with lower - cost). This process is recursively applied to the generated subgoals. - - By default, :tacn:`auto` only uses the hypotheses of the current goal and - the hints of the database named ``core``. - - .. warning:: - - :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to - :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will - fail even if applying manually one of the hints would succeed. - - .. tacv:: auto @natural - - Forces the search depth to be :token:`natural`. The maximal search depth - is 5 by default. - - .. tacv:: auto with {+ @ident} - - Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. - - .. note:: - - Use the fake database `nocore` if you want to *not* use the `core` - database. - - .. tacv:: auto with * - - Uses all existing hint databases. Using this variant is highly discouraged - in finished scripts since it is both slower and less robust than the variant - where the required databases are explicitly listed. - - .. seealso:: - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of - pre-defined databases and the way to create or extend a database. - - .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - - Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an - inductive type, it is the collection of its constructors which are added - as hints. - - .. note:: - - The hints passed through the `using` clause are used in the same - way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` - may fail where :n:`apply @qualid` succeeds. - - Given that this can be seen as counter-intuitive, it could be useful - to have an option to use full-blown :tacn:`apply` for lemmas passed - through the `using` clause. Contributions welcome! - - .. tacv:: info_auto - - Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. - - .. tacv:: debug auto - :name: debug auto - - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. - - .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} - - This is the most general form, combining the various options. - -.. tacv:: trivial - :name: trivial - - This tactic is a restriction of :tacn:`auto` that is not recursive - and tries only hints that cost `0`. Typically it solves trivial - equalities like :g:`X=X`. - - .. tacv:: trivial with {+ @ident} - trivial with * - trivial using {+ @qualid} - debug trivial - info_trivial - {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} - :name: _; _; _; debug trivial; info_trivial; _ - :undocumented: - -.. note:: - :tacn:`auto` and :tacn:`trivial` either solve completely the goal or - else succeed without changing the goal. Use :g:`solve [ auto ]` and - :g:`solve [ trivial ]` if you would prefer these tactics to fail when - they do not manage to solve the goal. - -.. flag:: Info Auto - Debug Auto - Info Trivial - Debug Trivial - - These flags enable printing of informative or debug information for - the :tacn:`auto` and :tacn:`trivial` tactics. - -.. tacn:: eauto - :name: eauto - - This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try - resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it internally uses a tactic - close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` - in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` - can solve such a goal: - - .. example:: - - .. coqtop:: all - - Hint Resolve ex_intro : core. - Goal forall P:nat -> Prop, P 0 -> exists n, P n. - eauto. - - Note that ``ex_intro`` should be declared as a hint. - - - .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} - - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. - - :tacn:`eauto` also obeys the following flags: - - .. flag:: Info Eauto - Debug Eauto - :undocumented: - - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` - - -.. tacn:: autounfold with {+ @ident} - :name: autounfold - - This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` - in the given databases. - -.. tacv:: autounfold with {+ @ident} in @goal_occurrences - - Performs the unfolding in the given clause (:token:`goal_occurrences`). - -.. tacv:: autounfold with * - - Uses the unfold hints declared in all the hint databases. - -.. tacn:: autorewrite with {+ @ident} - :name: autorewrite - - This tactic carries out rewritings according to the rewriting rule - bases :n:`{+ @ident}`. - - Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until - it fails. Once all the rules have been processed, if the main subgoal has - progressed (e.g., if it is distinct from the initial main goal) then the rules - of this base are processed again. If the main subgoal has not progressed then - the next base is processed. For the bases, the behavior is exactly similar to - the processing of the rewriting rules. - - The rewriting rule bases are built with the :cmd:`Hint Rewrite` - command. - -.. warning:: - - This tactic may loop if you build non terminating rewriting systems. - -.. tacv:: autorewrite with {+ @ident} using @tactic - - Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}` - applying tactic to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @qualid - - Performs all the rewritings in hypothesis :n:`@qualid`. - -.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic - - Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` - to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - - Performs all the rewriting in the clause :n:`@goal_occurrences`. - -.. seealso:: - - :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by - :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. - -.. tacn:: easy - :name: easy - - This tactic tries to solve the current goal by a number of standard closing steps. - In particular, it tries to close the current goal using the closing tactics - :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` - and :tacn:`inversion` of hypothesis. - If this fails, it tries introducing variables and splitting and-hypotheses, - using the closing tactics afterwards, and splitting the goal using - :tacn:`split` and recursing. - - This tactic solves goals that belong to many common classes; in particular, many cases of - unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. - -.. tacv:: now @tactic - :name: now - - Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. - -Controlling automation --------------------------- - -.. _thehintsdatabasesforautoandeauto: - -The hints databases for auto and eauto -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database -maps head symbols to a list of hints. - -.. cmd:: Print Hint @ident - - Use this command - to display the hints associated to the head symbol :n:`@ident` - (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative - integer, and an optional pattern. The hints with lower cost are tried first. A - hint is tried by :tacn:`auto` when the conclusion of the current goal matches its - pattern or when it has no pattern. - -Creating Hint databases -``````````````````````` - -One can optionally declare a hint database using the command -:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be -automatically created. - -.. cmd:: Create HintDb @ident {? discriminated} - - This command creates a new database named :n:`@ident`. The database is - implemented by a Discrimination Tree (DT) that serves as an index of - all the lemmas. The DT can use transparency information to decide if a - constant should be indexed or not - (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), - making the retrieval more efficient. The legacy implementation (the default one - for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` - goals), for non-Immediate hints and does not make use of transparency - hints, putting more work on the unification that is run after - retrieval (it keeps a list of the lemmas in case the DT is not used). - The new implementation enabled by the discriminated option makes use - of DTs in all cases and takes transparency information into account. - However, the order in which hints are retrieved from the DT may differ - from the order in which they were inserted, making this implementation - observationally different from the legacy one. - -.. cmd:: Hint @hint_definition : {+ @ident} - - The general command to add a hint to some databases :n:`{+ @ident}`. - - This command supports the :attr:`local`, :attr:`global` and :attr:`export` - locality attributes. When no locality is explictly given, the - command is :attr:`local` inside a section and :attr:`global` otherwise. - - + :attr:`local` hints are never visible from other modules, even if they - require or import the current module. Inside a section, the :attr:`local` - attribute is useless since hints do not survive anyway to the closure of - sections. - - + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. - - + :attr:`global` hints are made available by merely requiring the current - module. - - The various possible :production:`hint_definition`\s are given below. - - .. cmdv:: Hint @hint_definition - - No database name is given: the hint is registered in the ``core`` database. - - .. deprecated:: 8.10 - - .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident - :name: Hint Resolve - - This command adds :n:`simple apply @qualid` to the hint list with the head - symbol of the type of :n:`@qualid`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The - associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@qualid` does not start with a product the tactic added in the hint list - is :n:`exact @qualid`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @qualid` is also stored in - the hints list. If the inferred type of :n:`@qualid` contains a dependent - quantification on a variable which occurs only in the premisses of the type - and not in its conclusion, no instance could be inferred for the variable by - unification with the goal. In this case, the hint is added to the hint list - of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A - typical example of a hint that is used only by :tacn:`eauto` is a transitivity - lemma. - - .. exn:: @qualid cannot be used as a hint - - The head symbol of the type of :n:`@qualid` is a bound variable - such that this tactic cannot be associated to a constant. - - .. cmdv:: Hint Resolve {+ @qualid} : @ident - - Adds each :n:`Hint Resolve @qualid`. - - .. cmdv:: Hint Resolve -> @qualid : @ident - - Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @qualid`, although as mentioned - before, the tactic actually used is a restricted version of - :tacn:`apply`). - - .. cmdv:: Hint Resolve <- @qualid - - Adds the right-to-left implication of an equivalence as a hint. - - .. cmdv:: Hint Immediate @qualid : @ident - :name: Hint Immediate - - This command adds :n:`simple apply @qualid; trivial` to the hint list associated - with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are - not solved immediately by the :tacn:`trivial` tactic (which only tries tactics - with cost 0).This command is useful for theorems such as the symmetry of - equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited - use in order to avoid useless proof-search. The cost of this tactic (which - never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` - itself. - - .. exn:: @qualid cannot be used as a hint - :undocumented: - - .. cmdv:: Hint Immediate {+ @qualid} : @ident - - Adds each :n:`Hint Immediate @qualid`. - - .. cmdv:: Hint Constructors @qualid : @ident - :name: Hint Constructors - - If :token:`qualid` is an inductive type, this command adds all its constructors as - hints of type ``Resolve``. Then, when the conclusion of current goal has the form - :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. - - .. exn:: @qualid is not an inductive type - :undocumented: - - .. cmdv:: Hint Constructors {+ @qualid} : @ident - - Extends the previous command for several inductive types. - - .. cmdv:: Hint Unfold @qualid : @ident - :name: Hint Unfold - - This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :token:`qualid`. - Its cost is 4. - - .. cmdv:: Hint Unfold {+ @qualid} - - Extends the previous command for several defined constants. - - .. cmdv:: Hint Transparent {+ @qualid} : @ident - Hint Opaque {+ @qualid} : @ident - :name: Hint Transparent; Hint Opaque - - This adds transparency hints to the database, making :n:`@qualid` - transparent or opaque constants during resolution. This information is used - during unification of the goal with any lemma in the database and inside the - discrimination network to relax or constrain it in the case of discriminated - databases. - - .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident - Hint Constants {| Transparent | Opaque } : @ident - :name: Hint Variables; Hint Constants - - This sets the transparency flag used during unification of - hints in the database for all constants or all variables, - overwriting the existing settings of opacity. It is advised - to use this just after a :cmd:`Create HintDb` command. - - .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident - :name: Hint Extern - - This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and - :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a - :n:`@tactic` to execute. - - .. example:: - - .. coqtop:: in - - Hint Extern 4 (~(_ = _)) => discriminate : core. - - Now, when the head of the goal is a disequality, ``auto`` will try - discriminate if it does not manage to solve the goal with hints with a - cost less than 4. - - One can even use some sub-patterns of the pattern in - the tactic script. A sub-pattern is a question mark followed by an - identifier, like ``?X1`` or ``?X2``. Here is an example: - - .. example:: - - .. coqtop:: reset all - - Require Import List. - Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. - Goal forall a b:list (nat * nat), {a = b} + {a <> b}. - Info 1 auto with eqdec. - - .. cmdv:: Hint Cut @regexp : @ident - :name: Hint Cut - - .. warning:: - - These hints currently only apply to typeclass proof search and the - :tacn:`typeclasses eauto` tactic. - - This command can be used to cut the proof-search tree according to a regular - expression matching paths to be cut. The grammar for regular expressions is - the following. Beware, there is no operator precedence during parsing, one can - check with :cmd:`Print HintDb` to verify the current cut expression: - - .. prodn:: - regexp ::= @ident (hint or instance identifier) - | _ (any hint) - | @regexp | @regexp (disjunction) - | @regexp @regexp (sequence) - | @regexp * (Kleene star) - | emp (empty) - | eps (epsilon) - | ( @regexp ) - - The `emp` regexp does not match any search path while `eps` - matches the empty path. During proof search, the path of - successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have - an associated identifier). - Before applying any hint :n:`@ident` the current path `p` extended with - :n:`@ident` is matched against the current cut expression `c` associated to - the hint database. If matching succeeds, the hint is *not* applied. The - semantics of :n:`Hint Cut @regexp` is to set the cut expression - to :n:`c | regexp`, the initial cut expression being `emp`. - - .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident - :name: Hint Mode - - This sets an optional mode of use of the identifier :n:`@qualid`. When - proof-search faces a goal that ends in an application of :n:`@qualid` to - arguments :n:`@term ... @term`, the mode tells if the hints associated to - :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, - ``!`` or ``-`` items that specify if an argument of the identifier is to be - treated as an input (``+``), if its head only is an input (``!``) or an output - (``-``) of the identifier. For a mode to match a list of arguments, input - terms and input heads *must not* contain existential variables or be - existential variables respectively, while outputs can be any term. Multiple - modes can be declared for a single identifier, in that case only one mode - needs to match the arguments for the hints to be applied. The head of a term - is understood here as the applicative head, or the match or projection - scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is - especially useful for typeclasses, when one does not want to support default - instances and avoid ambiguity in general. Setting a parameter of a class as an - input forces proof-search to be driven by that index of the class, with ``!`` - giving more flexibility by allowing existentials to still appear deeper in the - index but not at its head. - - .. note:: - - + One can use a :cmd:`Hint Extern` with no pattern to do - pattern matching on hypotheses using ``match goal with`` - inside the tactic. - - + If you want to add hints such as :cmd:`Hint Transparent`, - :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass - resolution, do not forget to put them in the - ``typeclass_instances`` hint database. - - -Hint databases defined in the |Coq| standard library -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Several hint databases are defined in the |Coq| standard library. The -actual content of a database is the collection of hints declared -to belong to this database in each of the various modules currently -loaded. Especially, requiring new modules may extend the database. -At |Coq| startup, only the core database is nonempty and can be used. - -:core: This special database is automatically used by ``auto``, except when - pseudo-database ``nocore`` is given to ``auto``. The core database - contains only basic lemmas about negation, conjunction, and so on. - Most of the hints in this database come from the Init and Logic directories. - -:arith: This database contains all lemmas about Peano’s arithmetic proved in the - directories Init and Arith. - -:zarith: contains lemmas about binary signed integers from the - directories theories/ZArith. The database also contains - high-cost hints that call :tacn:`lia` on equations and - inequalities in ``nat`` or ``Z``. - -:bool: contains lemmas about booleans, mostly from directory theories/Bool. - -:datatypes: is for lemmas about lists, streams and so on that are mainly proved - in the Lists subdirectory. - -:sets: contains lemmas about sets and relations from the directories Sets and - Relations. - -:typeclass_instances: contains all the typeclass instances declared in the - environment, including those used for ``setoid_rewrite``, - from the Classes directory. - -: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. - -.. _removehints: - -.. cmd:: Remove Hints {+ @term} : {+ @ident} - - This command removes the hints associated to terms :n:`{+ @term}` in databases - :n:`{+ @ident}`. - -.. _printhint: - -.. cmd:: Print Hint - - This command displays all hints that apply to the current goal. It - fails if no proof is being edited, while the two variants can be used - at every moment. - -**Variants:** - - -.. cmd:: Print Hint @ident - - This command displays only tactics associated with :n:`@ident` in the hints - list. This is independent of the goal being edited, so this command will not - fail if no goal is being edited. - -.. cmd:: Print Hint * - - This command displays all declared hints. - -.. cmd:: Print HintDb @ident - - This command displays all hints from database :n:`@ident`. - -.. _hintrewrite: - -.. cmd:: Hint Rewrite {+ @term} : {+ @ident} - - This vernacular command adds the terms :n:`{+ @term}` (their types must be - equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation - (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` - hint bases and that :tacn:`auto` does not take them into account. - - This command is synchronous with the section mechanism (see :ref:`section-mechanism`): - when closing a section, all aliases created by ``Hint Rewrite`` in that - section are lost. Conversely, when loading a module, all ``Hint Rewrite`` - declarations at the global level of that module are loaded. - -**Variants:** - -.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident} - - This is strictly equivalent to the command above (we only make explicit the - orientation which otherwise defaults to ->). - -.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident} - - Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in - the bases :n:`{+ @ident}`. - -.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } - - When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the - tactic ``tactic`` will be applied to the generated subgoals, the main subgoal - excluded. - -.. cmd:: Print Rewrite HintDb @ident - - This command displays all rewrite hints contained in :n:`@ident`. - -Hint locality -~~~~~~~~~~~~~ - -Hints provided by the ``Hint`` commands are erased when closing a section. -Conversely, all hints of a module ``A`` that are not defined inside a -section (and not defined with option ``Local``) become available when the -module ``A`` is required (using e.g. ``Require A.``). - -As of today, hints only have a binary behavior regarding locality, as -described above: either they disappear at the end of a section scope, -or they remain global forever. This causes a scalability issue, -because hints coming from an unrelated part of the code may badly -influence another development. It can be mitigated to some extent -thanks to the :cmd:`Remove Hints` command, -but this is a mere workaround and has some limitations (for instance, external -hints cannot be removed). - -A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects |Coq| uses. Hints should only be made available when -the module they are defined in is imported, not just required. It is very -difficult to change the historical behavior, as it would break a lot of scripts. -We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` -option which accepts three flags allowing for a fine-grained handling of -non-imported hints. - -.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } - :name: Loose Hint Behavior - - This option accepts three values, which control the behavior of hints w.r.t. - :cmd:`Import`: - - - "Lax": this is the default, and corresponds to the historical behavior, - that is, hints defined outside of a section have a global scope. - - - "Warn": outputs a warning when a non-imported hint is used. Note that this - is an over-approximation, because a hint may be triggered by a run that - will eventually fail and backtrack, resulting in the hint not being - actually useful for the proof. - - - "Strict": changes the behavior of an unloaded hint to a immediate fail - tactic, allowing to emulate an import-scoped hint mechanism. - -.. _tactics-implicit-automation: - -Setting implicit automation tactics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Proof with @tactic - - This command may be used to start a proof. It defines a default tactic - to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. - In this case the tactic command typed by the user is equivalent to - ``tactic``:sub:`1` ``;tactic``. - - .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - - - .. cmdv:: Proof with @tactic using {+ @ident} - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - - .. cmdv:: Proof using {+ @ident} with @tactic - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - -.. _decisionprocedures: - -Decision procedures -------------------- - -.. tacn:: tauto - :name: tauto - - This tactic implements a decision procedure for intuitionistic propositional - calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff - :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an - intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and - logical equivalence but does not unfold any other definition. - -.. example:: - - The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would - fail: - - .. coqtop:: reset all - - Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. - intros. - tauto. - -Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. -Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. -:tacn:`tauto` can for instance for: - -.. example:: - - .. coqtop:: reset all - - Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. - tauto. - -.. note:: - In contrast, :tacn:`tauto` cannot solve the following goal - :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` - :g:`forall x:nat, ~ ~ (A \/ P x).` - because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and - an instantiation of `x` is necessary. - -.. tacv:: dtauto - :name: dtauto - - While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. - -.. tacn:: intuition @tactic - :name: intuition - - The tactic :tacn:`intuition` takes advantage of the search-tree built by the - decision procedure involved in the tactic :tacn:`tauto`. It uses this - information to generate a set of subgoals equivalent to the original one (but - simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If - this tactic fails on some goals then :tacn:`intuition` fails. In fact, - :tacn:`tauto` is simply :g:`intuition fail`. - - .. example:: - - For instance, the tactic :g:`intuition auto` applied to the goal:: - - (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O - - internally replaces it by the equivalent one:: - - (forall (x:nat), P x), B |- P O - - and then uses :tacn:`auto` which completes the proof. - -Originally due to César Muñoz, these tactics (:tacn:`tauto` and -:tacn:`intuition`) have been completely re-engineered by David Delahaye using -mainly the tactic language (see :ref:`ltac`). The code is -now much shorter and a significant increase in performance has been noticed. -The general behavior with respect to dependent types, unfolding and -introductions has slightly changed to get clearer semantics. This may lead to -some incompatibilities. - -.. tacv:: intuition - - Is equivalent to :g:`intuition auto with *`. - -.. tacv:: dintuition - :name: dintuition - - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. - -.. flag:: Intuition Negation Unfolding - - Controls whether :tacn:`intuition` unfolds inner negations which do not need - to be unfolded. This flag is on by default. - -.. tacn:: rtauto - :name: rtauto - - The :tacn:`rtauto` tactic solves propositional tautologies similarly to what - :tacn:`tauto` does. The main difference is that the proof term is built using a - reflection scheme applied to a sequent calculus proof of the goal. The search - procedure is also implemented using a different technique. - - Users should be aware that this difference may result in faster proof-search - but slower proof-checking, and :tacn:`rtauto` might not solve goals that - :tacn:`tauto` would be able to solve (e.g. goals involving universal - quantifiers). - - Note that this tactic is only available after a ``Require Import Rtauto``. - -.. tacn:: firstorder - :name: firstorder - - The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to - first- order reasoning, written by Pierre Corbineau. It is not restricted to - usual logical connectives but instead may reason about any first-order class - inductive definition. - -.. opt:: Firstorder Solver @tactic - :name: Firstorder Solver - - The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with core`, it can be reset locally or globally using this option. - - .. cmd:: Print Firstorder Solver - - Prints the default tactic used by :tacn:`firstorder` when no rule applies. - -.. tacv:: firstorder @tactic - - Tries to solve the goal with :n:`@tactic` when no logical rule may apply. - -.. tacv:: firstorder using {+ @qualid} - - .. deprecated:: 8.3 - - Use the syntax below instead (with commas). - -.. tacv:: firstorder using {+, @qualid} - - Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` - refers to an inductive type, it is the collection of its constructors which are - added to the proof-search environment. - -.. tacv:: firstorder with {+ @ident} - - Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search - environment. - -.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} - - This combines the effects of the different variants of :tacn:`firstorder`. - -.. opt:: Firstorder Depth @natural - :name: Firstorder Depth - - This option controls the proof-search depth bound. - -.. tacn:: congruence - :name: congruence - - The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard - Nelson and Oppen congruence closure algorithm, which is a decision procedure - for ground equalities with uninterpreted symbols. It also includes - constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal - is a non-quantified equality, congruence tries to prove it with non-quantified - equalities in the context. Otherwise it tries to infer a discriminable equality - from those in the context. Alternatively, congruence tries to prove that a - hypothesis is equal to the goal or to the negation of another hypothesis. - - :tacn:`congruence` is also able to take advantage of hypotheses stating - quantified equalities, but you have to provide a bound for the number of extra - equalities generated that way. Please note that one of the sides of the - equality must contain all the quantified variables in order for congruence to - match against it. - -.. example:: - - .. coqtop:: reset all - - Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. - intros. - congruence. - Qed. - - Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. - intros. - congruence. - Qed. - -.. tacv:: congruence @natural - - Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of :token:`natural` does not make - success slower, only failure. You might consider adding some lemmas as - hypotheses using assert in order for :tacn:`congruence` to use them. - -.. tacv:: congruence with {+ @term} - :name: congruence with - - Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps - in case you have partially applied constructors in your goal. - -.. exn:: I don’t know how to handle dependent equality. - - The decision procedure managed to find a proof of the goal or of a - discriminable equality but this proof could not be built in |Coq| because of - dependently-typed functions. - -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. - - The decision procedure could solve the goal with the provision that additional - arguments are supplied for some partially applied constructors. Any term of an - appropriate type will allow the tactic to successfully solve the goal. Those - additional arguments can be given to congruence by filling in the holes in the - terms given in the error message, using the :tacn:`congruence with` variant described above. - -.. flag:: Congruence Verbose - - This flag makes :tacn:`congruence` print debug information. - Checking properties of terms ---------------------------- @@ -4647,189 +2893,6 @@ using the ``Require Import`` command. Use :tacn:`classical_right` to prove the right part of the disjunction with the assumption that the negation of left part holds. -.. _tactics-automating: - -Automating ------------- - - -.. tacn:: btauto - :name: btauto - - The tactic :tacn:`btauto` implements a reflexive solver for boolean - tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are - constructed over the following grammar: - - .. prodn:: - btauto_term ::= @ident - | true - | false - | orb @btauto_term @btauto_term - | andb @btauto_term @btauto_term - | xorb @btauto_term @btauto_term - | negb @btauto_term - | if @btauto_term then @btauto_term else @btauto_term - - Whenever the formula supplied is not a tautology, it also provides a - counter-example. - - Internally, it uses a system very similar to the one of the ring - tactic. - - Note that this tactic is only available after a ``Require Import Btauto``. - - .. exn:: Cannot recognize a boolean equality. - - The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` - doesn't introduce variables into the context on its own. - -.. tacv:: field - field_simplify {* @term} - field_simplify_eq - - The field tactic is built on the same ideas as ring: this is a - reflexive tactic that solves or simplifies equations in a field - structure. The main idea is to reduce a field expression (which is an - extension of ring expressions with the inverse and division - operations) to a fraction made of two polynomial expressions. - - Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` - replaces the provided terms by their reduced fraction. - :n:`field_simplify_eq` applies when the conclusion is an equation: it - simplifies both hand sides and multiplies so as to cancel - denominators. So it produces an equation without division nor inverse. - - All of these 3 tactics may generate a subgoal in order to prove that - denominators are different from zero. - - See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to - declare new field structures. All declared field structures can be - printed with the Print Fields command. - -.. example:: - - .. coqtop:: reset all - - Require Import Reals. - Goal forall x y:R, - (x * y > 0)%R -> - (x * (1 / x + x / (x + y)))%R = - ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. - - intros; field. - -.. seealso:: - - File plugins/ring/RealField.v for an example of instantiation, - theory theories/Reals for many examples of use of field. - -Non-logical tactics ------------------------- - - -.. tacn:: cycle @integer - :name: cycle - - Reorders the selected goals so that the first :n:`@integer` goals appear after the - other selected goals. - If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the - beginning of the list. - The tactic is only useful with a goal selector, most commonly `all:`. - Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent - to `all: cycle 1`. See :tacn:`… : … (goal selector)`. - -.. example:: - - .. coqtop:: none reset - - Parameter P : nat -> Prop. - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: cycle 2. - all: cycle -3. - -.. tacn:: swap @integer @integer - :name: swap - - Exchanges the position of the specified goals. - Negative values for :n:`@integer` indicate counting goals - backward from the end of the list of selected goals. Goals are indexed from 1. - The tactic is only useful with a goal selector, most commonly `all:`. - Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent - to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. - -.. example:: - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: swap 1 3. - all: swap 1 -1. - -.. tacn:: revgoals - :name: revgoals - - Reverses the order of the selected goals. The tactic is only useful with a goal - selector, most commonly `all :`. Note that other selectors reorder goals; - `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. - - .. example:: - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: revgoals. - -.. tacn:: shelve - :name: shelve - - This tactic moves all goals under focus to a shelf. While on the - shelf, goals will not be focused on. They can be solved by - unification, or they can be called back into focus with the command - :cmd:`Unshelve`. - - .. tacv:: shelve_unifiable - :name: shelve_unifiable - - Shelves only the goals under focus that are mentioned in other goals. - Goals that appear in the type of other goals can be solved by unification. - - .. example:: - - .. coqtop:: all abort - - Goal exists n, n=0. - refine (ex_intro _ _ _). - all: shelve_unifiable. - reflexivity. - -.. cmd:: Unshelve - - This command moves all the goals on the shelf (see :tacn:`shelve`) - from the shelf into focus, by appending them to the end of the current - list of focused goals. - -.. tacn:: unshelve @tactic - :name: unshelve - - Performs :n:`@tactic`, then unshelves existential variables added to the - shelf by the execution of :n:`@tactic`, prepending them to the current goal. - -.. tacn:: give_up - :name: give_up - - This tactic removes the focused goals from the proof. They are not - solved, and cannot be solved later in the proof. As the goals are not - solved, the proof cannot be closed. - - The ``give_up`` tactic can be used while editing a proof, to choose to - write the proof script in a non-sequential order. - Delaying solving unification constraints ---------------------------------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 301559d69d..dd0b12f8ec 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -990,11 +990,6 @@ described first. has to check the conversion (see Section :ref:`conversion-rules`) of two distinct applied constants. - .. seealso:: - - Sections :ref:`performingcomputations`, :ref:`tactics-automating`, - :ref:`proof-editing-mode` - .. cmd:: Transparent {+ @reference } This command accepts the :attr:`global` attribute. By default, the scope @@ -1015,10 +1010,7 @@ described first. There is no constant named :n:`@qualid` in the environment. - .. seealso:: - - Sections :ref:`performingcomputations`, - :ref:`tactics-automating`, :ref:`proof-editing-mode` +.. seealso:: :ref:`performingcomputations` and :ref:`proof-editing-mode` .. _vernac-strategy: diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst new file mode 100644 index 0000000000..cc8af976d2 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -0,0 +1,672 @@ +.. _automation: + +========================= +Programmable proof search +========================= + +.. tacn:: auto + :name: auto + + This tactic implements a Prolog-like resolution procedure to solve the + current goal. It first tries to solve the goal using the :tacn:`assumption` + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and + introduces the newly generated hypotheses as hints. Then it looks at + the list of tactics associated to the head symbol of the goal and + tries to apply one of them (starting from the tactics with lower + cost). This process is recursively applied to the generated subgoals. + + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. + + .. warning:: + + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. + + .. tacv:: auto @natural + + Forces the search depth to be :token:`natural`. The maximal search depth + is 5 by default. + + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + + .. note:: + + Use the fake database `nocore` if you want to *not* use the `core` + database. + + .. tacv:: auto with * + + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. + + .. seealso:: + :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of + pre-defined databases and the way to create or extend a database. + + .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } + + Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an + inductive type, it is the collection of its constructors which are added + as hints. + + .. note:: + + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` + may fail where :n:`apply @qualid` succeeds. + + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! + + .. tacv:: info_auto + + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. + + .. tacv:: debug auto + :name: debug auto + + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. + + .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + + This is the most general form, combining the various options. + +.. tacv:: trivial + :name: trivial + + This tactic is a restriction of :tacn:`auto` that is not recursive + and tries only hints that cost `0`. Typically it solves trivial + equalities like :g:`X=X`. + + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @qualid} + debug trivial + info_trivial + {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: + +.. note:: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. + +.. flag:: Info Auto + Debug Auto + Info Trivial + Debug Trivial + + These flags enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. + +.. tacn:: eauto + :name: eauto + + This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try + resolution hints which would leave existential variables in the goal, + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` + can solve such a goal: + + .. example:: + + .. coqtop:: all + + Hint Resolve ex_intro : core. + Goal forall P:nat -> Prop, P 0 -> exists n, P n. + eauto. + + Note that ``ex_intro`` should be declared as a hint. + + + .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + + :tacn:`eauto` also obeys the following flags: + + .. flag:: Info Eauto + Debug Eauto + :undocumented: + + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + + +.. tacn:: autounfold with {+ @ident} + :name: autounfold + + This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + in the given databases. + +.. tacv:: autounfold with {+ @ident} in @goal_occurrences + + Performs the unfolding in the given clause (:token:`goal_occurrences`). + +.. tacv:: autounfold with * + + Uses the unfold hints declared in all the hint databases. + +.. tacn:: autorewrite with {+ @ident} + :name: autorewrite + + This tactic carries out rewritings according to the rewriting rule + bases :n:`{+ @ident}`. + + Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + it fails. Once all the rules have been processed, if the main subgoal has + progressed (e.g., if it is distinct from the initial main goal) then the rules + of this base are processed again. If the main subgoal has not progressed then + the next base is processed. For the bases, the behavior is exactly similar to + the processing of the rewriting rules. + + The rewriting rule bases are built with the :cmd:`Hint Rewrite` + command. + +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. + +.. tacv:: autorewrite with {+ @ident} using @tactic + + Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}` + applying tactic to the main subgoal after each rewriting step. + +.. tacv:: autorewrite with {+ @ident} in @qualid + + Performs all the rewritings in hypothesis :n:`@qualid`. + +.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic + + Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` + to the main subgoal after each rewriting step. + +.. tacv:: autorewrite with {+ @ident} in @goal_occurrences + + Performs all the rewriting in the clause :n:`@goal_occurrences`. + +.. seealso:: + + :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by + :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. + +.. tacn:: easy + :name: easy + + This tactic tries to solve the current goal by a number of standard closing steps. + In particular, it tries to close the current goal using the closing tactics + :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` + and :tacn:`inversion` of hypothesis. + If this fails, it tries introducing variables and splitting and-hypotheses, + using the closing tactics afterwards, and splitting the goal using + :tacn:`split` and recursing. + + This tactic solves goals that belong to many common classes; in particular, many cases of + unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +.. tacv:: now @tactic + :name: now + + Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. + +Controlling automation +-------------------------- + +.. _thehintsdatabasesforautoandeauto: + +The hints databases for auto and eauto +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database +maps head symbols to a list of hints. + +.. cmd:: Print Hint @ident + + Use this command + to display the hints associated to the head symbol :n:`@ident` + (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative + integer, and an optional pattern. The hints with lower cost are tried first. A + hint is tried by :tacn:`auto` when the conclusion of the current goal matches its + pattern or when it has no pattern. + +Creating Hint databases +``````````````````````` + +One can optionally declare a hint database using the command +:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be +automatically created. + +.. cmd:: Create HintDb @ident {? discriminated} + + This command creates a new database named :n:`@ident`. The database is + implemented by a Discrimination Tree (DT) that serves as an index of + all the lemmas. The DT can use transparency information to decide if a + constant should be indexed or not + (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), + making the retrieval more efficient. The legacy implementation (the default one + for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` + goals), for non-Immediate hints and does not make use of transparency + hints, putting more work on the unification that is run after + retrieval (it keeps a list of the lemmas in case the DT is not used). + The new implementation enabled by the discriminated option makes use + of DTs in all cases and takes transparency information into account. + However, the order in which hints are retrieved from the DT may differ + from the order in which they were inserted, making this implementation + observationally different from the legacy one. + +.. cmd:: Hint @hint_definition : {+ @ident} + + The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + sections. + + + :attr:`export` are visible from other modules when they import the current + module. Requiring it is not enough. This attribute is only effective for + the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and + :cmd:`Hint Extern` variants of the command. + + + :attr:`global` hints are made available by merely requiring the current + module. + + The various possible :production:`hint_definition`\s are given below. + + .. cmdv:: Hint @hint_definition + + No database name is given: the hint is registered in the ``core`` database. + + .. deprecated:: 8.10 + + .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident + :name: Hint Resolve + + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The + associated :n:`@pattern` is inferred from the conclusion of the type of + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent + quantification on a variable which occurs only in the premisses of the type + and not in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the hint list + of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A + typical example of a hint that is used only by :tacn:`eauto` is a transitivity + lemma. + + .. exn:: @qualid cannot be used as a hint + + The head symbol of the type of :n:`@qualid` is a bound variable + such that this tactic cannot be associated to a constant. + + .. cmdv:: Hint Resolve {+ @qualid} : @ident + + Adds each :n:`Hint Resolve @qualid`. + + .. cmdv:: Hint Resolve -> @qualid : @ident + + Adds the left-to-right implication of an equivalence as a hint (informally + the hint will be used as :n:`apply <- @qualid`, although as mentioned + before, the tactic actually used is a restricted version of + :tacn:`apply`). + + .. cmdv:: Hint Resolve <- @qualid + + Adds the right-to-left implication of an equivalence as a hint. + + .. cmdv:: Hint Immediate @qualid : @ident + :name: Hint Immediate + + This command adds :n:`simple apply @qualid; trivial` to the hint list associated + with the head symbol of the type of :n:`@ident` in the given database. This + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are + not solved immediately by the :tacn:`trivial` tactic (which only tries tactics + with cost 0).This command is useful for theorems such as the symmetry of + equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited + use in order to avoid useless proof-search. The cost of this tactic (which + never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` + itself. + + .. exn:: @qualid cannot be used as a hint + :undocumented: + + .. cmdv:: Hint Immediate {+ @qualid} : @ident + + Adds each :n:`Hint Immediate @qualid`. + + .. cmdv:: Hint Constructors @qualid : @ident + :name: Hint Constructors + + If :token:`qualid` is an inductive type, this command adds all its constructors as + hints of type ``Resolve``. Then, when the conclusion of current goal has the form + :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. + + .. exn:: @qualid is not an inductive type + :undocumented: + + .. cmdv:: Hint Constructors {+ @qualid} : @ident + + Extends the previous command for several inductive types. + + .. cmdv:: Hint Unfold @qualid : @ident + :name: Hint Unfold + + This adds the tactic :n:`unfold @qualid` to the hint list that will only be + used when the head constant of the goal is :token:`qualid`. + Its cost is 4. + + .. cmdv:: Hint Unfold {+ @qualid} + + Extends the previous command for several defined constants. + + .. cmdv:: Hint Transparent {+ @qualid} : @ident + Hint Opaque {+ @qualid} : @ident + :name: Hint Transparent; Hint Opaque + + This adds transparency hints to the database, making :n:`@qualid` + transparent or opaque constants during resolution. This information is used + during unification of the goal with any lemma in the database and inside the + discrimination network to relax or constrain it in the case of discriminated + databases. + + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident + :name: Hint Variables; Hint Constants + + This sets the transparency flag used during unification of + hints in the database for all constants or all variables, + overwriting the existing settings of opacity. It is advised + to use this just after a :cmd:`Create HintDb` command. + + .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident + :name: Hint Extern + + This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a + :n:`@tactic` to execute. + + .. example:: + + .. coqtop:: in + + Hint Extern 4 (~(_ = _)) => discriminate : core. + + Now, when the head of the goal is a disequality, ``auto`` will try + discriminate if it does not manage to solve the goal with hints with a + cost less than 4. + + One can even use some sub-patterns of the pattern in + the tactic script. A sub-pattern is a question mark followed by an + identifier, like ``?X1`` or ``?X2``. Here is an example: + + .. example:: + + .. coqtop:: reset all + + Require Import List. + Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + Goal forall a b:list (nat * nat), {a = b} + {a <> b}. + Info 1 auto with eqdec. + + .. cmdv:: Hint Cut @regexp : @ident + :name: Hint Cut + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + This command can be used to cut the proof-search tree according to a regular + expression matching paths to be cut. The grammar for regular expressions is + the following. Beware, there is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression: + + .. prodn:: + regexp ::= @ident (hint or instance identifier) + | _ (any hint) + | @regexp | @regexp (disjunction) + | @regexp @regexp (sequence) + | @regexp * (Kleene star) + | emp (empty) + | eps (epsilon) + | ( @regexp ) + + The `emp` regexp does not match any search path while `eps` + matches the empty path. During proof search, the path of + successive successful hints on a search branch is recorded, as a + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have + an associated identifier). + Before applying any hint :n:`@ident` the current path `p` extended with + :n:`@ident` is matched against the current cut expression `c` associated to + the hint database. If matching succeeds, the hint is *not* applied. The + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. + + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident + :name: Hint Mode + + This sets an optional mode of use of the identifier :n:`@qualid`. When + proof-search faces a goal that ends in an application of :n:`@qualid` to + arguments :n:`@term ... @term`, the mode tells if the hints associated to + :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, + ``!`` or ``-`` items that specify if an argument of the identifier is to be + treated as an input (``+``), if its head only is an input (``!``) or an output + (``-``) of the identifier. For a mode to match a list of arguments, input + terms and input heads *must not* contain existential variables or be + existential variables respectively, while outputs can be any term. Multiple + modes can be declared for a single identifier, in that case only one mode + needs to match the arguments for the hints to be applied. The head of a term + is understood here as the applicative head, or the match or projection + scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is + especially useful for typeclasses, when one does not want to support default + instances and avoid ambiguity in general. Setting a parameter of a class as an + input forces proof-search to be driven by that index of the class, with ``!`` + giving more flexibility by allowing existentials to still appear deeper in the + index but not at its head. + + .. note:: + + + One can use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. + + + If you want to add hints such as :cmd:`Hint Transparent`, + :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass + resolution, do not forget to put them in the + ``typeclass_instances`` hint database. + + +Hint databases defined in the |Coq| standard library +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Several hint databases are defined in the |Coq| standard library. The +actual content of a database is the collection of hints declared +to belong to this database in each of the various modules currently +loaded. Especially, requiring new modules may extend the database. +At |Coq| startup, only the core database is nonempty and can be used. + +:core: This special database is automatically used by ``auto``, except when + pseudo-database ``nocore`` is given to ``auto``. The core database + contains only basic lemmas about negation, conjunction, and so on. + Most of the hints in this database come from the Init and Logic directories. + +:arith: This database contains all lemmas about Peano’s arithmetic proved in the + directories Init and Arith. + +:zarith: contains lemmas about binary signed integers from the + directories theories/ZArith. The database also contains + high-cost hints that call :tacn:`lia` on equations and + inequalities in ``nat`` or ``Z``. + +:bool: contains lemmas about booleans, mostly from directory theories/Bool. + +:datatypes: is for lemmas about lists, streams and so on that are mainly proved + in the Lists subdirectory. + +:sets: contains lemmas about sets and relations from the directories Sets and + Relations. + +:typeclass_instances: contains all the typeclass instances declared in the + environment, including those used for ``setoid_rewrite``, + from the Classes directory. + +: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. + +.. _removehints: + +.. cmd:: Remove Hints {+ @term} : {+ @ident} + + This command removes the hints associated to terms :n:`{+ @term}` in databases + :n:`{+ @ident}`. + +.. _printhint: + +.. cmd:: Print Hint + + This command displays all hints that apply to the current goal. It + fails if no proof is being edited, while the two variants can be used + at every moment. + +**Variants:** + + +.. cmd:: Print Hint @ident + + This command displays only tactics associated with :n:`@ident` in the hints + list. This is independent of the goal being edited, so this command will not + fail if no goal is being edited. + +.. cmd:: Print Hint * + + This command displays all declared hints. + +.. cmd:: Print HintDb @ident + + This command displays all hints from database :n:`@ident`. + +.. _hintrewrite: + +.. cmd:: Hint Rewrite {+ @term} : {+ @ident} + + This vernacular command adds the terms :n:`{+ @term}` (their types must be + equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation + (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` + hint bases and that :tacn:`auto` does not take them into account. + + This command is synchronous with the section mechanism (see :ref:`section-mechanism`): + when closing a section, all aliases created by ``Hint Rewrite`` in that + section are lost. Conversely, when loading a module, all ``Hint Rewrite`` + declarations at the global level of that module are loaded. + +**Variants:** + +.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident} + + This is strictly equivalent to the command above (we only make explicit the + orientation which otherwise defaults to ->). + +.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident} + + Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in + the bases :n:`{+ @ident}`. + +.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } + + When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the + tactic ``tactic`` will be applied to the generated subgoals, the main subgoal + excluded. + +.. cmd:: Print Rewrite HintDb @ident + + This command displays all rewrite hints contained in :n:`@ident`. + +Hint locality +~~~~~~~~~~~~~ + +Hints provided by the ``Hint`` commands are erased when closing a section. +Conversely, all hints of a module ``A`` that are not defined inside a +section (and not defined with option ``Local``) become available when the +module ``A`` is required (using e.g. ``Require A.``). + +As of today, hints only have a binary behavior regarding locality, as +described above: either they disappear at the end of a section scope, +or they remain global forever. This causes a scalability issue, +because hints coming from an unrelated part of the code may badly +influence another development. It can be mitigated to some extent +thanks to the :cmd:`Remove Hints` command, +but this is a mere workaround and has some limitations (for instance, external +hints cannot be removed). + +A proper way to fix this issue is to bind the hints to their module scope, as +for most of the other objects |Coq| uses. Hints should only be made available when +the module they are defined in is imported, not just required. It is very +difficult to change the historical behavior, as it would break a lot of scripts. +We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` +option which accepts three flags allowing for a fine-grained handling of +non-imported hints. + +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } + :name: Loose Hint Behavior + + This option accepts three values, which control the behavior of hints w.r.t. + :cmd:`Import`: + + - "Lax": this is the default, and corresponds to the historical behavior, + that is, hints defined outside of a section have a global scope. + + - "Warn": outputs a warning when a non-imported hint is used. Note that this + is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being + actually useful for the proof. + + - "Strict": changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. + +.. _tactics-implicit-automation: + +Setting implicit automation tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Proof with @tactic + + This command may be used to start a proof. It defines a default tactic + to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. + In this case the tactic command typed by the user is equivalent to + ``tactic``:sub:`1` ``;tactic``. + + .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. + + + .. cmdv:: Proof with @tactic using {+ @ident} + + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` + + .. cmdv:: Proof using {+ @ident} with @tactic + + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index a219770c69..c3712b109d 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -1,20 +1,22 @@ .. _automatic-tactics: ===================================================== -Built-in decision procedures and programmable tactics +Automatic solvers and programmable tactics ===================================================== Some tactics are largely automated and are able to solve complex -goals. This chapter presents both some decision procedures that can -be used to solve some specific categories of goals, and some -programmable tactics, that the user can instrument to handle some +goals. This chapter presents both built-in solvers that can +be used on specific categories of goals and +programmable tactics that the user can instrument to handle complex goals in new domains. .. toctree:: :maxdepth: 1 + logic ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz + auto ../../addendum/generalized-rewriting diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst new file mode 100644 index 0000000000..acf64ae437 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -0,0 +1,294 @@ +.. _decisionprocedures: + +============================== +Solvers for logic and equality +============================== + +.. tacn:: tauto + :name: tauto + + This tactic implements a decision procedure for intuitionistic propositional + calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff + :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an + intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and + logical equivalence but does not unfold any other definition. + +.. example:: + + The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would + fail: + + .. coqtop:: reset all + + Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. + intros. + tauto. + +Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. +Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. +:tacn:`tauto` can for instance for: + +.. example:: + + .. coqtop:: reset all + + Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. + tauto. + +.. note:: + In contrast, :tacn:`tauto` cannot solve the following goal + :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` + :g:`forall x:nat, ~ ~ (A \/ P x).` + because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and + an instantiation of `x` is necessary. + +.. tacv:: dtauto + :name: dtauto + + While :tacn:`tauto` recognizes inductively defined connectives isomorphic to + the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. + +.. tacn:: intuition @tactic + :name: intuition + + The tactic :tacn:`intuition` takes advantage of the search-tree built by the + decision procedure involved in the tactic :tacn:`tauto`. It uses this + information to generate a set of subgoals equivalent to the original one (but + simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If + this tactic fails on some goals then :tacn:`intuition` fails. In fact, + :tacn:`tauto` is simply :g:`intuition fail`. + + .. example:: + + For instance, the tactic :g:`intuition auto` applied to the goal:: + + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O + + internally replaces it by the equivalent one:: + + (forall (x:nat), P x), B |- P O + + and then uses :tacn:`auto` which completes the proof. + +Originally due to César Muñoz, these tactics (:tacn:`tauto` and +:tacn:`intuition`) have been completely re-engineered by David Delahaye using +mainly the tactic language (see :ref:`ltac`). The code is +now much shorter and a significant increase in performance has been noticed. +The general behavior with respect to dependent types, unfolding and +introductions has slightly changed to get clearer semantics. This may lead to +some incompatibilities. + +.. tacv:: intuition + + Is equivalent to :g:`intuition auto with *`. + +.. tacv:: dintuition + :name: dintuition + + While :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. + +.. flag:: Intuition Negation Unfolding + + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. This flag is on by default. + +.. tacn:: rtauto + :name: rtauto + + The :tacn:`rtauto` tactic solves propositional tautologies similarly to what + :tacn:`tauto` does. The main difference is that the proof term is built using a + reflection scheme applied to a sequent calculus proof of the goal. The search + procedure is also implemented using a different technique. + + Users should be aware that this difference may result in faster proof-search + but slower proof-checking, and :tacn:`rtauto` might not solve goals that + :tacn:`tauto` would be able to solve (e.g. goals involving universal + quantifiers). + + Note that this tactic is only available after a ``Require Import Rtauto``. + +.. tacn:: firstorder + :name: firstorder + + The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to + first- order reasoning, written by Pierre Corbineau. It is not restricted to + usual logical connectives but instead may reason about any first-order class + inductive definition. + +.. opt:: Firstorder Solver @tactic + :name: Firstorder Solver + + The default tactic used by :tacn:`firstorder` when no rule applies is + :g:`auto with core`, it can be reset locally or globally using this option. + + .. cmd:: Print Firstorder Solver + + Prints the default tactic used by :tacn:`firstorder` when no rule applies. + +.. tacv:: firstorder @tactic + + Tries to solve the goal with :n:`@tactic` when no logical rule may apply. + +.. tacv:: firstorder using {+ @qualid} + + .. deprecated:: 8.3 + + Use the syntax below instead (with commas). + +.. tacv:: firstorder using {+, @qualid} + + Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` + refers to an inductive type, it is the collection of its constructors which are + added to the proof-search environment. + +.. tacv:: firstorder with {+ @ident} + + Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search + environment. + +.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} + + This combines the effects of the different variants of :tacn:`firstorder`. + +.. opt:: Firstorder Depth @natural + :name: Firstorder Depth + + This option controls the proof-search depth bound. + +.. tacn:: congruence + :name: congruence + + The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard + Nelson and Oppen congruence closure algorithm, which is a decision procedure + for ground equalities with uninterpreted symbols. It also includes + constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal + is a non-quantified equality, congruence tries to prove it with non-quantified + equalities in the context. Otherwise it tries to infer a discriminable equality + from those in the context. Alternatively, congruence tries to prove that a + hypothesis is equal to the goal or to the negation of another hypothesis. + + :tacn:`congruence` is also able to take advantage of hypotheses stating + quantified equalities, but you have to provide a bound for the number of extra + equalities generated that way. Please note that one of the sides of the + equality must contain all the quantified variables in order for congruence to + match against it. + +.. example:: + + .. coqtop:: reset all + + Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. + intros. + congruence. + Qed. + + Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. + intros. + congruence. + Qed. + +.. tacv:: congruence @natural + + Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`natural` does not make + success slower, only failure. You might consider adding some lemmas as + hypotheses using assert in order for :tacn:`congruence` to use them. + +.. tacv:: congruence with {+ @term} + :name: congruence with + + Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps + in case you have partially applied constructors in your goal. + +.. exn:: I don’t know how to handle dependent equality. + + The decision procedure managed to find a proof of the goal or of a + discriminable equality but this proof could not be built in |Coq| because of + dependently-typed functions. + +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. + + The decision procedure could solve the goal with the provision that additional + arguments are supplied for some partially applied constructors. Any term of an + appropriate type will allow the tactic to successfully solve the goal. Those + additional arguments can be given to congruence by filling in the holes in the + terms given in the error message, using the :tacn:`congruence with` variant described above. + +.. flag:: Congruence Verbose + + This flag makes :tacn:`congruence` print debug information. + +.. tacn:: btauto + :name: btauto + + The tactic :tacn:`btauto` implements a reflexive solver for boolean + tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are + constructed over the following grammar: + + .. prodn:: + btauto_term ::= @ident + | true + | false + | orb @btauto_term @btauto_term + | andb @btauto_term @btauto_term + | xorb @btauto_term @btauto_term + | negb @btauto_term + | if @btauto_term then @btauto_term else @btauto_term + + Whenever the formula supplied is not a tautology, it also provides a + counter-example. + + Internally, it uses a system very similar to the one of the ring + tactic. + + Note that this tactic is only available after a ``Require Import Btauto``. + + .. exn:: Cannot recognize a boolean equality. + + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. + +.. tacv:: field + field_simplify {* @term} + field_simplify_eq + + The field tactic is built on the same ideas as ring: this is a + reflexive tactic that solves or simplifies equations in a field + structure. The main idea is to reduce a field expression (which is an + extension of ring expressions with the inverse and division + operations) to a fraction made of two polynomial expressions. + + Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` + replaces the provided terms by their reduced fraction. + :n:`field_simplify_eq` applies when the conclusion is an equation: it + simplifies both hand sides and multiplies so as to cancel + denominators. So it produces an equation without division nor inverse. + + All of these 3 tactics may generate a subgoal in order to prove that + denominators are different from zero. + + See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to + declare new field structures. All declared field structures can be + printed with the Print Fields command. + +.. example:: + + .. coqtop:: reset all + + Require Import Reals. + Goal forall x y:R, + (x * y > 0)%R -> + (x * (1 / x + x / (x + y)))%R = + ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. + + intros; field. + +.. seealso:: + + File plugins/ring/RealField.v for an example of instantiation, + theory theories/Reals for many examples of use of field. diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 3f5526dba8..1c7fd050f1 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -1,8 +1,8 @@ .. _writing-proofs: -============== -Writing proofs -============== +=================== +Basic proof writing +=================== |Coq| is an interactive theorem prover, or proof assistant, which means that proofs can be constructed interactively through a dialog between @@ -27,8 +27,9 @@ flavors of tactics, including the SSReflect proof language. .. toctree:: :maxdepth: 1 - ../../proof-engine/proof-handling + proof-mode ../../proof-engine/tactics + rewriting ../../proof-engine/ssreflect-proof-language ../../proof-engine/detailed-tactic-examples ../../user-extensions/proof-schemes diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst new file mode 100644 index 0000000000..b74c9d3a23 --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -0,0 +1,1037 @@ +.. _proofhandling: + +------------------- + Proof handling +------------------- + +In |Coq|’s proof editing mode all top-level commands documented in +Chapter :ref:`vernacularcommands` remain available and the user has access to specialized +commands dealing with proof development pragmas documented in this +section. They can also use some other specialized commands called +*tactics*. They are the very tools allowing the user to deal with +logical reasoning. They are documented in Chapter :ref:`tactics`. + +|Coq| user interfaces usually have a way of marking whether the user has +switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into +:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. + +At each stage of a proof development, one has a list of goals to +prove. Initially, the list consists only in the theorem itself. After +having applied some tactics, the list of goals contains the subgoals +generated by the tactics. + +To each subgoal is associated a number of hypotheses called the *local context* +of the goal. Initially, the local context contains the local variables and +hypotheses of the current section (see Section :ref:`gallina-assumptions`) and +the local variables and hypotheses of the theorem statement. It is enriched by +the use of certain tactics (see e.g. :tacn:`intro`). + +When a proof is completed, the message ``Proof completed`` is displayed. +One can then register this proof as a defined constant in the +environment. Because there exists a correspondence between proofs and +terms of λ-calculus, known as the *Curry-Howard isomorphism* +:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those +terms are called *proof terms*. + + +.. exn:: No focused proof. + + |Coq| raises this error message when one attempts to use a proof editing command + out of the proof editing mode. + +.. _proof-editing-mode: + +Entering and leaving proof editing mode +--------------------------------------- + +The proof editing mode is entered by asserting a statement, which typically is +the assertion of a theorem using an assertion command like :cmd:`Theorem`. The +list of assertion commands is given in :ref:`Assertions`. The command +:cmd:`Goal` can also be used. + +.. cmd:: Goal @type + + This is intended for quick assertion of statements, without knowing in + advance which name to give to the assertion, typically for quick + testing of the provability of a statement. If the proof of the + statement is eventually completed and validated, the statement is then + bound to the name ``Unnamed_thm`` (or a variant of this name not already + used for another statement). + +.. cmd:: Qed + + This command is available in interactive editing proof mode when the + proof is completed. Then :cmd:`Qed` extracts a proof term from the proof + script, switches back to |Coq| top-level and attaches the extracted + proof term to the declared name of the original goal. The name is + added to the environment as an opaque constant. + + .. exn:: Attempt to save an incomplete proof. + :undocumented: + + .. note:: + + Sometimes an error occurs when building the proof term, because + tactics do not enforce completely the term construction + constraints. + + The user should also be aware of the fact that since the + proof term is completely rechecked at this point, one may have to wait + a while when the proof is large. In some exceptional cases one may + even incur a memory overflow. + +.. cmd:: Save @ident + :name: Save + + Saves a completed proof with the name :token:`ident`, which + overrides any name provided by the :cmd:`Theorem` command or + its variants. + +.. cmd:: Defined {? @ident } + + Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means + that its content can be explicitly used for type checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). If :token:`ident` is specified, + the proof is defined with the given name, which overrides any name + provided by the :cmd:`Theorem` command or its variants. + +.. cmd:: Admitted + + This command is available in interactive editing mode to give up + the current proof and declare the initial goal as an axiom. + +.. cmd:: Abort {? {| All | @ident } } + + Cancels the current proof development, switching back to + the previous proof development, or to the |Coq| toplevel if no other + proof was being edited. + + :n:`@ident` + Aborts editing the proof named :n:`@ident` for use when you have + nested proofs. See also :flag:`Nested Proofs Allowed`. + + :n:`All` + Aborts all current proofs. + + .. exn:: No focused proof (No proof-editing in progress). + :undocumented: + +.. cmd:: Proof @term + :name: Proof `term` + + This command applies in proof editing mode. It is equivalent to + :n:`exact @term. Qed.` + That is, you have to give the full proof in one gulp, as a + proof term (see Section :ref:`applyingtheorems`). + + .. warning:: + + Use of this command is discouraged. In particular, it + doesn't work in Proof General because it must + immediately follow the command that opened proof mode, but + Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see + `Proof General issue #498 + <https://github.com/ProofGeneral/PG/issues/498>`_). + +.. cmd:: Proof + + Is a no-op which is useful to delimit the sequence of tactic commands + which start a proof, after a :cmd:`Theorem` command. It is a good practice to + use :cmd:`Proof` as an opening parenthesis, closed in the script with a + closing :cmd:`Qed`. + + .. seealso:: :cmd:`Proof with` + +.. cmd:: Proof using @section_var_expr {? with @ltac_expr } + + .. insertprodn section_var_expr starred_ident_ref + + .. prodn:: + section_var_expr ::= {* @starred_ident_ref } + | {? - } @section_var_expr50 + section_var_expr50 ::= @section_var_expr0 - @section_var_expr0 + | @section_var_expr0 + @section_var_expr0 + | @section_var_expr0 + section_var_expr0 ::= @starred_ident_ref + | ( @section_var_expr ) {? * } + starred_ident_ref ::= @ident {? * } + | Type {? * } + | All + + Opens proof editing mode, declaring the set of + section variables (see :ref:`gallina-assumptions`) used by the proof. + At :cmd:`Qed` time, the + system verifies that the set of section variables used in + the proof is a subset of the declared one. + + The set of declared variables is closed under type dependency. For + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. + + The set of declared variables always includes the variables used by + the statement. In other words ``Proof using e`` is equivalent to + ``Proof using Type + e`` for any declaration expression ``e``. + + :n:`- @section_var_expr50` + Use all section variables except those specified by :n:`@section_var_expr50` + + :n:`@section_var_expr0 + @section_var_expr0` + Use section variables from the union of both collections. + See :ref:`nameaset` to see how to form a named collection. + + :n:`@section_var_expr0 - @section_var_expr0` + Use section variables which are in the first collection but not in the + second one. + + :n:`{? * }` + Use the transitive closure of the specified collection. + + :n:`Type` + Use only section variables occurring in the statement. Specifying :n:`*` + uses the forward transitive closure of all the section variables occurring + in the statement. For example, if the variable ``H`` has type ``p < 5`` then + ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``. + + :n:`All` + Use all section variables. + + .. seealso:: :ref:`tactics-implicit-automation` + +.. attr:: using + + This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`, + :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and + its variants. It takes + a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to + specifying the same :n:`@section_var_expr` in + :cmd:`Proof using`. + + .. example:: + + .. coqtop:: all + + Section Test. + Variable n : nat. + Hypothesis Hn : n <> 0. + + #[using="Hn"] + Lemma example : 0 < n. + + .. coqtop:: in + + Abort. + End Test. + + +Proof using options +``````````````````` + +The following options modify the behavior of ``Proof using``. + + +.. opt:: Default Proof Using "@section_var_expr" + :name: Default Proof Using + + Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default + Proof Using "a b"`` will complete all ``Proof`` commands not followed by a + ``using`` part with ``using a b``. + + +.. flag:: Suggest Proof Using + + When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not + provide one. + +.. _`nameaset`: + +Name a set of section hypotheses for ``Proof using`` +```````````````````````````````````````````````````` + +.. cmd:: Collection @ident := @section_var_expr + + This can be used to name a set of section + hypotheses, with the purpose of making ``Proof using`` annotations more + compact. + + .. example:: + + Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: + + Collection Some := x y z. + + Define the collection named ``Fewer`` containing only ``x`` and ``y``:: + + Collection Fewer := Some - z + + Define the collection named ``Many`` containing the set union or set + difference of ``Fewer`` and ``Some``:: + + Collection Many := Fewer + Some + Collection Many := Fewer - Some + + Define the collection named ``Many`` containing the set difference of + ``Fewer`` and the unnamed collection ``x y``:: + + Collection Many := Fewer - (x y) + + + +.. cmd:: Existential @natural {? : @type } := @term + + This command instantiates an existential variable. :token:`natural` is an index in + the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. + + This command is intended to be used to instantiate existential + variables when the proof is completed but some uninstantiated + existential variables remain. To instantiate existential variables + during proof edition, you should use the tactic :tacn:`instantiate`. + +.. cmd:: Grab Existential Variables + + This command can be run when a proof has no more goal to be solved but + has remaining uninstantiated existential variables. It takes every + uninstantiated existential variable and turns it into a goal. + +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. All proof modes support vernacular commands; the proof mode determines + which tactic language and set of tactic definitions are available. The + possible option values are: + + `"Classic"` + Activates the |Ltac| language and the tactics with the syntax documented + in this manual. + Some tactics are not available until the associated plugin is loaded, + such as `SSR` or `micromega`. + This proof mode is set when the :term:`prelude` is loaded. + + `"Noedit"` + No tactic + language is activated at all. This is the default when the :term:`prelude` + is not loaded, e.g. through the `-noinit` option for `coqc`. + + `"Ltac2"` + Activates the Ltac2 language and the Ltac2-specific variants of the documented + tactics. + This value is only available after :cmd:`Requiring <Require>` Ltac2. + :cmd:`Importing <Import>` Ltac2 sets this mode. + + Some external plugins also define their own proof mode, which can be + activated with this command. + +Navigation in the proof tree +-------------------------------- + +.. cmd:: Undo {? {? To } @natural } + + Cancels the effect of the last :token:`natural` commands or tactics. + The :n:`To @natural` form goes back to the specified state number. + If :token:`natural` is not specified, the command goes back one command or tactic. + +.. cmd:: Restart + + Restores the proof editing process to the original goal. + + .. exn:: No focused proof to restart. + :undocumented: + +.. cmd:: Focus {? @natural } + + Focuses the attention on the first subgoal to prove or, if :token:`natural` is + specified, the :token:`natural`\-th. The + printing of the other subgoals is suspended until the focused subgoal + is solved or unfocused. + + .. deprecated:: 8.8 + + Prefer the use of bullets or focusing brackets with a goal selector (see below). + +.. cmd:: Unfocus + + This command restores to focus the goal that were suspended by the + last :cmd:`Focus` command. + + .. deprecated:: 8.8 + +.. cmd:: Unfocused + + Succeeds if the proof is fully unfocused, fails if there are some + goals out of focus. + +.. _curly-braces: + +.. index:: { + } + +.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, + hence the verbose names + +.. tacn:: {? {| @natural | [ @ident ] } : } %{ + %} + + .. todo + See https://github.com/coq/coq/issues/12004 and + https://github.com/coq/coq/issues/12825. + + ``{`` (without a terminating period) focuses on the first + goal. The subproof can only be + unfocused when it has been fully solved (*i.e.*, when there is no + focused goal left). Unfocusing is then handled by ``}`` (again, without a + terminating period). See also an example in the next section. + + Note that when a focused goal is proved a message is displayed + together with a suggestion about the right bullet or ``}`` to unfocus it + or focus the next one. + + :n:`@natural:` + Focuses on the :token:`natural`\-th subgoal to prove. + + :n:`[ @ident ]: %{` + Focuses on the named goal :token:`ident`. + + .. note:: + + Goals are just existential variables and existential variables do not + get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: + + .. coqtop:: in + + Ltac name_goal name := refine ?[name]. + + .. seealso:: :ref:`existential-variables` + + .. example:: + + This first example uses the Ltac definition above, and the named goals + only serve for documentation. + + .. coqtop:: all + + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { + + .. coqtop:: all + + reflexivity. + + .. coqtop:: in + + } + + .. coqtop:: all + + [step]: { + + .. coqtop:: all + + simpl. + f_equal. + assumption. + } + Qed. + + This can also be a way of focusing on a shelved goal, for instance: + + .. coqtop:: all + + Goal exists n : nat, n = n. + eexists ?[x]. + reflexivity. + [x]: exact 0. + Qed. + + .. exn:: This proof is focused, but cannot be unfocused this way. + + You are trying to use ``}`` but the current subproof has not been fully solved. + + .. exn:: No such goal (@natural). + :undocumented: + + .. exn:: No such goal (@ident). + :undocumented: + + .. exn:: Brackets do not support multi-goal selectors. + + Brackets are used to focus on a single goal given either by its position + or by its name if it has one. + + .. seealso:: The error messages for bullets below. + +.. _bullets: + +Bullets +``````` + +Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The +use of a bullet ``b`` for the first time focuses on the first goal ``g``, the +same bullet cannot be used again until the proof of ``g`` is completed, +then it is mandatory to focus the next goal with ``b``. The consequence is +that ``g`` and all goals present when ``g`` was focused are focused with the +same bullet ``b``. See the example below. + +Different bullets can be used to nest levels. The scope of bullet does +not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further +nesting levels provided they are delimited by these. Bullets are made of +repeated ``-``, ``+`` or ``*`` symbols: + +.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } + +Note again that when a focused goal is proved a message is displayed +together with a suggestion about the right bullet or ``}`` to unfocus it +or focus the next one. + +.. note:: + + In Proof General (``Emacs`` interface to |Coq|), you must use + bullets with the priority ordering shown above to have a correct + indentation. For example ``-`` must be the outer bullet and ``**`` the inner + one in the example below. + +The following example script illustrates all these features: + +.. example:: + + .. coqtop:: all + + Goal (((True /\ True) /\ True) /\ True) /\ True. + Proof. + split. + - split. + + split. + ** { split. + - trivial. + - trivial. + } + ** trivial. + + trivial. + - assert True. + { trivial. } + assumption. + Qed. + +.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished. + + Before using bullet :n:`@bullet__1` again, you should first finish proving + the current focused goal. + Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same. + +.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here. + + You must put :n:`@bullet__2` to focus on the next goal. No other bullet is + allowed here. + +.. exn:: No such goal. Focus next goal with bullet @bullet. + + You tried to apply a tactic but no goals were under focus. + Using :n:`@bullet` is mandatory here. + +.. FIXME: the :noindex: below works around a Sphinx issue. + (https://github.com/sphinx-doc/sphinx/issues/4979) + It should be removed once that issue is fixed. + +.. exn:: No such goal. Try unfocusing with %}. + :noindex: + + You just finished a goal focused by ``{``, you must unfocus it with ``}``. + +Mandatory Bullets +~~~~~~~~~~~~~~~~~ + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + +Set Bullet Behavior +~~~~~~~~~~~~~~~~~~~ + +.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } + :name: Bullet Behavior + + This option controls the bullet behavior and can take two possible values: + + - "None": this makes bullets inactive. + - "Strict Subproofs": this makes bullets active (this is the default behavior). + +Modifying the order of goals +```````````````````````````` + +.. tacn:: cycle @integer + :name: cycle + + Reorders the selected goals so that the first :n:`@integer` goals appear after the + other selected goals. + If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the + beginning of the list. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent + to `all: cycle 1`. See :tacn:`… : … (goal selector)`. + +.. example:: + + .. coqtop:: none reset + + Parameter P : nat -> Prop. + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: cycle 2. + all: cycle -3. + +.. tacn:: swap @integer @integer + :name: swap + + Exchanges the position of the specified goals. + Negative values for :n:`@integer` indicate counting goals + backward from the end of the list of selected goals. Goals are indexed from 1. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent + to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. + +.. example:: + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: swap 1 3. + all: swap 1 -1. + +.. tacn:: revgoals + :name: revgoals + + Reverses the order of the selected goals. The tactic is only useful with a goal + selector, most commonly `all :`. Note that other selectors reorder goals; + `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. + + .. example:: + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: revgoals. + +Postponing the proof of some goals +`````````````````````````````````` + +.. tacn:: shelve + :name: shelve + + This tactic moves all goals under focus to a shelf. While on the + shelf, goals will not be focused on. They can be solved by + unification, or they can be called back into focus with the command + :cmd:`Unshelve`. + + .. tacv:: shelve_unifiable + :name: shelve_unifiable + + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. + + .. example:: + + .. coqtop:: all abort + + Goal exists n, n=0. + refine (ex_intro _ _ _). + all: shelve_unifiable. + reflexivity. + +.. cmd:: Unshelve + + This command moves all the goals on the shelf (see :tacn:`shelve`) + from the shelf into focus, by appending them to the end of the current + list of focused goals. + +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + +.. tacn:: give_up + :name: give_up + + This tactic removes the focused goals from the proof. They are not + solved, and cannot be solved later in the proof. As the goals are not + solved, the proof cannot be closed. + + The ``give_up`` tactic can be used while editing a proof, to choose to + write the proof script in a non-sequential order. + +.. _requestinginformation: + +Requesting information +---------------------- + + +.. cmd:: Show {? {| @ident | @natural } } + + Displays the current goals. + + :n:`@natural` + Display only the :token:`natural`\-th subgoal. + + :n:`@ident` + Displays the named goal :token:`ident`. This is useful in + particular to display a shelved goal but only works if the + corresponding existential variable has been named by the user + (see :ref:`existential-variables`) as in the following example. + + .. example:: + + .. coqtop:: all abort + + Goal exists n, n = 0. + eexists ?[n]. + Show n. + + .. exn:: No focused proof. + :undocumented: + + .. exn:: No such goal. + :undocumented: + +.. cmd:: Show Proof {? Diffs {? removed } } + + Displays the proof term generated by the tactics + that have been applied so far. If the proof is incomplete, the term + will contain holes, which correspond to subterms which are still to be + constructed. Each hole is an existential variable, which appears as a + question mark followed by an identifier. + + 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_proof_diffs`. + +.. cmd:: Show Conjectures + + Prints the names of all the + theorems that are currently being proved. As it is possible to start + proving a previous lemma during the proof of a theorem, there may + be multiple names. + +.. cmd:: Show Intro + + If the current goal begins by at least one product, + prints the name of the first product as it would be + generated by an anonymous :tacn:`intro`. The aim of this command is to ease + the writing of more robust scripts. For example, with an appropriate + Proof General macro, it is possible to transform any anonymous :tacn:`intro` + into a qualified one such as ``intro y13``. In the case of a non-product + goal, it prints nothing. + +.. cmd:: Show Intros + + Similar to the previous command. + Simulates the naming process of :tacn:`intros`. + +.. cmd:: Show Existentials + + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. + +.. cmd:: Show Match @qualid + + Displays a template of the Gallina :token:`match<term_match>` + construct with a branch for each constructor of the type + :token:`qualid`. This is used internally by + `company-coq <https://github.com/cpitclaudel/company-coq>`_. + + .. example:: + + .. coqtop:: all + + Show Match nat. + + .. exn:: Unknown inductive type. + :undocumented: + +.. cmd:: Show Universes + + Displays the set of all universe constraints and + its normalized form at the current stage of the proof, useful for + debugging universe inconsistencies. + +.. cmd:: Show Goal @natural at @natural + + Available in coqtop. Displays a goal at a + proof state using the goal ID number and the proof state ID number. + It is primarily for use by tools such as Prooftree that need to fetch + goal history in this way. Prooftree is a tool for visualizing a proof + as a tree that runs in Proof General. + +.. cmd:: Guarded + + Some tactics (e.g. :tacn:`refine`) allow to build proofs using + fixpoint or co-fixpoint constructions. Due to the incremental nature + of interactive proof construction, the check of the termination (or + guardedness) of the recursive calls in the fixpoint or cofixpoint + constructions is postponed to the time of the completion of the proof. + + The command :cmd:`Guarded` allows checking if the guard condition for + fixpoint and cofixpoint is violated at some time of the construction + of the proof without having to wait the completion of the proof. + +.. _showing_diffs: + +Showing differences between proof steps +--------------------------------------- + +|Coq| can automatically highlight the differences between successive proof steps +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 +to it. The second screenshot uses the "removed" option, so it shows the conclusion a +second time with the old text, with deletions marked in red. Also, since the hypotheses are +new, no line of old text is shown for them. + +.. comment screenshot produced with: + Inductive ev : nat -> Prop := + | ev_0 : ev 0 + | ev_SS : forall n : nat, ev n -> ev (S (S n)). + + Fixpoint double (n:nat) := + match n with + | O => O + | S n' => S (S (double n')) + end. + + Goal forall n, ev n -> exists k, n = double k. + intros n E. + +.. + + .. image:: ../../_static/diffs-coqide-on.png + :alt: |CoqIDE| with Set Diffs on + +.. + + .. image:: ../../_static/diffs-coqide-removed.png + :alt: |CoqIDE| with Set Diffs removed + +.. + + .. image:: ../../_static/diffs-coqtop-on3.png + :alt: coqtop with Set Diffs on + +This image shows an error message with diff highlighting in |CoqIDE|: + +.. + + .. image:: ../../_static/diffs-error-message.png + :alt: |CoqIDE| error message with diffs + +How to enable diffs +``````````````````` + +.. opt:: Diffs {| "on" | "off" | "removed" } + :name: Diffs + + The “on” setting highlights added tokens in green, while the “removed” setting + additionally reprints items with removed tokens in red. Unchanged tokens in + modified items are shown with pale green or red. Diffs in error messages + use red and green for the compared values; they appear regardless of the setting. + (Colors are user-configurable.) + +For coqtop, showing diffs can be enabled when starting coqtop with the +``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option +within |Coq|. You will need to provide the ``-color on|auto`` command-line option when +you start coqtop in either case. + +Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment +variable. See section :ref:`customization-by-environment-variables`. Diffs +use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. + +In |CoqIDE|, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in |CoqIDE|. You can change the background colors shown for diffs from the +``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, +``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also +lets you control other attributes of the highlights, such as the foreground +color, bold, italic, underline and strikeout. + +Proof General can also display |Coq|-generated proof diffs automatically. +Please see the PG documentation section +"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) +for details. + +How diffs are calculated +```````````````````````` + +Diffs are calculated as follows: + +1. Select the old proof state to compare to, which is the proof state before + the last tactic that changed the proof. Changes that only affect the view + of the proof, such as ``all: swap 1 2``, are ignored. + +2. For each goal in the new proof state, determine what old goal to compare + it to—the one it is derived from or is the same as. Match the hypotheses by + name (order is ignored), handling compacted items specially. + +3. For each hypothesis and conclusion (the “items”) in each goal, pass + them as strings to the lexer to break them into tokens. Then apply the + Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. + +Notes: + +* Aside from the highlights, output for the "on" option should be identical + to the undiffed output. +* Goals completed in the last proof step will not be shown even with the + "removed" setting. + +.. comment The following screenshots show diffs working with multiple goals and with compacted + hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at + all after the split because it has not changed. + + .. todo: Use this script and remove the screenshots when COQ_COLORS + works for coqtop in sphinx + .. coqtop:: none + + Set Diffs "on". + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3. + + .. coqtop:: out + + split. + + .. coqtop:: all abort + + 2: split. + + .. + + .. coqtop:: none + + Set Diffs "on". + Goal forall n m : nat, n + m = m + n. + Set Diffs "on". + + .. coqtop:: out + + intros n. + + .. coqtop:: all abort + + intros m. + +This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal +with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after +the split because it has not changed. + +.. + + .. image:: ../../_static/diffs-coqide-multigoal.png + :alt: coqide with Set Diffs on with multiple goals + +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 +------------------------------------------------ + + +.. opt:: Hyps Limit @natural + :name: Hyps Limit + + This option controls the maximum number of hypotheses displayed in goals + after the application of a tactic. All the hypotheses remain usable + in the proof development. + When unset, it goes back to the default mode which is to print all + available hypotheses. + + +.. flag:: Nested Proofs Allowed + + When turned on (it is off by default), this flag enables support for nested + proofs: a new assertion command can be inserted before the current proof is + finished, in which case |Coq| will temporarily switch to the proof of this + *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` + or :cmd:`Defined`), its statement will be made available (as if it had been + 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 +------------------------ + +.. cmd:: Print Debug GC + + Prints heap usage statistics, which are values from the `stat` type of the `Gc` module + described + `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ + in the |OCaml| documentation. + The `live_words`, `heap_words` and `top_heap_words` values give the basic information. + Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. + +When experiencing high memory usage the following commands can be used +to force |Coq| to optimize some of its internal data structures. + +.. cmd:: Optimize Proof + + Shrink the data structure used to represent the current proof. + + +.. cmd:: Optimize Heap + + Perform a heap compaction. This is generally an expensive operation. + See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + There is also an analogous tactic :tacn:`optimize_heap`. + +Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` +environment variable. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst new file mode 100644 index 0000000000..1358aad432 --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -0,0 +1,857 @@ +================================= +Term rewriting and simplification +================================= + +.. _rewritingexpressions: + +Rewriting expressions +--------------------- + +These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in +file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is +simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. + +.. tacn:: rewrite @term + :name: rewrite + + This tactic applies to any goal. The type of :token:`term` must have the form + + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` + + where :g:`eq` is the Leibniz equality or a registered setoid equality. + + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. + + .. exn:: The @term provided does not end with an equation. + :undocumented: + + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + :undocumented: + + .. tacv:: rewrite -> @term + + Is equivalent to :n:`rewrite @term` + + .. tacv:: rewrite <- @term + + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + + .. tacv:: rewrite @term in @goal_occurrences + + Analogous to :n:`rewrite @term` but rewriting is done following + the clause :token:`goal_occurrences`. For instance: + + + :n:`rewrite H in H'` will rewrite `H` in the hypothesis + ``H'`` instead of the current goal. + + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means + :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` + In particular a failure will happen if any of these three simpler tactics + fails. + + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses + :g:`H'` different from :g:`H`. + A success will happen as soon as at least one of these simpler tactics succeeds. + + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` + that succeeds if at least one of these two tactics succeeds. + + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. + + .. tacv:: rewrite @term at @occurrences + + Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. + + .. tacv:: rewrite @term by @tactic + + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. + + .. tacv:: rewrite {+, @orientation @term} {? in @ident } + + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. An :production:`orientation` + ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. + + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: + + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, + leading to failure if these :token:`natural` rewrites are not possible. + + .. tacv:: erewrite @term + :name: erewrite + + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. + + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + +.. tacn:: replace @term with @term’ + :name: replace + + This tactic applies to any goal. It replaces all free occurrences of :n:`@term` + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + + .. exn:: Terms do not have convertible types. + :undocumented: + + .. tacv:: replace @term with @term’ by @tactic + + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. + + .. tacv:: replace @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. + + .. tacv:: replace -> @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` + + .. tacv:: replace <- @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` + + .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} + replace -> @term in @goal_occurrences + replace <- @term in @goal_occurrences + + Acts as before but the replacements take place in the specified clauses + (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not + only in the conclusion of the goal. The clause argument must not contain + any ``type of`` nor ``value of``. + +.. tacn:: subst @ident + :name: subst + + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. + + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. + + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. + + .. tacv:: subst {+ @ident} + + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + + .. tacv:: subst + + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. + + .. flag:: Regular Subst Tactic + + This flag controls the behavior of :tacn:`subst`. When it is + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the flag, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the flag would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + flag would be a cause of failure of :tacn:`subst`. + + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the flag it may break. + default. + + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + + +.. tacn:: stepl @term + :name: stepl + + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. + + .. cmd:: Declare Left Step @term + + Adds :n:`@term` to the database used by :tacn:`stepl`. + + This tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). + + .. tacv:: stepl @term by @tactic + + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. + + .. tacv:: stepr @term by @tactic + :name: stepr + + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. + + .. cmd:: Declare Right Step @term + + Adds :n:`@term` to the database used by :tacn:`stepr`. + + +.. tacn:: change @term + :name: change + + This tactic applies to any goal. It implements the rule ``Conv`` given in + :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` + with `U` providing that `U` is well-formed and that `T` and `U` are + convertible. + + .. exn:: Not convertible. + :undocumented: + + .. tacv:: change @term with @term’ + + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. + + .. tacv:: change @term at {+ @natural} with @term’ + + This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. + + .. exn:: Too few occurrences. + :undocumented: + + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + + .. seealso:: :ref:`Performing computations <performingcomputations>` + +.. _performingcomputations: + +Performing computations +--------------------------- + +.. insertprodn red_expr pattern_occ + +.. prodn:: + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @reference } ] + strategy_flag ::= {+ @red_flag } + | @delta_flag + red_flag ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @reference {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @natural | @ident } } + | - {| @natural | @ident } {* @int_or_var } + int_or_var ::= @integer + | @ident + unfold_occ ::= @reference {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + +This set of tactics implements different specialized usages of the +tactic :tacn:`change`. + +All conversion tactics (including :tacn:`change`) can be parameterized by the +parts of the goal where the conversion can occur. This is done using +*goal clauses* which consists in a list of hypotheses and, optionally, +of a reference to the conclusion of the goal. For defined hypothesis +it is possible to specify if the conversion should occur on the type +part, the body part or both (default). + +Goal clauses are written after a conversion tactic (tactics :tacn:`set`, +:tacn:`rewrite`, :tacn:`replace` and :tacn:`autorewrite` also use goal +clauses) and are introduced by the keyword `in`. If no goal clause is +provided, the default is to perform the conversion only in the +conclusion. + +The syntax and description of the various goal clauses is the +following: + ++ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` ++ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the + conclusion ++ :n:`in * |-` in every hypothesis ++ :n:`in *` (equivalent to in :n:`* |- *`) everywhere ++ :n:`in (type of @ident) (value of @ident) ... |-` in type part of + :n:`@ident`, in the value part of :n:`@ident`, etc. + +For backward compatibility, the notation :n:`in {+ @ident}` performs +the conversion in hypotheses :n:`{+ @ident}`. + +.. tacn:: cbv {? @strategy_flag } + lazy {? @strategy_flag } + :name: cbv; lazy + + These parameterized reduction tactics apply to any goal and perform + the normalization of the goal according to the specified flags. In + correspondence with the kinds of reduction considered in |Coq| namely + :math:`\beta` (reduction of functional application), :math:`\delta` + (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), + :math:`\iota` (reduction of + pattern matching over a constructed term, and unfolding of :g:`fix` and + :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the + 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 + 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 + construction inside the :n:`@term` itself (use here the ``zeta`` flag). In + any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). + + Normalization according to the flags is done by first evaluating the + head of the expression into a *weak-head* normal form, i.e. until the + evaluation is blocked by a variable (or an opaque constant, or an + axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or + :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a + :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a + product type, a sort), or is a redex that the flags prevent to reduce. Once a + weak-head normal form is obtained, subterms are recursively reduced using the + same strategy. + + Reduction to weak-head normal form can be done using two strategies: + *lazy* (``lazy`` tactic), or *call-by-value* (``cbv`` tactic). The lazy + strategy is a call-by-need strategy, with sharing of reductions: the + arguments of a function call are weakly evaluated only when necessary, + and if an argument is used several times then it is weakly computed + only once. This reduction is efficient for reducing expressions with + dead code. For instance, the proofs of a proposition :g:`exists x. P(x)` + reduce to a pair of a witness :g:`t`, and a proof that :g:`t` satisfies the + predicate :g:`P`. Most of the time, :g:`t` may be computed without computing + the proof of :g:`P(t)`, thanks to the lazy strategy. + + The call-by-value strategy is the one used in ML languages: the + arguments of a function call are systematically weakly evaluated + first. Despite the lazy strategy always performs fewer reductions than + the call-by-value strategy, the latter is generally more efficient for + evaluating purely computational expressions (i.e. with little dead code). + +.. tacv:: compute + cbv + :name: compute; _ + + These are synonyms for ``cbv beta delta iota zeta``. + +.. tacv:: lazy + + This is a synonym for ``lazy beta delta iota zeta``. + +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. + +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. + +.. 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`. + +.. tacv:: vm_compute + :name: vm_compute + + 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 + :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. + +.. tacv:: native_compute + :name: native_compute + + 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 :tacn:`vm_compute`. Note however that the + compilation cost is higher, so it is worth using only for intensive + computations. + + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. + + .. flag:: NativeCompute Profiling + + On Linux, if you have the ``perf`` profiler installed, this flag makes + it possible to profile :tacn:`native_compute` evaluations. + + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename + + This option specifies the profile output; the default is + ``native_compute_profile.data``. The actual filename used + 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 + :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. + +.. flag:: Debug Cbv + + This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + information about the constants it encounters and the unfolding decisions it + makes. + +.. tacn:: red + :name: red + + This tactic applies to a goal that has the form:: + + forall (x:T1) ... (xk:Tk), T + + with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a + constant. If :g:`c` is transparent then it replaces :g:`c` with its + definition (say :g:`t`) and then reduces + :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. + +.. exn:: Not reducible. + :undocumented: + +.. exn:: No head constant to reduce. + :undocumented: + +.. tacn:: hnf + :name: hnf + + This tactic applies to any goal. It replaces the current goal with its + head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it + reduces the head of the goal until it becomes a product or an + irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. + The behavior of both :tacn:`hnf` can be tuned using the :cmd:`Arguments` command. + + Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. + +.. note:: + The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` + on transparency and opacity). + +.. tacn:: cbn + simpl + :name: cbn; simpl + + These tactics apply to any goal. They try to reduce a term to + something still readable instead of fully normalizing it. They perform + a sort of strong normalization with two key differences: + + + They unfold a constant if and only if it leads to a :math:`\iota`-reduction, + i.e. reducing a match or unfolding a fixpoint. + + While reducing a constant unfolding to (co)fixpoints, the tactics + use the name of the constant the (co)fixpoint comes from instead of + the (co)fixpoint definition in recursive calls. + + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. + + 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 :cmd:`Arguments` command. + + .. todo add "See <subsection about controlling the behavior of reduction strategies>" + to TBA section + + Notice that only transparent constants whose name can be reused in the + 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 :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} ] + + 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 + + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. + +.. tacv:: simpl @pattern at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences. + :undocumented: + +.. tacv:: simpl @qualid + simpl @string + + This applies :tacn:`simpl` only to the applicative subterms whose head occurrence + is the unfoldable constant :n:`@qualid` (the constant can be referred to by + its notation using :n:`@string` if such a notation exists). + +.. tacv:: simpl @qualid at {+ @natural} + simpl @string at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose + head occurrence is :n:`@qualid` (or :n:`@string`). + +.. flag:: Debug RAKAM + + This flag makes :tacn:`cbn` print various debugging information. + ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. + +.. tacn:: unfold @qualid + :name: unfold + + This tactic applies to any goal. The argument qualid must denote a + defined transparent constant or local definition (see + :ref:`gallina-definitions` and + :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. + + .. exn:: Cannot coerce @qualid to an evaluable reference. + + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. + + .. example:: + + .. coqtop:: abort all fail + + Goal 0 <= 1. + unfold le. + + This error can also be raised if you are trying to unfold + something that has been marked as opaque. + + .. example:: + + .. coqtop:: abort all fail + + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. + + .. tacv:: unfold @qualid in @goal_occurrences + + Replaces :n:`@qualid` in hypothesis (or hypotheses) designated + by :token:`goal_occurrences` with its definition and replaces + the hypothesis with its :math:`\beta`:math:`\iota` normal form. + + .. tacv:: unfold {+, @qualid} + + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. + + .. tacv:: unfold {+, @qualid at @occurrences } + + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. + + .. exn:: Bad occurrence number of @qualid. + :undocumented: + + .. exn:: @qualid does not occur. + :undocumented: + + .. tacv:: unfold @string + + If :n:`@string` denotes the discriminating symbol of a notation + (e.g. "+") or an expression defining a notation (e.g. `"_ + + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. + + .. tacv:: unfold @string%@ident + + This is variant of :n:`unfold @string` where :n:`@string` gets + its interpretation from the scope bound to the delimiting key + :token:`ident` instead of its default interpretation (see + :ref:`Localinterpretationrulesfornotations`). + + .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } + + This is the most general form. + +.. tacn:: fold @term + :name: fold + + This tactic applies to any goal. The term :n:`@term` is reduced using the + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. + + .. example:: + + .. coqtop:: all abort + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. tacv:: fold {+ @term} + + Equivalent to :n:`fold @term ; ... ; fold @term`. + +.. tacn:: pattern @term + :name: pattern + + This command applies to any goal. The argument :n:`@term` must be a free + subterm of the current goal. The command pattern performs :math:`\beta`-expansion + (the inverse of :math:`\beta`-reduction) of the current goal (say :g:`T`) by + + + replacing all occurrences of :n:`@term` in :g:`T` with a fresh variable + + abstracting this variable + + applying the abstracted goal to :n:`@term` + + For instance, if the current goal :g:`T` is expressible as + :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` + in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into + :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for + instance, when the tactic ``apply`` fails on matching. + +.. tacv:: pattern @term at {+ @natural} + + Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for + :math:`\beta`-expansion. Occurrences are located from left to right. + +.. tacv:: pattern @term at - {+ @natural} + + All occurrences except the occurrences of indexes :n:`{+ @natural }` + of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from + left to right. + +.. tacv:: pattern {+, @term} + + Starting from a goal :math:`\varphi`:g:`(t`:sub:`1` :g:`... t`:sub:`m`:g:`)`, + the tactic :n:`pattern t`:sub:`1`:n:`, ..., t`:sub:`m` generates the + equivalent goal + :g:`(fun (x`:sub:`1`:g:`:A`:sub:`1`:g:`) ... (x`:sub:`m` :g:`:A`:sub:`m` :g:`) =>`:math:`\varphi`:g:`(x`:sub:`1` :g:`... x`:sub:`m` :g:`)) t`:sub:`1` :g:`... t`:sub:`m`. + If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these + occurrences will also be considered and possibly abstracted. + +.. tacv:: pattern {+, @term at {+ @natural}} + + This behaves as above but processing only the occurrences :n:`{+ @natural}` of + :n:`@term` starting from :n:`@term`. + +.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} + + This is the most general syntax that combines the different variants. + +.. tacn:: with_strategy @strategy_level_or_var [ {+ @reference } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + with_strategy transparent [id] unfold id. + + .. warning:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort fail + + exact I. + Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + <https://github.com/coq/coq/issues/12200>`_ for more details. + +Conversion tactics applied to hypotheses +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. tacn:: @tactic in {+, @ident} + + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. + + If :token:`ident` is a local definition, then :token:`ident` can be replaced by + :n:`type of @ident` to address not the body but the type of the local + definition. + + Example: :n:`unfold not in (type of H1) (type of H3)`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 06018304ab..9d1fcc160d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1386,7 +1386,7 @@ Scopes` or :cmd:`Print Scope`. ``char_scope`` This scope includes interpretation for all strings of the form ``"c"`` where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is - a three-digits number (possibly with leading 0's), or of the form + a three-digit number (possibly with leading 0s), or of the form ``""""``. Their respective denotations are the ASCII code of :g:`c`, the decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e. the ASCII code 34), all of them being represented in the type :g:`ascii`. @@ -1553,16 +1553,18 @@ numbers (see :ref:`datatypes`). Number notations ~~~~~~~~~~~~~~~~ -.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } +.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name :name: Number Notation - .. insertprodn numeral_modifier numeral_modifier + .. insertprodn number_modifier number_string_via .. prodn:: - numeral_modifier ::= ( warning after @bignat ) - | ( abstract after @bignat ) + number_modifier ::= warning after @bignat + | abstract after @bignat + | @number_string_via + number_string_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ] - This command allows the user to customize the way numeral literals + This command allows the user to customize the way number literals are parsed and printed. :n:`@qualid__type` @@ -1571,32 +1573,32 @@ Number notations parsing and printing functions, respectively. The parsing function :n:`@qualid__parse` should have one of the following types: - * :n:`Numeral.int -> @qualid__type` - * :n:`Numeral.int -> option @qualid__type` - * :n:`Numeral.uint -> @qualid__type` - * :n:`Numeral.uint -> option @qualid__type` + * :n:`Number.int -> @qualid__type` + * :n:`Number.int -> option @qualid__type` + * :n:`Number.uint -> @qualid__type` + * :n:`Number.uint -> option @qualid__type` * :n:`Z -> @qualid__type` * :n:`Z -> option @qualid__type` - * :n:`Numeral.numeral -> @qualid__type` - * :n:`Numeral.numeral -> option @qualid__type` + * :n:`Number.number -> @qualid__type` + * :n:`Number.number -> option @qualid__type` And the printing function :n:`@qualid__print` should have one of the following types: - * :n:`@qualid__type -> Numeral.int` - * :n:`@qualid__type -> option Numeral.int` - * :n:`@qualid__type -> Numeral.uint` - * :n:`@qualid__type -> option Numeral.uint` + * :n:`@qualid__type -> Number.int` + * :n:`@qualid__type -> option Number.int` + * :n:`@qualid__type -> Number.uint` + * :n:`@qualid__type -> option Number.uint` * :n:`@qualid__type -> Z` * :n:`@qualid__type -> option Z` - * :n:`@qualid__type -> Numeral.numeral` - * :n:`@qualid__type -> option Numeral.numeral` + * :n:`@qualid__type -> Number.number` + * :n:`@qualid__type -> option Number.number` .. deprecated:: 8.12 - Numeral notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by numeral - notations on :g:`Numeral.uint`, :g:`Numeral.int` and - :g:`Numeral.numeral`. + Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and + :g:`Decimal.decimal` are replaced respectively by number + notations on :g:`Number.uint`, :g:`Number.int` and + :g:`Number.number`. When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes @@ -1606,7 +1608,44 @@ Number notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. - :n:`( warning after @bignat )` + .. _number-string-via: + + :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` + When using this option, :n:`@qualid__type` no + longer needs to be an inductive type and is instead mapped to the + inductive type :n:`@qualid__ind` according to the provided + list of pairs, whose first component :n:`@qualid__constant` is a + constant of type :n:`@qualid__type` + (or a function of type :n:`{* _ -> } @qualid__type`) and the second a + constructor of type :n:`@qualid__ind`. The type + :n:`@qualid__type` is then replaced by :n:`@qualid__ind` in the + above parser and printer types. + + When :n:`@qualid__constant` is surrounded by square brackets, + all the implicit arguments of :n:`@qualid__constant` (whether maximally inserted or not) are ignored + when translating to :n:`@qualid__constructor` (i.e., before + applying :n:`@qualid__print`) and replaced with implicit + argument holes :g:`_` when translating from + :n:`@qualid__constructor` to :n:`@qualid__constant` (after + :n:`@qualid__parse`). See below for an :ref:`example <example-number-notation-implicit-args>`. + + .. note:: + The implicit status of the arguments is considered + only at notation declaration time, any further + modification of this status has no impact + on the previously declared notations. + + .. note:: + In case of multiple implicit options (for instance + :g:`Arguments eq_refl {A}%type_scope {x}, [_] _`), an + argument is considered implicit when it is implicit in any of the + options. + + .. note:: + To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation <Abbreviations>` + as in the :ref:`example below <example-number-notation-non-inductive>`. + + :n:`warning after @bignat` displays a warning message about a possible stack overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`. @@ -1616,11 +1655,11 @@ Number notations with :n:`(warning after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. - :n:`( abstract after @bignat )` + :n:`abstract after @bignat` returns :n:`(@qualid__parse m)` when parsing a literal :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a - :g:`Numeral.int`, :g:`Numeral.uint`, :g:`Z` or :g:`Numeral.numeral`, depending on the + :g:`Number.int`, :g:`Number.uint`, :g:`Z` or :g:`Number.number`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a @@ -1642,76 +1681,94 @@ Number notations As noted above, the :n:`(abstract after @natural)` directive has no effect when :n:`@qualid__parse` lands in an :g:`option` type. + .. exn:: 'via' and 'abstract' cannot be used together. + + With the :n:`abstract after` option, the parser function + :n:`@qualid__parse` does not reduce large numbers to a normal form, + which prevents doing the translation given in the :n:`mapping` list. + .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support + The number notation registered for :token:`type` does not support the given number. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. - .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The parsing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. exn:: @qualid__print should go from @type to Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The printing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a number notation. Parsing functions must always return ground terms, made up of - applications of constructors, inductive types, and primitive + function application, constructors, inductive type families, sorts and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a number notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a concrete number expressed as a (hexa)decimal. They may not return opaque constants. + .. exn:: Multiple 'via' options. + + At most one :g:`via` option can be given. + + .. exn:: Multiple 'warning after' or 'abstract after' options. + + At most one :g:`warning after` or :g:`abstract after` option can be given. + .. _string-notations: String notations ~~~~~~~~~~~~~~~~ -.. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name +.. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name :name: String Notation Allows the user to customize how strings are parsed and printed. - The token :n:`@qualid` should be the name of an inductive type, - while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@qualid__parse` should have one of the following types: + :n:`@qualid__type` + the name of an inductive type, + while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@qualid__parse` should have one of the following types: - * :n:`Byte.byte -> @qualid` - * :n:`Byte.byte -> option @qualid` - * :n:`list Byte.byte -> @qualid` - * :n:`list Byte.byte -> option @qualid` + * :n:`Byte.byte -> @qualid__type` + * :n:`Byte.byte -> option @qualid__type` + * :n:`list Byte.byte -> @qualid__type` + * :n:`list Byte.byte -> option @qualid__type` - The printing function :n:`@qualid__print` should have one of the - following types: + The printing function :n:`@qualid__print` should have one of the + following types: - * :n:`@qualid -> Byte.byte` - * :n:`@qualid -> option Byte.byte` - * :n:`@qualid -> list Byte.byte` - * :n:`@qualid -> option (list Byte.byte)` + * :n:`@qualid__type -> Byte.byte` + * :n:`@qualid__type -> option Byte.byte` + * :n:`@qualid__type -> list Byte.byte` + * :n:`@qualid__type -> option (list Byte.byte)` - When parsing, the application of the parsing function - :n:`@qualid__parse` to the string will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@qualid__parse` to the string will be fully reduced, and universes + of the resulting term will be refreshed. - Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. - .. exn:: Cannot interpret this string as a value of type @type + :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` + works as for :ref:`number notations above <number-string-via>`. + + .. exn:: Cannot interpret this string as a value of type @type The string notation registered for :token:`type` does not support the given string. This error is given when the interpretation @@ -1730,7 +1787,7 @@ String notations .. exn:: Unexpected term @term while parsing a string notation. Parsing functions must always return ground terms, made up of - applications of constructors, inductive types, and primitive + function application, constructors, inductive type families, sorts and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. @@ -1741,16 +1798,37 @@ String notations concrete string expressed as a decimal. They may not return opaque constants. -The following errors apply to both string and numeral notations: +.. note:: + Number or string notations for parameterized inductive types can be + added by declaring an :ref:`abbreviation <Abbreviations>` for the + inductive which instantiates all parameters. See :ref:`example below <example-string-notation-parameterized-inductive>`. + +The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. - String and numeral notations can only be declared for inductive types with no - arguments. + String and number notations can only be declared for inductive types. + Declare string or numeral notations for non-inductive types using :n:`@number_string_via`. + + .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid + + Duplicates are not allowed in the :n:`mapping` list. + + .. exn:: Missing mapping for constructor @qualid + + A mapping should be provided for :n:`@qualid` in the :n:`mapping` list. + + .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation. + + Two pairs in the :n:`mapping` list associate types that might be incompatible. + + .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation. + + A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. - The inductive type used to register the string or numeral notation is no + The inductive type used to register the string or number notation is no longer available in the environment. Most likely, this is because the notation was declared inside a functor for an inductive type inside the functor. This use case is not currently @@ -1779,6 +1857,198 @@ The following errors apply to both string and numeral notations: .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703 +.. example:: Number Notation for radix 3 + + The following example parses and prints natural numbers + whose digits are :g:`0`, :g:`1` or :g:`2` as terms of the following + inductive type encoding radix 3 numbers. + + .. coqtop:: in reset + + Inductive radix3 : Set := + | x0 : radix3 + | x3 : radix3 -> radix3 + | x3p1 : radix3 -> radix3 + | x3p2 : radix3 -> radix3. + + We first define a parsing function + + .. coqtop:: in + + Definition of_uint_dec (u : Decimal.uint) : option radix3 := + let fix f u := match u with + | Decimal.Nil => Some x0 + | Decimal.D0 u => match f u with Some u => Some (x3 u) | None => None end + | Decimal.D1 u => match f u with Some u => Some (x3p1 u) | None => None end + | Decimal.D2 u => match f u with Some u => Some (x3p2 u) | None => None end + | _ => None end in + f (Decimal.rev u). + Definition of_uint (u : Number.uint) : option radix3 := + match u with Number.UIntDecimal u => of_uint_dec u | Number.UIntHexadecimal _ => None end. + + and a printing function + + .. coqtop:: in + + Definition to_uint_dec (x : radix3) : Decimal.uint := + let fix f x := match x with + | x0 => Decimal.Nil + | x3 x => Decimal.D0 (f x) + | x3p1 x => Decimal.D1 (f x) + | x3p2 x => Decimal.D2 (f x) end in + Decimal.rev (f x). + Definition to_uint (x : radix3) : Number.uint := Number.UIntDecimal (to_uint_dec x). + + before declaring the notation + + .. coqtop:: in + + Declare Scope radix3_scope. + Open Scope radix3_scope. + Number Notation radix3 of_uint to_uint : radix3_scope. + + We can check the printer + + .. coqtop:: all + + Check x3p2 (x3p1 x0). + + and the parser + + .. coqtop:: all + + Set Printing All. + Check 120. + + Digits other than :g:`0`, :g:`1` and :g:`2` are rejected. + + .. coqtop:: all fail + + Check 3. + +.. _example-number-notation-non-inductive: + +.. example:: Number Notation for a non inductive type + + The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )` + as the number of units in the term. For instance :g:`sum unit (sum unit unit)` + is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. + The inductive :g:`I` will be used as :n:`@qualid__ind`. + + .. coqtop:: in reset + + Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. + + We then define :n:`@qualid__parse` and :n:`@qualid__print` + + .. coqtop:: in + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with + | O => Iempty | S O => Iunit + | S n => Isum Iunit (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with + | Iempty => O | Iunit => 1 + | Isum i1 i2 => f i1 + f i2 end in + Nat.to_num_uint (f x). + + Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. + + the number notation itself + + .. coqtop:: in + + Notation nSet := Set (only parsing). + Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope. + + and check the printer + + .. coqtop:: all + + Local Open Scope type_scope. + Check sum unit (sum unit unit). + + and the parser + + .. coqtop:: all + + Set Printing All. + Check 3. + +.. _example-number-notation-implicit-args: + +.. example:: Number Notation with implicit arguments + + The following example parses and prints natural numbers between + :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. + + .. coqtop:: all reset + + Require Import Vector. + Print Fin.t. + + Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`, + which won't appear in the corresponding inductive type. + + .. coqtop:: in + + Inductive I := I1 : I | IS : I -> I. + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with O => I1 | S n => IS (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with I1 => O | IS n => S (f n) end in + Nat.to_num_uint (f x). + + Declare Scope fin_scope. + Delimit Scope fin_scope with fin. + Local Open Scope fin_scope. + Number Notation Fin.t of_uint to_uint (via I + mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope. + + Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is + :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`. + + .. coqtop:: all + + Check 2. + + which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`) + + .. coqtop:: all + + Check 2 : Fin.t 3. + + but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`) + + .. coqtop:: all fail + + Check 2 : Fin.t 2. + +.. _example-string-notation-parameterized-inductive: + +.. example:: String Notation with a parameterized inductive type + + The parameter :g:`Byte.byte` for the parameterized inductive type + :g:`list` is given through an :ref:`abbreviation <Abbreviations>`. + + .. coqtop:: in reset + + Notation string := (list Byte.byte) (only parsing). + Definition id_string := @id string. + + String Notation string id_string id_string : list_scope. + + .. coqtop:: all + + Check "abc"%list. + .. _TacticNotation: Tactic Notations diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 4d2972ef8f..e4f0967794 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,3 +1,4 @@ +theories/Init/Numeral.v theories/btauto/Algebra.v theories/btauto/Btauto.v theories/btauto/Reflect.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7c1328916b..b08d7e9d2c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -22,7 +22,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Nat.v theories/Init/Decimal.v theories/Init/Hexadecimal.v - theories/Init/Numeral.v + theories/Init/Number.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v @@ -238,6 +238,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/DecimalN.v theories/Numbers/DecimalZ.v theories/Numbers/DecimalQ.v + theories/Numbers/DecimalR.v theories/Numbers/DecimalString.v theories/Numbers/HexadecimalFacts.v theories/Numbers/HexadecimalNat.v @@ -245,6 +246,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/HexadecimalN.v theories/Numbers/HexadecimalZ.v theories/Numbers/HexadecimalQ.v + theories/Numbers/HexadecimalR.v theories/Numbers/HexadecimalString.v </dd> diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f6a684bbd7..97d479b238 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,12 +1285,12 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "String" "Notation" reference reference reference ":" ident -| WITH "String" "Notation" reference reference reference ":" scope_name +| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident +| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name +| REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier +| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident +| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) | DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -numeral_modifier: [ -| OPTINREF -] - binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 @@ -2198,6 +2194,7 @@ ltac2_expr5: [ | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 | MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) +| MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | DELETE simple_tactic ] @@ -2464,6 +2461,9 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_string_mapping +| number_options +| string_option ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index b7f1e18d2b..92bcd51528 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) "plugins/ltac/g_eqdecide.mlg"; "plugins/ltac/g_tactic.mlg"; "plugins/ltac/g_ltac.mlg"; - "plugins/syntax/g_string.mlg"; "plugins/btauto/g_btauto.mlg"; "plugins/rtauto/g_rtauto.mlg"; "plugins/cc/g_congruence.mlg"; "plugins/firstorder/g_ground.mlg"; - "plugins/syntax/g_numeral.mlg"; + "plugins/syntax/g_number_string.mlg"; ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c764cb6f37..20ac8f8bf3 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,9 +686,9 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numeral_modifier -| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier -| "String" "Notation" reference reference reference ":" ident +| "Number" "Notation" reference reference reference OPT number_options ":" ident +| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| "String" "Notation" reference reference reference OPT string_option ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) @@ -2549,12 +2549,35 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numeral_modifier: [ +deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] +number_string_mapping: [ +| reference "=>" reference +| "[" reference "]" "=>" reference +] + +number_string_via: [ +| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]" +] + +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_string_via +] + +number_options: [ +| "(" LIST1 number_modifier SEP "," ")" +] + +string_option: [ +| "(" number_string_via ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) @@ -2586,6 +2609,7 @@ ltac2_expr5: [ | "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *) | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *) +| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | ltac2_expr4 (* Ltac2 plugin *) ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 12a7bc684d..75c0ca1453 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,6 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +908,9 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "String" "Notation" qualid qualid qualid ":" scope_name +| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name +| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier +| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] @@ -1269,11 +1269,22 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +deprecated_number_modifier: [ +| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_string_via +] + +number_string_via: [ +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" @@ -1640,6 +1651,7 @@ simple_tactic: [ | "ring" OPT ( "[" LIST1 one_term "]" ) | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) | "match" ltac2_expr5 "with" OPT ltac2_branches "end" +| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 | qualid LIST1 tactic_arg ] |