Convert rewriting and proof-mode chapters to prodn

3 files changed, 410 insertions, 277 deletions

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index 472df2bd91..d7228a3907 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -335,7 +335,7 @@ Creating Hints
       .. 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.
+         such that this tactic cannot be associated with a constant.
 
    .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } }
 
diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index 40d032543f..931ac905f6 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -1,74 +1,175 @@
 .. _proofhandling:
 
--------------------
- Proof handling
--------------------
+----------
+Proof mode
+----------
 
-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`.
+:gdef:`Proof mode <proof mode>` is used to prove theorems.
+Coq enters proof mode when you begin a proof,
+such as with the :cmd:`Theorem` command.  It exits proof mode when
+you complete a proof, such as with the :cmd:`Qed` command.  Tactics,
+which are available only in proof mode, incrementally transform incomplete
+proofs to eventually generate a complete proof.
 
-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.
+When you run Coq interactively, such as through CoqIDE, Proof General or
+coqtop, Coq shows the current proof state (the incomplete proof) as you
+enter tactics.  This information isn't shown when you run Coq in batch
+mode with `coqc`.
 
-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.
+Proof State
+-----------
 
-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`).
+The :gdef:`proof state` consists of one or more unproven goals.
+Each goal has a :gdef:`conclusion` (the statement that is to be proven)
+and a :gdef:`local context`, which contains named :term:`hypotheses <hypothesis>`
+(which are propositions), variables and local definitions that can be used in
+proving the conclusion.  The proof may also use *constants* from the :term:`global environment`
+such as definitions and proven theorems.
 
-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*.
+The term ":gdef:`goal`" may refer to an entire goal or to the conclusion
+of a goal, depending on the context.
 
+The conclusion appears below a line and the local context appears above the line.
+The conclusion is a type.  Each item in the local context begins with a name
+and ends, after a colon, with an associated type.
+Local definitions are shown in the form `n := 0 : nat`, for example, in which `nat` is the
+type of `0`.
 
-.. exn:: No focused proof.
+The local context of a goal contains items specific to the goal as well
+as section-local variables and hypotheses (see :ref:`gallina-assumptions`) defined
+in the current :ref:`section <section-mechanism>`.  The latter are included in the
+initial proof state.
+Items in the local context are ordered; an item can only refer to items that appear
+before it.  (A more mathematical description of the *local context* is
+:ref:`here <Local-context>`.)
 
-   Coq raises this error message when one attempts to use a proof editing command
-   out of the proof editing mode.
+The :gdef:`global environment` has definitions and proven theorems that are global in scope.
+(A more mathematical description of the *global environment* is :ref:`here <Global-environment>`.)
+
+When you begin proving a theorem, the proof state shows
+the statement of the theorem below the line and often nothing in the
+local context:
+
+.. coqtop:: none
+
+   Parameter P: nat -> Prop.
+
+.. coqtop:: out
+
+   Goal forall n m: nat, n > m -> P 1 /\ P 2.
+
+After applying the :tacn:`intros` :term:`tactic`, we see hypotheses above the line.
+The names of variables (`n` and `m`) and hypotheses (`H`) appear before a colon, followed by
+the type they represent.
+
+.. coqtop:: all
+
+   intros.
+
+Some tactics, such as :tacn:`split`, create new goals, which may
+be referred to as :gdef:`subgoals <subgoal>` for clarity.
+Goals are numbered from 1 to N at each step of the proof to permit applying a
+tactic to specific goals.  The local context is only shown for the first goal.
+
+.. coqtop:: all
+
+   split.
+
+"Variables" may refer specifically to local context items for which the type of their type
+is `Set` or `Type`, and :gdef:`"hypotheses" <hypothesis>` refers to items that are
+:term:`propositions <proposition>`,
+for which the type of their type is `Prop` or `SProp`,
+but these terms are also used interchangeably.
+
+.. coqtop:: out
+
+   let t_n := type of n in idtac "type of n :" t_n;
+   let tt_n := type of t_n in idtac "type of" t_n ":" tt_n.
+   let t_H := type of H in idtac "type of H :" t_H;
+   let tt_H := type of t_H in idtac "type of" t_H ":" tt_H.
+
+A proof script, consisting of the tactics that are applied to prove a
+theorem, is often informally referred to as a "proof".
+The real proof, whether complete or incomplete, is a term, the :gdef:`proof term`,
+which users may occasionally want to examine.  (This is based on the
+*Curry-Howard isomorphism* :cite:`How80,Bar81,Gir89,H89`, which is
+a correspondence between between proofs and terms and between
+propositions and types of λ-calculus.  The isomorphism is also
+sometimes called the "propositions-as-types correspondence".)
+
+The :cmd:`Show Proof` command displays the incomplete proof term
+before you've completed the proof.  For example, here's the proof
+term after using the :tacn:`split` tactic above:
+
+.. coqtop:: all
+
+   Show Proof.
+
+The incomplete parts, the goals, are represented by
+:term:`existential variables <existential variable>`
+with names that begin with `?Goal`.  The :cmd:`Show Existentials` command
+shows each existential with the hypotheses and conclusion for the associated goal.
+
+.. coqtop:: all
+
+   Show Existentials.
+
+Coq's kernel verifies the correctness of proof terms when it exits
+proof mode by checking that the proof term is :term:`well-typed` and
+that its type is the same as the theorem statement.
+
+After a proof is completed, :cmd:`Print` `<theorem_name>`
+shows the proof term and its type.  The type appears after
+the colon (`forall ...`), as for this theorem from Coq's standard library:
+
+.. coqtop:: all
+
+   Print proj1.
 
 .. _proof-editing-mode:
 
-Entering and leaving proof editing mode
----------------------------------------
+Entering and exiting proof mode
+-------------------------------
+
+Coq enters :term:`proof mode` when you begin a proof through
+commands such as :cmd:`Theorem` or :cmd:`Goal`.  Coq user interfaces
+usually have a way to indicate that you're in proof mode.
+
+:term:`Tactics <tactic>` are available only in proof mode (currently they give syntax
+errors outside of proof mode).  Most :term:`commands <command>` can be used both in and out of
+proof mode, but some commands only work in or outside of proof 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.
+When the proof is completed, you can exit proof mode with commands such as
+:cmd:`Qed`, :cmd:`Defined` and :cmd:`Save`.
 
 .. 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).
+   Asserts an unnamed proposition.  This is intended for quick tests that
+   a proposition is provable.  If the proof is eventually completed and
+   validated, you can assign a name with the :cmd:`Save` or :cmd:`Defined`
+   commands.  If no name is given, the name will be `Unnamed_thm` (or,
+   if that name is already defined, a variant of that).
 
 .. 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.
+   Passes a completed :term:`proof term` to Coq's kernel
+   to check that the proof term is :term:`well-typed` and
+   to verify that its type matches the theorem statement.  If it's verified, the
+   proof term is added to the global environment as an opaque constant
+   using the declared name from the original goal.
+
+   It's very rare for a proof term to fail verification.  Generally this
+   indicates a bug in a tactic you used or that you misused some
+   unsafe tactics.
 
    .. exn:: Attempt to save an incomplete proof.
       :undocumented:
 
+   .. exn:: No focused proof (No proof-editing in progress).
+
+      You tried to use a proof mode command such as :cmd:`Qed` outside of proof
+      mode.
+
    .. note::
 
       Sometimes an error occurs when building the proof term, because
@@ -81,9 +182,9 @@ list of assertion commands is given in :ref:`Assertions`. The command
       even incur a memory overflow.
 
 .. cmd:: Save @ident
-   :name: Save
 
-   Saves a completed proof with the name :token:`ident`, which
+   Similar to :cmd:`Qed`, except that the proof term is added to the global
+   context with the name :token:`ident`, which
    overrides any name provided by the :cmd:`Theorem` command or
    its variants.
 
@@ -98,7 +199,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
 .. cmd:: Admitted
 
-   This command is available in interactive editing mode to give up
+   This command is available in proof mode to give up
    the current proof and declare the initial goal as an axiom.
 
 .. cmd:: Abort {? {| All | @ident } }
@@ -120,7 +221,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 .. cmd:: Proof @term
    :name: Proof `term`
 
-   This command applies in proof editing mode. It is equivalent to
+   This command applies in proof 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`).
@@ -159,7 +260,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
       | Type {? * }
       | All
 
-   Opens proof editing mode, declaring the set of
+   Opens proof 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
@@ -210,7 +311,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all reset
 
          Section Test.
          Variable n : nat.
@@ -232,7 +333,6 @@ 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
@@ -301,7 +401,7 @@ Name a set of section hypotheses for ``Proof using``
       Use :cmd:`Unshelve` instead.
 
 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
@@ -312,8 +412,8 @@ 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
+   mode, various syntactic constructs are allowed when writing a
+   proof. All proof modes support commands; the proof mode determines
    which tactic language and set of tactic definitions are available.  The
    possible option values are:
 
@@ -349,16 +449,16 @@ Navigation in the proof tree
 
 .. cmd:: Restart
 
-   Restores the proof editing process to the original goal.
+   Restores the proof 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
+   Focuses the attention on the first goal to prove or, if :token:`natural` is
    specified, the :token:`natural`\-th.  The
-   printing of the other subgoals is suspended until the focused subgoal
+   printing of the other goals is suspended until the focused goal
    is solved or unfocused.
 
    .. deprecated:: 8.8
@@ -379,14 +479,9 @@ Navigation in the proof tree
 
 .. _curly-braces:
 
-.. index:: {
-           }
-
-.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket,
-   hence the verbose names
-
 .. tacn:: {? {| @natural | [ @ident ] } : } %{
-         %}
+          %}
+   :name: {; }
 
    .. todo
       See https://github.com/coq/coq/issues/12004 and
@@ -403,7 +498,7 @@ Navigation in the proof tree
    or focus the next one.
 
    :n:`@natural:`
-     Focuses on the :token:`natural`\-th subgoal to prove.
+     Focuses on the :token:`natural`\-th goal to prove.
 
    :n:`[ @ident ]: %{`
      Focuses on the named goal :token:`ident`.
@@ -477,7 +572,7 @@ Navigation in the proof tree
       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.
+   .. seealso:: The error messages for bullets below.
 
 .. _bullets:
 
@@ -567,7 +662,6 @@ Set Bullet Behavior
 ~~~~~~~~~~~~~~~~~~~
 
 .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
-   :name: Bullet Behavior
 
    This option controls the bullet behavior and can take two possible values:
 
@@ -577,8 +671,7 @@ Set Bullet Behavior
 Modifying the order of goals
 ````````````````````````````
 
-.. tacn:: cycle @integer
-   :name: cycle
+.. tacn:: cycle @int_or_var
 
    Reorders the selected goals so that the first :n:`@integer` goals appear after the
    other selected goals.
@@ -601,8 +694,7 @@ Modifying the order of goals
       all: cycle 2.
       all: cycle -3.
 
-.. tacn:: swap @integer @integer
-   :name: swap
+.. tacn:: swap @int_or_var @int_or_var
 
    Exchanges the position of the specified goals.
    Negative values for :n:`@integer` indicate counting goals
@@ -621,7 +713,6 @@ Modifying the order of goals
       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;
@@ -638,16 +729,17 @@ Modifying the order of goals
 Postponing the proof of some goals
 ``````````````````````````````````
 
+Goals can be :gdef:`shelved` so they are no longer displayed in the proof state.
+They can then be :gdef:`unshelved` to make them visible again.
+
 .. 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
+   .. tacn:: 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.
@@ -667,14 +759,12 @@ Postponing the proof of some goals
    from the shelf into focus, by appending them to the end of the current
    list of focused goals.
 
-.. tacn:: unshelve @tactic
-   :name: unshelve
+.. tacn:: unshelve @ltac_expr1
 
    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
@@ -694,7 +784,7 @@ Requesting information
    Displays the current goals.
 
    :n:`@natural`
-     Display only the :token:`natural`\-th subgoal.
+     Display only the :token:`natural`\-th goal.
 
    :n:`@ident`
      Displays the named goal :token:`ident`. This is useful in
@@ -791,7 +881,7 @@ Requesting information
 
    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
+   of 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.
 
@@ -854,7 +944,6 @@ 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
@@ -983,12 +1072,11 @@ To show differences in the proof term:
     .. image:: ../../_static/diffs-show-proof.png
        :alt: coqide with Set Diffs on with compacted hypotheses
 
-Controlling the effect of proof editing commands
-------------------------------------------------
+Controlling proof mode
+----------------------
 
 
 .. 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
@@ -1009,7 +1097,7 @@ Controlling the effect of proof editing commands
 
 .. flag:: Printing Goal Names
 
-   When turned on, the name of the goal is printed in interactive
+   When turned on, the name of the goal is printed in
    proof mode, which can be useful in cases of cross references
    between goals.
 
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 3649202b45..c54701b153 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -1,102 +1,123 @@
-=================================
-Term rewriting and simplification
-=================================
+=========================
+Reasoning with equalities
+=========================
 
-.. _rewritingexpressions:
+There are multiple notions of :gdef:`equality` in Coq:
 
-Rewriting expressions
----------------------
+- :gdef:`Leibniz equality` is the standard
+  way to define equality in Coq and the Calculus of Inductive Constructions,
+  which is in terms of a binary relation, i.e. a binary function that returns
+  a `Prop`.  The standard library
+  defines `eq` similar to this:
 
-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`.
+   .. coqdoc::
 
-.. tacn:: rewrite @term
-   :name: rewrite
+      Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x.
 
-   This tactic applies to any goal. The type of :token:`term` must have the form
+  The notation `x = y` represents the term `eq x y`.  The notation `x = y :> A`
+  gives the type of x and y explicitly.
 
-   ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.``
+- :gdef:`Setoid equality <setoid equality>` defines equality in terms of an equivalence
+  relation.  A :gdef:`setoid` is a set that is equipped with an equivalence relation
+  (see https://en.wikipedia.org/wiki/Setoid).  These are needed to form a :gdef:`quotient set`
+  or :gdef:`quotient`
+  (see https://en.wikipedia.org/wiki/Equivalence_Class).  In Coq, users generally work
+  with setoids rather than constructing quotients, for which there is no specific support.
 
-   where :g:`eq` is the Leibniz equality or a registered setoid equality.
+- :gdef:`Definitional equality <definitional equality>` is equality based on the
+  :ref:`conversion rules <Conversion-rules>`, which Coq can determine automatically.
+  When two terms are definitionally equal, Coq knows it can
+  replace one with the other, such as with :tacn:`change` `X with Y`, among many
+  other advantages.  ":term:`Convertible <convertible>`" is another way of saying that
+  two terms are definitionally equal.
 
-   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.
+.. _rewritingexpressions:
 
-   .. exn:: The @term provided does not end with an equation.
-      :undocumented:
+Rewriting with Leibniz and setoid equality
+------------------------------------------
 
-   .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
-      :undocumented:
+.. tacn:: rewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 }
 
-   .. tacv:: rewrite -> @term
+   .. insertprodn oriented_rewriter one_term_with_bindings
 
-      Is equivalent to :n:`rewrite @term`
+   .. prodn::
+      oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings
+      one_term_with_bindings ::= {? > } @one_term {? with @bindings }
 
-   .. tacv:: rewrite <- @term
+   Rewrites terms based on equalities.  The type of :n:`@one_term` must have the form:
 
-      Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left
+      :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2`
 
-   .. tacv:: rewrite @term in @goal_occurrences
+   where :g:`EQ` is the Leibniz equality `eq` or a registered 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>`.
+   In the general form, any :n:`@binder` may be used, not just :n:`(x__i: A__i)`.
 
-      Analogous to :n:`rewrite @term` but rewriting is done following
-      the clause :token:`goal_occurrences`. For instance:
+   .. todo doublecheck the @binder comment is correct.
 
-      + :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.
+   :n:`rewrite @one_term` finds subterms matching :n:`@term__1` in the goal,
+   and replaces them with :n:`@term__2` (or the reverse if `<-` is given).
+   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`
+   if you want to find such occurrences.
 
-      Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite.
+   :n:`{+, @oriented_rewriter }`
+     The :n:`@oriented_rewriter`\s are applied sequentially
+     to the first goal generated by the previous :n:`@oriented_rewriter`.  If any of them fail,
+     the tactic fails.
 
-   .. tacv:: rewrite @term at @occurrences
+   :n:`{? {| -> | <- } }`
+     For `->` (the default), :n:`@term__1` is rewritten
+     into :n:`@term__2`.  For `<-`, :n:`@term__2` is rewritten into :n:`@term__1`.
 
-      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.
+   :n:`{? @natural } {? {| ? | ! } }`
+     :n:`@natural` is the number of rewrites to perform.  If `?` is given, :n:`@natural`
+     is the maximum number of rewrites to perform; otherwise :n:`@natural` is the exact number
+     of rewrites to perform.
 
-   .. tacv:: rewrite @term by @tactic
+     `?` (without :n:`@natural`) performs the rewrite as many times as possible
+     (possibly zero times).
+     This form never fails.  `!` (without :n:`@natural`) performs the rewrite as many
+     times as possible
+     and at least once.  The tactic fails if the requested number of rewrites can't
+     be performed.  :n:`@natural !` is equivalent to :n:`@natural`.
 
-      Use tactic to completely solve the side-conditions arising from the
-      :tacn:`rewrite`.
+   :n:`@occurrences`
+     If :n:`@occurrences` specifies multiple occurrences, the tactic succeeds if
+     any of them can be rewritten.  If not specified, only the first occurrence
+     in the conclusion is replaced.
 
-   .. tacv:: rewrite {+, @orientation @term} {? in @ident }
+     If :n:`at @occs_nums` is specified, rewriting is always done with
+     :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality.
 
-      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.
+   :n:`by @ltac_expr3`
+     If specified, is used to resolve all side conditions generated by the tactic.
 
-   In all forms of rewrite described above, a :token:`term` to rewrite can be
-   immediately prefixed by one of the following modifiers:
+   .. exn:: Tactic failure: Setoid library not loaded.
+      :undocumented:
 
-   + `?` : 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.
+      .. todo You can use Typeclasses Debug to tell whether rewrite used
+         setoid rewriting.  Example here: https://github.com/coq/coq/pull/13470#discussion_r539230973
 
-   .. tacv:: erewrite @term
-      :name: erewrite
+   .. exn:: Cannot find a relation to rewrite.
+      :undocumented:
+
+   .. exn:: Tactic generated a subgoal identical to the original goal.
+      :undocumented:
+
+   .. exn:: Found no subterm matching @term in @ident.
+            Found no subterm matching @term in the current goal.
 
-      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 happens if :n:`@term` does not occur in, respectively, the named hypothesis or the goal.
+
+   .. tacn:: erewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 }
+
+      Works like :tacn:`rewrite`, but turns
+      unresolved bindings, if any, into existential variables instead of
+      failing. It has the same parameters as :tacn:`rewrite`.
 
    .. flag:: Keyed Unification
 
@@ -105,197 +126,221 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       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’`.
+.. tacn:: rewrite * {? {| -> | <- } } @one_term {? in @ident } {? at @rewrite_occs } {? by @ltac_expr3 }
+          rewrite * {? {| -> | <- } } @one_term at @rewrite_occs in @ident {? by @ltac_expr3 }
+   :name: rewrite *; _
+   :undocumented:
 
-   .. tacv:: replace @term
+.. tacn:: rewrite_db @ident {? in @ident }
+   :undocumented:
 
-      Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
-      the form :n:`@term = @term’` or :n:`@term’ = @term`.
+.. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 }
+          replace {? {| -> | <- } } @one_term__from {? @occurrences }
+   :name: replace; _
 
-   .. tacv:: replace -> @term
+   The first form replaces all free occurrences of :n:`@one_term__from`
+   in the current goal with :n:`@one_term__to` and generates an equality
+   :n:`@one_term__to = @one_term__from`
+   as a subgoal. (Note the generated equality is reversed with respect
+   to the order of the two terms in the tactic syntax; see
+   issue `#13480 <https://github.com/coq/coq/issues/13480>`_.)
+   This equality is automatically solved if it occurs among
+   the hypotheses, or if its symmetric form occurs.
 
-      Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
-      the form :n:`@term = @term’`
+   The second form, with `->` or no arrow, replaces :n:`@one_term__from`
+   with :n:`@term__to` using
+   the first hypothesis whose type has the form :n:`@one_term__from = @term__to`.
+   If `<-` is given, the tactic uses the first hypothesis with the reverse form,
+   i.e. :n:`@term__to = @one_term__from`.
 
-   .. tacv:: replace <- @term
+   :n:`@occurrences`
+     The `type of` and `value of` forms are not supported.
+     Note you must `Require Setoid` to use the `at` clause in :n:`@occurrences`.
 
-      Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has
-      the form :n:`@term’ = @term`
+   :n:`by @ltac_expr3`
+     Applies the :n:`@ltac_expr3` to solve the generated equality.
 
-   .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic}
-             replace -> @term in @goal_occurrences
-             replace <- @term in @goal_occurrences
+   .. exn:: Terms do not have convertible types.
+      :undocumented:
 
-      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:: cutrewrite {? {| -> | <- } } @one_term {? in @ident }
 
-   .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident }
-      :name: cutrewrite
+      Where :n:`@one_term` is an equality.
 
       .. deprecated:: 8.5
 
          Use :tacn:`replace` instead.
 
-.. tacn:: subst @ident
-   :name: subst
+.. tacn:: substitute {? {| -> | <- } } @one_term {? with @bindings }
+   :undocumented:
+
+.. tacn:: subst {* @ident }
 
-   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.
+   For each :n:`@ident`, in order, for which there is a hypothesis in the form
+   :n:`@ident = @term` or :n:`@term = @ident`, replaces :n:`@ident` with :n:`@term`
+   everywhere in the hypotheses and the conclusion and clears :n:`@ident` and the hypothesis
+   from the context.  If there are multiple hypotheses that match the :n:`@ident`,
+   the first one is used.  If no :n:`@ident` is given, replacement is done for all
+   hypotheses in the appropriate form in top to bottom order.
 
-   If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also
+   If :n:`@ident` is a local definition of the form :n:`@ident := @term`, 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
+   If :n:`@ident` is a section variable it must have no
+   indirect occurrences in the goal, i.e. no global declarations
+   implicitly depending on the section variable may 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.
+      If the hypothesis is itself dependent in the goal, it is replaced by the proof of
+      reflexivity of equality.
 
    .. 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
+      + A context with ordered hypotheses :n:`@ident__1 = @ident__2`
+        and :n:`@ident__1 = t`, or :n:`t′ = @ident__1` with `t′` not
+        a variable, and no other hypotheses of the form :n:`@ident__2 = u`
+        or :n:`u = @ident__2`; without the flag, a second call to
+        subst would be necessary to replace :n:`@ident__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
+      + A context with cyclic dependencies as with hypotheses :n:`@ident__1 = f @ident__2`
+        and :n:`@ident__2 = g @ident__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
+      Additionally, it prevents a local definition such as :n:`@ident := t` from being
       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`.
+   .. exn:: Cannot find any non-recursive equality over @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.
+   .. exn:: Section variable @ident occurs implicitly in global declaration @qualid present in hypothesis @ident.
+            Section variable @ident occurs implicitly in global declaration @qualid present in the conclusion.
 
       Raised when the variable is a section variable with indirect
       dependencies in the goal.
+      If :n:`@ident` is a section variable, it must not have any
+      indirect occurrences in the goal, i.e. no global declarations
+      implicitly depending on the section variable may be present in the
+      goal.
 
+.. tacn:: simple subst
+   :undocumented:
 
-.. tacn:: stepl @term
-   :name: stepl
+.. tacn:: stepl @one_term {? by @ltac_expr }
 
-   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
+   For chaining rewriting steps. It assumes a goal in the
+   form :n:`R @term__1 @term__2` 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`.
+   where `eq` is typically a setoid equality. The application of :n:`stepl @one_term`
+   then replaces the goal by :n:`R @one_term @term__2` and adds a new goal stating
+   :n:`eq @one_term @term__1`.
 
