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/addendum/type-classes.rst

@@ -492,10 +492,18 @@ Command summary
      to remain at any point during search.
 
      When :n:`with` is not specified, :tacn:`typeclasses eauto` uses
-     the ``typeclass_instances`` database by default (instead of ``core``).
+     the ``typeclass_instances`` database by default.  (If `with` is provided,
+     you must explicitly specify `typeclass_instances` to use it.)
+     Unlike :tacn:`auto` and :tacn:`eauto`, `core` is not automatically included.
      Dependent subgoals are automatically shelved, and shelved goals can
      remain after resolution ends (following the behavior of Coq 8.5).
 
+     .. comment
+        if `with` given then typeclases_eauto must be explicit:
+          Tac2tactics.typeclasses_eauto (read code)
+          and Class_tactics.e_my_find_search (with debugger)
+        core not automatically included: test-suite/success/tceauto_nocore.v
+
      .. note::
         ``all:once (typeclasses eauto)`` faithfully
         mimics what happens during typeclass resolution when it is called

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/proof-engine/tactics.rst

@@ -1431,7 +1431,7 @@ Managing the local context
 
 .. tacn:: remember @one_term {? @as_name } {? eqn : @naming_intropattern } {? in @goal_occurrences }
 
-   Similar to :n:`set (@ident := @one_term) in *` but creates a hypothesis using
+   Similar to :tacn:`set` :n:`(@ident := @one_term) in *` but creates a hypothesis using
    :term:`Leibniz equality` to remember the relation between the introduced
    variable and the term rather than creating a
    :term:`local definition <context-local definition>`.  If :n:`@as_name` is not

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.

test-suite/output/disc_with_transparent.out

@@ -0,0 +1,134 @@
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* exact bar2 (in db). (*fail*)
+File "./output/disc_with_transparent.v", line 18, 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 : (two + 1 + 1 = 5)
+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 (two + 1 + 1 = 5) without backtracking
+Debug: 1.1: exact bar2 on (two + 1 + 1 = 5) failed with: Unable to unify
+ "3 + 1 + 1 = 5"
+with "two + 1 + 1 = 5".
+Debug: 1: no match for (two + 1 + 1 = 5), 1 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_with_transparent.v", line 19, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* exact bar (in db). (*fail*)
+File "./output/disc_with_transparent.v", line 24, 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: ?X8 : (1 + 1 + 1 = one)
+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: ?X8 status: initial
+Debug: considering goal 1 of status initial
+Debug: 1: looking for (1 + 1 + 1 = one) without backtracking
+Debug: 1.1: exact bar on (1 + 1 + 1 = one) failed with: Unable to unify
+ "1 + 1 + 1 = 3"
+with "1 + 1 + 1 = one".
+Debug: 1: no match for (1 + 1 + 1 = one), 1 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_with_transparent.v", line 25, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* exact bar2 (in db). (*fail*)
+* exact bar (in db). (*fail*)
+File "./output/disc_with_transparent.v", line 30, 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: ?X10 : (two + 1 + 1 = one)
+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: ?X10 status: initial
+Debug: considering goal 1 of status initial
+Debug: 1: looking for (two + 1 + 1 = one) without backtracking
+Debug: 1.1: exact bar2 on (two + 1 + 1 = one) failed with: Unable to unify
+ "3 + 1 + 1 = 5"
+with "two + 1 + 1 = one".
+Debug: 1.1: exact bar on (two + 1 + 1 = one) failed with: Unable to unify
+ "1 + 1 + 1 = 3"
+with "two + 1 + 1 = one".
+Debug: 1: no match for (two + 1 + 1 = one), 2 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_with_transparent.v", line 31, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+File "./output/disc_with_transparent.v", line 36, 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:
+?X12 : (1 + 1 + 1 = 1 + 1 + 1)
+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: ?X12 status: initial
+Debug: considering goal 1 of status initial
+Debug: 1: looking for (1 + 1 + 1 = 1 + 1 + 1) without backtracking
+Debug: 1: no match for (1 + 1 + 1 = 1 + 1 + 1), 0 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_with_transparent.v", line 37, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* exact bar (in db). (*success*)
+File "./output/disc_with_transparent.v", line 46, characters 5-26:
+The command has indeed failed with message:
+Unable to unify "1 + 1 + 1 = 3" with "1 + 1 + 1 = one_plus_one_plus_one".
+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:
+?X14 : (1 + 1 + 1 = one_plus_one_plus_one)
+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: ?X14 status: initial
+Debug: considering goal 1 of status initial
+Debug:
+1: looking for (1 + 1 + 1 = one_plus_one_plus_one) without backtracking
+Debug: 1.1: exact bar on
+(1 + 1 + 1 = one_plus_one_plus_one) failed with: Unable to unify
+ "1 + 1 + 1 = 3"
+with "1 + 1 + 1 = one_plus_one_plus_one".
+Debug: 1: no match for (1 + 1 + 1 = one_plus_one_plus_one), 1 possibilities
+Debug:
+Goal 1 has no more solutions, returning exception: Proof-search failed.
+File "./output/disc_with_transparent.v", line 50, characters 5-37:
+The command has indeed failed with message:
+Tactic failure: Proof search failed.

test-suite/output/disc_with_transparent.v

@@ -0,0 +1,51 @@
+(* discriminated database with transparent items in hints *)
+From Stdlib Require Import PeanoNat.
+Theorem bar: 1+1+1=3.  reflexivity.  Qed.
+Theorem bar2: 3+1+1=5.  reflexivity.  Qed.
+
+Definition one := 1.
+Definition two := 2.
+Definition one_plus_one_plus_one := 1+1+1.
+
+Create HintDb db discriminated.
+Hint Resolve bar | 2 : db.
+Hint Resolve bar2 | 1 : db.
+Hint Opaque Nat.add : db.
+Set Typeclasses Debug Verbosity 2.
+
+Goal two+1+1=5.
+(* matches bar2, which fails in the tactic*)
+Fail progress debug auto with db nocore.
+Fail typeclasses eauto with db nocore.
+Abort.
+
+Goal 1+1+1=one.
+(* matches bar, which fails in the tactic *)
+Fail progress debug auto with db nocore.
+Fail typeclasses eauto with db nocore.
+Abort.
+
+Goal two+1+1=one.
+(* matches both bar and bar2, which both fail in the tactic *)
+Fail progress debug auto with db nocore.
+Fail typeclasses eauto with db nocore.
+Abort.
+
+Goal 1+1+1=1+1+1.
+(* no match, fails *)
+Fail progress debug auto with db nocore.
+Fail typeclasses eauto with db nocore.
+Abort.
+
+Goal 1+1+1=one_plus_one_plus_one.
+(* matches bar, succeeds because tactic uses conversion *)
+Succeed progress debug auto with db nocore.
+
+Succeed exact bar.
+Succeed simple apply bar.
+Fail autoapply bar with db.  (* a bug or poor documentation? *)
+
+Set Typeclasses Debug Verbosity 2.
+(* fails because tc eauto uses autoapply, copying that Nat.add is opaque *)
+Fail typeclasses eauto with db nocore.
+Abort.

test-suite/output/extern_no_pattern.out

@@ -0,0 +1,35 @@
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+2
+* (*external*) (idtac "2"; fail) (in db). (*fail*)
+1
+* (*external*) (idtac "1"; fail) (in db). (*fail*)
+* (*external*) (apply bar) (in db). (*success*)
+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: ?X4 : (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: ?X4 status: initial
+Debug: considering goal 1 of status initial
+Debug: 1: looking for (3 = 3) without backtracking
+2
+Debug: 1.1: (*external*) (idtac "2"; fail) on
+(3 = 3) failed with: Tactic failure.
+1
+Debug: 1.1: (*external*) (idtac "1"; fail) on
+(3 = 3) failed with: Tactic failure.
+Debug: 1.1: (*external*) (apply bar) on (3 = 3), 0 subgoal(s)
+Debug:
+1.1: after (*external*) (apply bar) finished, 0 goals are shelved and unsolved ( )
+Debug: Goal 1 has a success, continuing resolution
+Debug:
+Calling fixpoint on : 0 initial goals, 0 stuck goals and 0 non-stuck failures kept with progress made in this run.
+Stuck: 
+Failed: 
+Initial: 
+Debug: Result goals after fixpoint: 0 goals: 
+Debug: after eauto_tac_stuck: 0 goals: 

test-suite/output/extern_no_pattern.v

@@ -0,0 +1,15 @@
+(* Hint Extern with no pattern always selected *)
+Theorem bar: 3=3.  reflexivity.  Qed.
+
+Create HintDb db discriminated.
+Hint Extern 1 => idtac "1"; fail : db.
+Hint Extern 1 => idtac "2"; fail : db.
+Hint Extern 2 => apply bar : db.
+Set Typeclasses Debug Verbosity 2.
+
+
+Goal 3=3.
+(* all 3 Hint Extern are tried *)
+Succeed progress debug auto with db nocore.
+Succeed typeclasses eauto with db nocore.
+Abort.