Document how rewrite works regarding occurrence selection.

1 files changed, 51 insertions, 8 deletions

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 663337bc64..f316815e01 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 much more advanced :tacn:`setoid_rewrite`
    if you want to find such occurrences.
 
    :n:`{+, @oriented_rewriter }`
@@ -90,15 +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,
-     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 already mentioned above).
+     .. 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 the
+      matched one 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, it will not work like this:
+
+      .. 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 much more advanced :tacn:`setoid_rewrite` tactic
+      behaves differently, and thus the number of occurrences
+      available to rewrite may differ if using one or the other.
+
    .. exn:: Tactic failure: Setoid library not loaded.
       :undocumented: