Merge PR #7508: Improve rewrite section in tactic chapter.

1 files changed, 127 insertions, 139 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 3835524f0..da4c3f9d7 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2398,35 +2398,35 @@ 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 :n:`@term` must have the form
+   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` ``.``
+   ``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.
+   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.
+   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.
+   .. exn:: The @term provided does not end with an equation.
 
-.. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
+   .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
 
-.. tacv:: rewrite -> @term
+   .. tacv:: rewrite -> @term
 
-  Is equivalent to :n:`rewrite @term`
+      Is equivalent to :n:`rewrite @term`
 
-.. tacv:: rewrite <- @term
+   .. tacv:: rewrite <- @term
 
-  Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left
+      Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left
 
-.. tacv:: rewrite @term in clause
+   .. tacv:: rewrite @term in clause
 
-  Analogous to :n:`rewrite @term` but rewriting is done following clause
-  (similarly to :ref:`performing computations <performingcomputations>`). For instance:
+      Analogous to :n:`rewrite @term` but rewriting is done following clause
+      (similarly to :ref:`performing computations <performingcomputations>`). For instance:
 
       + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis
         `H`:sub:`1` instead of the current goal.
@@ -2440,136 +2440,128 @@ subgoals.
       + :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 :n:`@term` to rewrite.
+      Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite.
 
-.. tacv:: rewrite @term at occurrences
+   .. tacv:: rewrite @term at occurrences
 
-  Rewrite only the given occurrences of :n:`@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.
+      Rewrite only the given 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
+   .. tacv:: rewrite @term by tactic
 
-  Use tactic to completely solve the side-conditions arising from the
-  :tacn:`rewrite`.
+      Use tactic to completely solve the side-conditions arising from the
+      :tacn:`rewrite`.
 
-.. tacv:: rewrite {+ @term}
+   .. tacv:: rewrite {+, @term}
 
-  Is equivalent to the `n` successive tactics :n:`{+ rewrite @term}`, each one
-  working on the first subgoal generated by the previous one. Orientation
-  :g:`->` or :g:`<-` can be inserted before each :n:`@term` to rewrite.  One
-  unique clause can be added at the end after the keyword in; it will then
-  affect all rewrite operations.
+      Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one
+      working on the first subgoal generated by the previous one. Orientation
+      :g:`->` or :g:`<-` 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 :n:`@term` to rewrite can be
-  immediately prefixed by one of the following modifiers:
+   In all forms of rewrite described above, a :token:`term` to rewrite can be
+   immediately prefixed by one of the following modifiers:
 
-  + `?` : the tactic rewrite :n:`?@term` performs the rewrite of :n:`@term` as many
-    times as possible (perhaps zero time). This form never fails.
-  + `n?` : works similarly, except that it will do at most `n` rewrites.
-  + `!` : works as ?, except that at least one rewrite should succeed, otherwise
-    the tactic fails.
-  + `n!` (or simply `n`) : precisely `n` rewrites of :n:`@term` will be done,
-    leading to failure if these n rewrites are not possible.
+   + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many
+     times as possible (perhaps zero time). This form never fails.
+   + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites.
+   + `!` : works as `?`, except that at least one rewrite should succeed, otherwise
+     the tactic fails.
+   + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done,
+     leading to failure if these :token:`num` rewrites are not possible.
 
-.. tacv:: erewrite @term
-   :name: erewrite
+   .. 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.
+      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.
 
-.. tacn:: replace @term with @term
+.. 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 the equality :n:`@term =
-   @term` as a subgoal. This equality is automatically solved if it occurs among
-   the assumption, 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]`.
+   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.
+   .. exn:: Terms do not have convertible types.
 
-.. tacv:: replace @term with @term by tactic
+   .. tacv:: replace @term with @term’ by @tactic
 
-  This acts as :n:`replace @term` with :n:`@term` but applies tactic to solve the generated
-  subgoal :n:`@term = @term`.
+      This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated
+      subgoal :n:`@term = @term’`.
 
-.. tacv:: replace @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`.
+      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
+   .. tacv:: replace -> @term
 
-  Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
-  the form :n:`@term = @term’`
+      Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
+      the form :n:`@term = @term’`
 
-.. tacv:: replace <- @term
+   .. tacv:: replace <- @term
 
-  Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
-  the form :n:`@term’ = @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 clause
-.. tacv:: replace @term with @term in clause by tactic
-.. tacv:: replace @term in clause replace -> @term in clause
-.. tacv:: replace <- @term in clause
+   .. tacv:: replace @term {? with @term} in clause {? by @tactic}
+   .. tacv:: replace -> @term in clause
+   .. tacv:: replace <- @term in clause
 
-  Acts as before but the replacements take place inclause (see
-  :ref:`performingcomputations`) and not only in the conclusion of the goal. The
-  clause argument must not contain any type of nor value of.
+      Acts as before but the replacements take place in the specified clause (see
+      :ref:`performingcomputations`) and not only in the conclusion of the goal. The
+      clause argument must not contain any ``type of`` nor ``value of``.
 
-.. tacv:: cutrewrite <- (@term = @term)
-   :cutrewrite:
+   .. tacv:: cutrewrite <- (@term = @term’)
+      :name: cutrewrite
 
-  This tactic is deprecated. It acts like :n:`replace @term with @term`, or,
-  equivalently as :n:`enough (@term = @term) as <-`.
+      This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`.
 
-.. tacv:: cutrewrite -> (@term = @term)
+   .. tacv:: cutrewrite -> (@term = @term’)
 
-  This tactic is deprecated. It can be replaced by enough :n:`(@term = @term) as ->`.
+      This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`.
 
 
 .. 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.
 
-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.
-
-
-.. note::
-  When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the
-  first one is used.
-
-
-.. note::
-  If `H` is itself dependent in the goal, it is replaced by the proof of
-  reflexivity of equality.
+   If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also
+   unfolded and cleared.
 
+   .. note::
+      + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the
+        first one is used.
 
-.. tacv:: subst {+ @ident}
+      + If :g:`H` is itself dependent in the goal, it is replaced by the proof of
+        reflexivity of equality.
 
-  This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`.
+   .. tacv:: subst {+ @ident}
 
-.. tacv:: subst
+      This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`.
 
-   This applies subst repeatedly from top to bottom to all identifiers 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`.
+   .. tacv:: subst
 
+      This applies subst repeatedly from top to bottom to all identifiers 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``.
 
    .. opt:: Regular Subst Tactic
 
       This option controls the behavior of :tacn:`subst`. When it is
-      activated, :tacn:`subst` also deals with the following corner cases:
+      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
@@ -2587,41 +2579,40 @@ unfolded and cleared.
       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 option it may break. The option is on by
+      hypotheses, which without the option it may break.
       default.
 
 
 .. 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`.
 
-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
 
-.. cmd:: Declare Left Step @term
+      Adds :n:`@term` to the database used by :tacn:`stepl`.
 
-   Adds :n:`@term` to the database used by :tacn:`stepl`.
+   The tactic is especially useful for parametric setoids which are not accepted
+   as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
+   :ref:`Generalizedrewriting`).
 
-The 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
 
-.. tacv:: stepl @term by tactic
+      This applies :n:`stepl @term` then applies :token:`tactic` to the second goal.
 
-   This applies :n:`stepl @term` then applies tactic to the second goal.
+   .. tacv:: stepr @term stepr @term by tactic
+      :name: stepr
 
-.. tacv:: stepr @term 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`.
 
-   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
+   .. cmd:: Declare Right Step @term
 
        Adds :n:`@term` to the database used by :tacn:`stepr`.
 
@@ -2634,28 +2625,25 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    with `U` providing that `U` is well-formed and that `T` and `U` are
    convertible.
 
-.. exn:: Not convertible.
-
+   .. exn:: Not convertible.
 
-.. tacv:: change @term with @term
+   .. 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.
+      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 {+ @num} with @term
+   .. tacv:: change @term at {+ @num} with @term’
 
-  This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term`
-  in the current goal. The terms :n:`@term` and :n:`@term` must be convertible.
+      This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’`
+      in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible.
 
-.. exn:: Too few occurrences.
+      .. exn:: Too few occurrences.
 
-.. tacv:: change @term in @ident
-.. tacv:: change @term with @term in @ident
-.. tacv:: change @term at {+ @num} with @term in @ident
+   .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident
 
-  This applies the change tactic not to the goal but to the hypothesis :n:`@ident`.
+      This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`.
 
-See also: :ref:`Performing computations <performingcomputations>`
+   .. seealso:: :ref:`Performing computations <performingcomputations>`
 
 .. _performingcomputations:
 
@@ -3434,7 +3422,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       Adds each :n:`Hint Unfold @ident`.
 
    .. cmdv:: Hint %( Transparent %| Opaque %) @qualid
-      :name: Hint %( Transparent %| Opaque %)
+      :name: Hint ( Transparent | Opaque )
 
       This adds a transparency hint to the database, making :n:`@qualid` a
       transparent or opaque constant during resolution. This information is used