Refine Hint Opaque/Transparent doc

doc/changelog/08-vernac-commands-and-options/19761-hintdb_doc.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Additional documentation of Create HintDb (discriminated), proof search
+  tactic performance, matching process and hint transparency
+  (`#19761 <https://github.com/coq/coq/pull/19761>`_,
+  by Jim Fehrle).

doc/sphinx/language/core/conversion.rst

@@ -141,9 +141,8 @@ or :term:`constants <constant>` defined in the :term:`global environment` with t
    --------------
    E[Γ] ⊢ c~\triangleright_δ~t
 
-:term:`Delta-reduction <delta-reduction>` only unfolds :term:`constants <constant>` that are
-marked :gdef:`transparent`.  :gdef:`Opaque <opaque>` is the opposite of
-transparent; :term:`delta-reduction` doesn't unfold opaque constants.
+:term:`Delta-reduction <delta-reduction>` unfolds constants when permitted by their
+:term:`opaqueness <opaque>` settings.
 
 ι-reduction
 ~~~~~~~~~~~

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

@@ -318,27 +318,71 @@ Creating hint databases
 ```````````````````````
 
 Hint databases can be created with the :cmd:`Create HintDb` command or implicitly
-by adding a hint to an unknown database.  We recommend you always use :cmd:`Create HintDb`
-and then imediately use :cmd:`Hint Constants` and :cmd:`Hint Variables` to make
-those settings explicit.
-
-Note that the default transparency
-settings differ between these two methods of creation.  Databases created with
-:cmd:`Create HintDb` have the default setting `Transparent` for both `Variables`
-and `Constants`, while implicitly created databases have the `Opaque` setting.
+by adding a hint to an unknown database.  Databases created with
+:cmd:`Create HintDb` have the default setting `Transparent`
+for `Constants`, `Projections` and `Variables`, while implicitly created databases
+have the `Opaque` setting.  We recommend using :cmd:`Hint Constants`,
+:cmd:`Hint Projections` and :cmd:`Hint Variables` immediately after :cmd:`Create HintDb`
+to make these settings explicit.
+
+Use :cmd:`Hint Opaque` and :cmd:`Hint Transparent` to control the opacity of
+individual items.  Hint opacity settings influence which hints the search tactics
+try, but they may or may not affect how the selected tactic is executed.
+(Usually not, except for :tacn:`typeclasses eauto`, which uses the equivalent of
+:tacn:`autoapply`, which explicitly uses the hint opacity settings when
+applying a :cmd:`Hint Resolve` hint.)
+The proof search tactics use unification to choose which tactics to try, for example
+whether the goal unifies with a theorem given by :cmd:`Hint Resolve`.
+These settings are distinct from the non-hint :cmd:`Opaque` and :cmd:`Transparent`
+settings.
 
 .. cmd:: Create HintDb @ident {? discriminated }
 
-   Creates a new hint database named :n:`@ident`. The database is
-   implemented by a Discrimination Tree (DT) that serves as a filter to select
-   the lemmas that will be applied. When discriminated, the DT uses
-   transparency information to decide if a constant should considered rigid for
-   filtering, making the retrieval more efficient. By contrast, undiscriminated
-   databases treat all constants as transparent, resulting in a larger
-   number of selected lemmas to be applied, and thus putting more pressure on
-   unification.
+   Creates a new hint database named :n:`@ident`.  If the hint database already
+   exists, its current data is dropped
+   (see `#16934 <https://github.com/coq/coq/issues/16934>`_).
+   All constants, variables and projections are set to default to unfoldable (use
+   :cmd:`Hint Constants`, :cmd:`Hint Projections` and :cmd:`Hint Variables`
+   to change this).
+
+   By default, hint databases are undiscriminated.  We recommend using `discriminated`
+   because it generally performs better.
+
+.. _hint_performance_considerations:
+
+Performance considerations
+``````````````````````````
+
+The proof search tactics decide which hints to try by first selecting hints
+whose pattern has the same :term:`head constant` as the goal.  Then the selected
+hints are tried as follows:
+
+- For hints other than :cmd:`Hint Extern`: If the database is discriminated, only
+  matching hints are tried.  Hints match if all compared items that are opaque in
+  both the goal and the pattern are identical.  In this case you can reduce the
+  number of matches by marking definitions as hint opaque through trial and error
+  (if the proof search fails after making something opaque, then it's incorrect).
+
+  Otherwise (if not discriminated), all hints will be tried.  (Therefore, use
+  `discriminated` databases whenever possible.)
+- For `Extern` hints: If the hint has a pattern, hints matching the goal will be tried.
+  In this case, matching uses `syntactic unification
+  <https://en.wikipedia.org/wiki/Unification_(computer_science)#Examples_of_syntactic_unification_of_first-order_terms>`_),
+  treating everything as hint opaque.
+
+  Otherwise (if there is no pattern), all hints will be tried. (Therefore, provide a
+  pattern in `Extern` hints whenever possible.)
 
