diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/logic.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 76 |
2 files changed, 55 insertions, 25 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 5aaded2726..3f1f5d46c5 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -194,9 +194,7 @@ Solvers for logic and equality additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the `with` clause. - .. flag:: Congruence Verbose - - Makes :tacn:`congruence` print debug information. + :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information. .. tacn:: btauto diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 8c8c88c526..4f937ad727 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings one_term_with_bindings ::= {? > } @one_term {? with @bindings } - Rewrites terms based on equalities. The type of :n:`@one_term` must have the form: + Replaces subterms with other subterms that have been proven to be equal. + The type of :n:`@one_term` must have the form: :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality. + .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3. + + where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`. Note that :n:`eq @term__1 @term__2` is typically written with the infix notation :n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`. @@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality Some of the variables :g:`x`\ :sub:`i` are solved by unification, and some of the types :n:`A__1, ..., A__n` may become new subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer - to variables bound by the `forall`; use :tacn:`setoid_rewrite` + to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite` if you want to find such occurrences. :n:`{+, @oriented_rewriter }` @@ -90,12 +93,55 @@ Rewriting with Leibniz and setoid equality any of them can be rewritten. If not specified, only the first occurrence in the conclusion is replaced. - If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. + .. note:: + + If :n:`at @occs_nums` is specified, rewriting is always done + with :ref:`setoid rewriting <generalizedrewriting>`, even for + Leibniz equality, which means that you must `Require + Setoid` to use that form. However, note that :tacn:`rewrite` + (even when using setoid rewriting) and :tacn:`setoid_rewrite` + don't behave identically (as is noted above and below). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. + .. note:: + + For each selected hypothesis and/or the conclusion, + :tacn:`rewrite` finds the first matching subterm in + depth-first search order. Only subterms identical to + that first matched subterm are rewritten. If the `at` clause is specified, + only these subterms are considered when counting occurrences. + To select a different set of matching subterms, you can + specify how some or all of the free variables are bound by + using a `with` clause (see :n:`@one_term_with_bindings`). + + For instance, if we want to rewrite the right-hand side in the + following goal, this will not work: + + .. coqtop:: none + + Require Import Arith. + + .. coqtop:: out + + Lemma example x y : x + y = y + x. + + .. coqtop:: all fail + + rewrite Nat.add_comm at 2. + + One can explicitly specify how some variables are bound to match + a different subterm: + + .. coqtop:: all abort + + rewrite Nat.add_comm with (m := x). + + Note that the more advanced :tacn:`setoid_rewrite` tactic + behaves differently, and thus the number of occurrences + available to rewrite may differ between the two tactics. + .. exn:: Tactic failure: Setoid library not loaded. :undocumented: @@ -338,13 +384,6 @@ Rewriting with definitional equality exact H. Qed. - .. tacn:: convert_concl_no_check @one_term - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. - .. _performingcomputations: Performing computations @@ -520,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`. 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 + :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -538,9 +575,6 @@ the conversion in hypotheses :n:`{+ @ident}`. 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: @@ -623,10 +657,8 @@ the conversion in hypotheses :n:`{+ @ident}`. 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. +:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information. +``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid :name: unfold |