Merge PR #12129: Add a `with_strategy` tactic

Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot

3 files changed, 156 insertions, 11 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8989dd29ab..bc2168411b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3355,6 +3355,128 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This is the most general syntax that combines the different variants.
 
+.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3
+   :name: with_strategy
+
+   Executes :token:`ltac_expr3`, applying the alternate unfolding
+   behavior that the :cmd:`Strategy` command controls, but only for
+   :token:`ltac_expr3`.  This can be useful for guarding calls to
+   reduction in tactic automation to ensure that certain constants are
+   never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to
+   ensure that unfolding does not fail.
+
+   .. note::
+
+      This tactic unfortunately does not yet play well with tactic
+      internalization, resulting in interpretation-time errors when
+      you try to use it directly with opaque identifiers, as seen in
+      the first (failing) use of :tacn:`with_strategy` in the
+      following example.  This can be worked around by binding the
+      identifier to an |Ltac| variable, and this issue should
+      disappear in a future version of |Coq|; see `#12179
+      <https://github.com/coq/coq/issues/12179>`_.
+
+   .. example::
+
+      .. coqtop:: all reset abort
+
+         Opaque id.
+         Goal id 10 = 10.
+         Fail unfold id.
+         Fail with_strategy transparent [id] unfold id.
+         let id' := id in with_strategy transparent [id] unfold id'.
+
+   .. warning::
+
+      Use this tactic with care, as effects do not persist past the
+      end of the proof script.  Notably, this fine-tuning of the
+      conversion strategy is not in effect during :cmd:`Qed` nor
+      :cmd:`Defined`, so this tactic is most useful either in
+      combination with :tacn:`abstract`, which will check the proof
+      early while the fine-tuning is still in effect, or to guard
+      calls to conversion in tactic automation to ensure that, e.g.,
+      :tacn:`unfold` does not fail just because the user made a
+      constant :cmd:`Opaque`.
+
+      This can be illustrated with the following example involving the
+      factorial function.
+
+      .. coqtop:: in reset
+
+         Fixpoint fact (n : nat) : nat :=
+           match n with
+           | 0 => 1
+           | S n' => n * fact n'
+           end.
+
+      Suppose now that, for whatever reason, we want in general to
+      unfold the :g:`id` function very late during conversion:
+
+      .. coqtop:: in
+
+         Strategy 1000 [id].
+
+      If we try to prove :g:`id (fact n) = fact n` by
+      :tacn:`reflexivity`, it will now take time proportional to
+      :math:`n!`, because |Coq| will keep unfolding :g:`fact` and
+      :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full
+      computation of :g:`fact n` (in unary, because we are using
+      :g:`nat`), which takes time :math:`n!`.  We can see this cross
+      the relevant threshold at around :math:`n = 9`:
+
+      .. coqtop:: all abort
+
+         Goal True.
+         Time assert (id (fact 8) = fact 8) by reflexivity.
+         Time assert (id (fact 9) = fact 9) by reflexivity.
+
+      Note that behavior will be the same if you mark :g:`id` as
+      :g:`Opaque` because while most reduction tactics refuse to
+      unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as
+      merely a hint to unfold this constant last.
+
+      We can get around this issue by using :tacn:`with_strategy`:
+
+      .. coqtop:: all
+
+         Goal True.
+         Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity.
+         Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity.
+
+      However, when we go to close the proof, we will run into
+      trouble, because the reduction strategy changes are local to the
+      tactic passed to :tacn:`with_strategy`.
+
+      .. coqtop:: all abort fail
+
+         exact I.
+         Timeout 1 Defined.
+
+      We can fix this issue by using :tacn:`abstract`:
+
+      .. coqtop:: all
+
+         Goal True.
+         Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity.
+         exact I.
+         Time Defined.
+
+      On small examples this sort of behavior doesn't matter, but
+      because |Coq| is a super-linear performance domain in so many
+      places, unless great care is taken, tactic automation using
+      :tacn:`with_strategy` may not be robustly performant when
+      scaling the size of the input.
+
+   .. warning::
+
+      In much the same way this tactic does not play well with
+      :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as
+      an intermediary, this tactic does not play well with ``coqchk``,
+      even when used with :tacn:`abstract`, due to the inability of
+      tactics to persist information about conversion hints in the
+      proof term. See `#12200
+      <https://github.com/coq/coq/issues/12200>`_ for more details.
+
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 1759264e87..7191444bac 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -817,13 +817,15 @@ described first.
 
 .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] }
 
-   .. insertprodn strategy_level strategy_level
+   .. insertprodn strategy_level strategy_level_or_var
 
    .. prodn::
       strategy_level ::= opaque
       | @int
       | expand
       | transparent
+      strategy_level_or_var ::= @strategy_level
+      | @ident
 
    This command accepts the :attr:`local` attribute, which limits its effect
    to the current section or module, in which case the section and module
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d72409e0d9..ea5ad79a80 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1714,6 +1714,11 @@ Tactic notations allow customizing the syntax of tactics.
         - a global reference of term
         - :tacn:`unfold`
 
+      * - ``smart_global``
+        - :token:`smart_qualid`
+        - a global reference of term
+        - :tacn:`with_strategy`
+
       * - ``constr``
         - :token:`term`
         - a term
@@ -1734,6 +1739,16 @@ Tactic notations allow customizing the syntax of tactics.
         - an integer
         - :tacn:`do`
 
+      * - ``strategy_level``
+        - :token:`strategy_level`
+        - a strategy level
+        -
+
+      * - ``strategy_level_or_var``
+        - :token:`strategy_level_or_var`
+        - a strategy level
+        - :tacn:`with_strategy`
+
       * - ``tactic``
         - :token:`ltac_expr`
         - a tactic
@@ -1766,18 +1781,24 @@ Tactic notations allow customizing the syntax of tactics.
 
    .. todo: notation doesn't support italics
 
-   .. note:: In order to be bound in tactic definitions, each syntactic
-             entry for argument type must include the case of a simple |Ltac|
-             identifier as part of what it parses. This is naturally the case for
-             ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``.
-             This is the reason for introducing a special entry ``int_or_var`` which
-             evaluates to integers only but which syntactically includes
+   .. note:: In order to be bound in tactic definitions, each
+             syntactic entry for argument type must include the case
+             of a simple |Ltac| identifier as part of what it
+             parses. This is naturally the case for ``ident``,
+             ``simple_intropattern``, ``reference``, ``constr``, ...
+             but not for ``integer`` nor for ``strategy_level``.  This
+             is the reason for introducing special entries
+             ``int_or_var`` and ``strategy_level_or_var`` which
+             evaluate to integers or strategy levels only,
+             respectively, but which syntactically includes
              identifiers in order to be usable in tactic definitions.
 
-   .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in
-             primitive tactics or in other notations at places where a list of the
-             underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer``
-             or ``int_or_var``.
+   .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*``
+             entries can be used in primitive tactics or in other
+             notations at places where a list of the underlying entry
+             can be used: entry is either ``constr``, ``hyp``,
+             ``integer``, ``smart_qualid``, ``strategy_level``,
+             ``strategy_level_or_var``, or ``int_or_var``.
 
 
 .. rubric:: Footnotes