-   By default, hint databases are undiscriminated.
+.. todo Mention that apply will use conversion (after bug is fixed)
+
+  .. comment:
+     discriminated matches patterns: see test-suite/output/disc_uses_patterns.v
+     discriminated with transparent: see test-suite/output/disc_with_transparent.v
+     non-discriminated ignores patterns: see test-suite/output/nondisc_ignores_pattern.v
+     Extern uses syntactic unification: see test-suite/success/hint_extern_syntactic_unify.v
+     Extern with no pattern:  see test-suite/output/extern_no_pattern.v
+
+.. comment not sure: Note: currently, proof search tactics won't unfold the head constant even if it is transparent.
 
 Hint databases defined in the Rocq standard library
 ```````````````````````````````````````````````````
@@ -380,7 +424,7 @@ At Rocq startup, only the core database is nonempty and ready to be used immedia
                mainly used in the ``FSets`` and ``FMaps`` libraries.
 
 You are advised not to put your own hints in the core database, but
-use one or more databases specific to your development.
+instead to use one or more databases specific to your development.
 
 .. _creating_hints:
 
@@ -432,16 +476,21 @@ Creating Hints
          hint_info ::= %| {? @natural } {? @one_pattern }
          one_pattern ::= @one_term
 
-      The first form adds each :n:`@qualid` as a hint with the head symbol of the type of
-      :n:`@qualid` to the specified hint databases (:n:`@ident`\s). The cost of the hint is the number of
-      subgoals generated by :tacn:`simple apply` :n:`@qualid` or, if specified, :n:`@natural`. The
+      The first form adds each :n:`@qualid` as a hint with the head symbol of the
+      type of :n:`@qualid` to the specified hint databases (:n:`@ident`\s). The
+      cost of the hint is :n:`@natural` (which can be inside :n:`@hint_info`). The
       associated pattern is inferred from the conclusion of the type of
       :n:`@qualid` or, if specified, the given :n:`@one_pattern`.
 
       If the inferred type
-      of :n:`@qualid` does not start with a product, :tacn:`exact` :n:`@qualid` is added
-      to the hint list.  If the type can be reduced to a type starting with a product,
-      :tacn:`simple apply` :n:`@qualid` is also added to the hints list.
+      of :n:`@qualid` does not start with a product, the command adds :tacn:`exact`
+      :n:`@qualid` to the hint list.  If the inferred type starts with a product,
+      the command adds :tacn:`simple apply` :n:`@qualid` to the hints list.  Note that
+      unlike :tacn:`auto` and :tacn:`eauto`,
+      :tacn:`typeclasses eauto` uses a tactic equivalent to :tacn:`autoapply`,
+      which behaves somewhat differently from :tacn:`simple apply`.
+      Nonetheless, that tactic's debug output and the hint database misleadingly show
+      :tacn:`simple apply`.
 
       If the inferred type of :n:`@qualid` contains a dependent
       quantification on a variable which occurs only in the premises of the type
@@ -466,6 +515,12 @@ Creating Hints
          .. warn:: Declaring arbitrary terms as hints is fragile and deprecated; it is recommended to declare a toplevel constant instead
             :undocumented:
 
+      :n:`@one_pattern`
+        Overrides the default pattern, which may occasionally be useful.  For
+        example, if a hint has the default pattern `_ = _`, you could limit
+        the hint being tried only for `bool`s with the pattern
+        `(@eq bool _ _)`.
+
       .. exn:: @qualid cannot be used as a hint
 
          The head symbol of the type of :n:`@qualid` is a bound variable
@@ -488,7 +543,8 @@ Creating Hints
 
       For each :n:`@qualid` that is an inductive type, adds all its constructors as
       hints of type ``Resolve``. Then, when the conclusion of current goal has the form
-      :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor.
+      :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor using
+      :tacn:`exact`.
 
       .. exn:: @qualid is not an inductive type
          :undocumented:
@@ -503,28 +559,90 @@ Creating Hints
       :name: Hint Transparent; Hint Opaque
 
       Adds transparency hints to the database, making each :n:`@qualid`
-      a transparent or opaque constant during resolution. This information is used
-      during unification of the goal with any lemma in the database and inside the
-      discrimination network to relax or constrain it in the case of discriminated
-      databases.
+      transparent or opaque during resolution.  The proof search tactics use
+      unification to determine whether to try most hints, for example checking if
+      the goal unifies with the theorem used in a :cmd:`Hint Resolve` hint.  See
+      :ref:`here <hint_performance_considerations>` for a description of how
+      opaque and transparent affect which hints are tried.
+      Note that transparency hints are independent of the non-hint :cmd:`Opaque`
+      and :n:`Transparent` settings.
+
+      .. example:: Transparency with Multiple Hint Databases
+
+         To use different transparency settings for particular hints, put them
+         in separate hint databases with distinct transparency settings and use
+         :tacn:`typeclasses eauto`.  (This doesn't work for :tacn:`auto` or :tacn:`eauto`.):
+
+         .. coqtop:: in
+
+            Definition one := 1.
+            Theorem thm : one = 1. reflexivity. Qed.
+
+            Create HintDb db1.
+            Hint Opaque one : db1.
+            Hint Resolve thm | 1 : db1.
+            Create HintDb db2.
+
+            Goal 1 = 1.
+            (* "one" is not unfolded because it's opaque in db1 *)
+            Fail typeclasses eauto with db1 db2 nocore.
+            Succeed eauto with db1 db2 nocore.           (* doesn't work with eauto *)
+            Succeed auto with db1 db2 nocore.            (* doesn't work with auto *)
+
+            Hint Resolve thm | 2 : db2.
+            (* "one" is unfolded because it's transparent (by default) in db2 *)
+            Succeed typeclasses eauto with db1 db2 nocore.
+
+         .. coqtop:: none
+
+            Abort.
+
+      .. example:: Independence of Hint Opaque and Opaque
+
+         .. coqtop:: reset in
+
+            Definition one := 1.
+            Opaque one.  (* not relevant to hint selection *)
+
+            Theorem bar: 1=1.  reflexivity.  Qed.
+
+            Create HintDb db.       (* constants, etc. transparent by default *)
+            Hint Opaque one : db.   (* except for "one" *)
+            Hint Resolve bar : db.  (* hint is not tried if one is Hint Opaque *)
+            Set Typeclasses Debug Verbosity 1.
+
+            Goal one = 1.
+            Fail typeclasses eauto with db nocore.  (* fail: no match for (one = 1) *)
+
+            Hint Transparent one : db.
+            Succeed typeclasses eauto with db nocore.  (* success: now bar is tried *)
+            Fail unfold one.                           (* fail: one is still Opaque *)
+
+         .. coqtop:: none
+
+            Abort.
 
       .. exn:: Cannot coerce @qualid to an evaluable reference.
          :undocumented:
 
    .. cmd:: Hint {| Constants | Projections | Variables } {| Transparent | Opaque } {? : {+ @ident } }
       :name: Hint Constants; Hint Projections; Hint Variables
 
-      Sets the transparency flag for constants, projections or variables for the specified hint
-      databases.
-      These flags affect the unification of hints in the database.
-      We advise using this just after a :cmd:`Create HintDb` command.
+      Sets the default transparency for constants, projections or variables for
+      the specified hint databases.  Existing transparency settings for individual
+      items (e.g., set with :cmd:`Hint Opaque`) are dropped.
+      We advise using this command just after a :cmd:`Create HintDb` command.
 
    .. cmd:: Hint Extern @natural {? @one_pattern } => @ltac_expr {? : {+ @ident } }
 
       Extends :tacn:`auto` with tactics other than :tacn:`apply` and
       :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_pattern` is the pattern
       to match and :n:`@ltac_expr` is the action to apply.
 
+      We recommend providing a pattern whenever possible.  Hints with patterns
+      are tried only if the pattern matches without unfolding transparent constants
+      (i.e., a syntactic match).  Hints without patterns are always tried.
+
       **Usage tip**: tactics that can succeed even if they don't change the context,
       such as most of the :ref:`conversion tactics <applyingconversionrules>`, should
       be prefaced with :tacn:`progress` to avoid needless repetition of the tactic.
@@ -539,8 +657,8 @@ Creating Hints
 
             Hint Extern 4 (~(_ = _)) => discriminate : core.
 
-         Now, when the head of the goal is a disequality, ``auto`` will try
-         discriminate if it does not manage to solve the goal with hints with a
+         Now, when the head of the goal is an inequality, ``auto`` will try
+         `discriminate` if it does not manage to solve the goal with hints with a
          cost less than 4.
 
       One can even use some sub-patterns of the pattern in
@@ -723,11 +841,14 @@ Creating Hints
 
 .. cmd:: Print HintDb @ident
 
-   This command displays all hints from database :n:`@ident`.  Hints
-   in each group ("For ... ->") are shown in the order in which they will be tried
-   (first to last).  The groups are shown ordered alphabetically on the last component of
-   the symbol name.  Note that hints with the same cost are tried in
-   reverse of the order they're defined in, i.e., last to first.
+   This command displays all hints from database :n:`@ident`.  Hints are grouped by
+   the :term:`head constants <head constant>` of their patterns ("For ... ->").
+   The groups are shown ordered alphabetically on the last component of the head
+   constant name.   Within each group, hints are shown in the order in which they
+   will be tried (first to last).  Note that hints with the same cost are tried in
+   reverse of the order they're defined in, i.e., last defined is used first.
+   Mode of resolution symbols, :n:`{+ {| + | ! | - } }`, when defined with
+   :cmd:`Hint Mode`, appear after the head constant.
 
 Hint locality
 `````````````

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

@@ -533,10 +533,8 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
        unfolding is applied to all constants that are not listed.
        Notice that the ``delta`` doesn't apply to variables bound by a let-in
        construction inside the term itself (use ``zeta`` to inline these).
-       Opaque constants are never unfolded except by :tacn:`vm_compute` and
-       :tacn:`native_compute`
-       (see `#4476 <https://github.com/coq/coq/issues/4476>`_ and
-       :ref:`controlling-the-reduction-strategies`).
+       Opaque constants are not unfolded by most tactics
+       (see :ref:`controlling-the-reduction-strategies`).
 
    `iota`
      :term:`iota-reduction` of pattern matching (`match`) over a constructed term and reduction
@@ -977,13 +975,28 @@ The commands to fine-tune the reduction strategies and the lazy conversion
 algorithm are described in this section.  Also see :ref:`Args_effect_on_unfolding`,
 which supports additional fine-tuning.
 
+:gdef:`Opaqueness <opaque>` is used to control whether constants can be
+:term:`unfolded <unfold>` with :term:`delta-reduction`.  Opaque means not to
+do unfolding is some cases, while :gdef:`Transparent <transparent>` permits
+unfolding.  Rocq has multiple notions of opaque:
+
+- **Sealed.**  Theorems ending with :cmd:`Qed` are permanently
+  marked `opaque`.  These are never unfolded and they can't be made transparent.
+- **Changeably opaque or transparent.**  Theorems ending with :cmd:`Defined`
+  and constants default to `transparent` (unfoldable).  "Constants" include items defined by
+  commands such as :cmd:`Definition`, :cmd:`Let` (with an explicit body),
+  :cmd:`Fixpoint`, :cmd:`CoFixpoint` and :cmd:`Function`.  Their opacity can
+  be changed at any time with the :cmd:`Opaque` and :cmd:`Transparent` commands.
+  Conversion tactics such as :tacn:`simpl` and :tacn:`unfold` only unfold transparent
+  constants.  Tactics that
+  use unification, such as :tacn:`reflexivity` and :tacn:`apply` may unfold
+  changeably opaque constants, as can :tacn:`vm_compute` and :tacn:`native_compute`
+  (see `#4476 <https://github.com/coq/coq/issues/4476>`_).
+- The :cmd:`Strategy` command provides some additional refinements (all changeable).
+
 .. cmd:: Opaque {? ! } {+ @reference }
 
-   Marks the specified constants as :term:`opaque` so tactics won't :term:`unfold` them
-   with :term:`delta-reduction`.
-   "Constants" are items defined by commands such as :cmd:`Definition`,
-   :cmd:`Let` (with an explicit body), :cmd:`Fixpoint`, :cmd:`CoFixpoint`
-   and :cmd:`Function`.
+   Marks the specified constants as changeably opaque.
 
    This command accepts the :attr:`global` attribute.  By default, the scope
    of :cmd:`Opaque` is limited to the current section or module.

test-suite/output/disc_uses_patterns.out

@@ -0,0 +1,22 @@
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+File "./output/disc_uses_patterns.v", line 13, characters 0-40:
+The command has indeed failed with message:
+Failed to progress.
+Debug:
+Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in regular mode, unbounded
+Debug: Launching resolution fixpoint on 1 goals: ?X6 : (3 = 3)
+Debug:
+Calling fixpoint on : 1 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run.
+Stuck: 
+Failed: 
+Initial: Goal 1 evar: ?X6 status: initial
+Debug: considering goal 1 of status initial
+Debug: 1: looking for (3 = 3) without backtracking
+Debug: 1: no match for (3 = 3), 0 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_uses_patterns.v", line 14, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.

test-suite/output/disc_uses_patterns.v

@@ -0,0 +1,15 @@
+(* discriminated uses head const and patterns *)
+Theorem bar: 1=1.  reflexivity.  Qed.
+Theorem bar2: 2=2.  reflexivity.  Qed.
+
+Create HintDb db discriminated .
+Hint Resolve bar : db.
+Hint Resolve bar2 : db.
+
+Set Typeclasses Debug Verbosity 2.
+
+Goal 3=3.
+(* neither theorem matches the goal *)
+Fail progress debug auto with db nocore.
+Fail typeclasses eauto with db nocore.
+Abort.