Describe info_auto limitations

doc/sphinx/addendum/type-classes.rst

@@ -517,10 +517,10 @@ Command summary
 
    The tactic ``autoapply`` applies :token:`one_term` using the transparency information
    of the hint database :token:`ident`, and does *no* typeclass resolution. This can
-   be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint
-   database ``typeclass_instances``) to allow backtracking on the typeclass
+   be used in :cmd:`Hint Extern`s for typeclass instances (in the hint
+   database `typeclass_instances`) to allow backtracking on the typeclass
    subgoals created by the lemma application, rather than doing typeclass
-   resolution locally at the hint application time.
+   resolution locally at hint application time.
 
 .. _TypeclassesTransparent:
 
@@ -665,6 +665,10 @@ Settings
    of goals.  Setting this :term:`option` to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this
    option to 0 turns that flag off.
 
+   Note that the tactics shown when :n:`@natural > 0`(after removing tactics that were
+   backtracked) may not always work as a replacement for the proof search
+   tactic.  See :ref:`here <info_auto_not_exact>`.
+
 Typeclasses eauto
 ~~~~~~~~~~~~~~~~~
 

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -85,6 +85,48 @@ Tactics
       variant is very useful for getting a better understanding of automation, or
       to know what lemmas/assumptions were used.
 
+.. _info_auto_not_exact:
+
+      The tactics shown in the info or debug output currently don't
+      correspond exactly to the variants that proof search tactics such
+      as :tacn:`auto` use, but they are close.
+
+      Occasionally the tactics shown (after removing tactics that were
+      backtracked) may not always work as a replacement for the proof search
+      tactic.  For example:
+
+      .. example:: `info_auto` output that isn't a valid proof
+
+         The output isn't accepted as a proof because the conversion
+         constraints are solved by default after every statement but
+         are not solved internally by :tacn:`auto` as it searches for
+         a proof.
+
+         .. coqtop:: in
+
+            Create HintDb db.
+
+            Hint Resolve conj : db.
+            Hint Resolve eq_refl : db.
+
+            Goal forall n, n=1 -> exists x y : nat, x = y /\ x = 0.
+            intros.
+            do 2 eexists; subst.      (* Fix 2: replace with "eexists; subst." twice *)
+
+         .. coqtop:: all
+
+            Succeed info_auto with nocore db.
+            simple apply conj.           (* from info_auto output *)
+              Fail simple apply @eq_refl.  (* Fix 1: change to "2: simple apply @eq_refl" *)
+              (* simple apply @eq_refl. *)
+
+         .. coqtop:: none abort
+
+         One fix is to apply the tactics to the goals in a non-default
+         order.  Another would be to avoid using `do 2` by repeating the commands
+         that follow it, which gives a different result.  The fixes are shown inline
+         in the example.
+
    .. tacn:: debug auto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
       Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
@@ -130,6 +172,9 @@ Tactics
    .. tacn:: info_eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
 
       The various options for :tacn:`info_eauto` are the same as for :tacn:`info_auto`.
+      Note that the tactics shown (after removing tactics that were
+      backtracked) may not always work as a replacement for the proof search
+      tactic.  See :ref:`here <info_auto_not_exact>`.
 
    :tacn:`eauto` uses the following flags:
 

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -117,15 +117,21 @@ Rewriting with Leibniz and setoid equality
    .. prodn::
       oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings
 
-   Replaces subterms with other subterms that have been proven to be equal.
-   The type of :n:`@one_term` must have the form:
+   Replaces subterms with other subterms that have been proven to be equal or logically
+   equivalent.  For equal terms, the type of :n:`@one_term` must have the form:
 
       :n:`{? forall @open_binders , } EQ @term__1 @term__2`
 
    where :g:`EQ` is the :term:`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>`.
+   :n:`@term__1 = @term__2`.
+
+   For logically equivalent terms, the type of :n:`@one_term` must have the form:
+
+     :n:`{? forall @open_binders , } @term__1 <-> @term__2`
+
+   You must `Require Setoid` to use the tactic with a setoid equality, logical
+   equivalence or with :ref:`setoid rewriting <generalizedrewriting>`.
 
    :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).