-   .. cmd:: Declare Left Step @term
+   If :n:`@ltac_expr` is specified, it is applied to the side condition.
 
-      Adds :n:`@term` to the database used by :tacn:`stepl`.
+   .. cmd:: Declare Left Step @one_term
+
+      Adds :n:`@one_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
+   .. tacn:: stepr @one_term {? by @ltac_expr }
 
-      This behaves as :tacn:`stepl` but on the right-hand-side of the binary
-      relation. Lemmas are expected to be of the form
+      This behaves like :tacn:`stepl` but on the right hand side of the binary
+      relation. Lemmas are expected to be in 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 @one_term
 
        Adds :n:`@term` to the database used by :tacn:`stepr`.
 
+Rewriting with definitional equality
+------------------------------------
 
-.. tacn:: change @term
-   :name: change
+.. tacn:: change {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences }
 
-   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.
+   Replaces terms with other :term:`convertible` terms.
+   If :n:`@one_term__from` is not specified, then :n:`@one_term__from` replaces the conclusion and/or
+   the specified hypotheses.  If :n:`@one_term__from` is specified, the tactic replaces occurrences
+   of :n:`@one_term__to` within the conclusion and/or the specified hypotheses.
+
+   :n:`{? @one_term__from {? at @occs_nums } with }`
+     Replaces the occurrences of :n:`@one_term__from` specified by :n:`@occs_nums`
+     with :n:`@one_term__to`, provided that the two :n:`@one_term`\s are
+     convertible.  :n:`@one_term__from` may contain pattern variables such as `?x`,
+     whose value which will substituted for `x` in :n:`@one_term__to`, such as in
+     `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`.
+
+   :n:`@occurrences`
+     If `with` is not specified, :n:`@occurrences` must only specify
+     entire hypotheses and/or the goal; it must not include any
+     :n:`at @occs_nums` clauses.
 
    .. exn:: Not convertible.
       :undocumented:
 
-   .. tacv:: change @term with @term’
+   .. exn:: Found an "at" clause without "with" clause
+      :undocumented:
 
-      This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal.
-      The term :n:`@term` and :n:`@term’` must be convertible.
+   .. tacn:: now_show @one_term
 
-   .. tacv:: change @term at {+ @natural} with @term’
+      A synonym for :n:`change @one_term`. It can be used to
+      make some proof steps explicit when refactoring a proof script
+      to make it readable.
 
-      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.
+   .. seealso:: :ref:`Performing computations <performingcomputations>`
 
-      .. exn:: Too few occurrences.
-         :undocumented:
+.. tacn:: change_no_check {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences }
 
-   .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences
+   For advanced usage. Similar to :tacn:`change`, but as an optimization,
+   it skips checking that :n:`@one_term__to` is convertible with the goal or
+   :n:`@one_term__from`.
 
-      In the presence of :n:`with`, this applies :tacn:`change` to the
-      occurrences specified by :n:`@goal_occurrences`. In the
-      absence of :n:`with`, :n:`@goal_occurrences` is expected to
-      only list hypotheses (and optionally the conclusion) without
-      specifying occurrences (i.e. no :n:`at` clause).
+   Recall that the Coq kernel typechecks proofs again when they are concluded to
+   ensure correctness. Hence, using :tacn:`change` checks convertibility twice
+   overall, while :tacn:`change_no_check` can produce ill-typed terms,
+   but checks convertibility only once.
+   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
+   scripts, especially if one knows by construction that the argument is
+   indeed convertible to the goal.
 
-   .. tacv:: now_show @term
+   In the following example, :tacn:`change_no_check` replaces :g:`False` with
+   :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency.
 
-      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.
+   .. example::
 
-   .. seealso:: :ref:`Performing computations <performingcomputations>`
+      .. coqtop:: all abort fail
+
+         Goal False.
+           change_no_check True.
+           exact I.
+         Qed.
+
+   .. example::
+
+      .. coqtop:: all abort fail
+
+         Goal True -> False.
+           intro H.
+           change_no_check False in H.
+           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: