From dab2676aebac817abbbc9a2634671c3995f69d08 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 21 Oct 2024 20:49:26 -0700 Subject: [PATCH] Refine Hint Opaque/Transparent doc --- .../19761-hintdb_doc.rst | 5 + doc/sphinx/addendum/type-classes.rst | 10 +- doc/sphinx/language/core/conversion.rst | 5 +- doc/sphinx/proof-engine/tactics.rst | 2 +- doc/sphinx/proofs/automatic-tactics/auto.rst | 212 ++++++++++++++---- doc/sphinx/proofs/writing-proofs/equality.rst | 31 ++- test-suite/output/disc_uses_patterns.out | 22 ++ test-suite/output/disc_uses_patterns.v | 15 ++ test-suite/output/disc_with_transparent.out | 134 +++++++++++ test-suite/output/disc_with_transparent.v | 51 +++++ test-suite/output/extern_no_pattern.out | 35 +++ test-suite/output/extern_no_pattern.v | 15 ++ test-suite/output/nondisc_ignores_pattern.out | 28 +++ test-suite/output/nondisc_ignores_pattern.v | 15 ++ .../success/hint_extern_syntactic_unify.v | 14 ++ test-suite/success/tceauto_nocore.v | 4 + .../success/transparency_multi_hintdb.v | 17 ++ 17 files changed, 557 insertions(+), 58 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/19761-hintdb_doc.rst create mode 100644 test-suite/output/disc_uses_patterns.out create mode 100644 test-suite/output/disc_uses_patterns.v create mode 100644 test-suite/output/disc_with_transparent.out create mode 100644 test-suite/output/disc_with_transparent.v create mode 100644 test-suite/output/extern_no_pattern.out create mode 100644 test-suite/output/extern_no_pattern.v create mode 100644 test-suite/output/nondisc_ignores_pattern.out create mode 100644 test-suite/output/nondisc_ignores_pattern.v create mode 100644 test-suite/success/hint_extern_syntactic_unify.v create mode 100644 test-suite/success/tceauto_nocore.v create mode 100644 test-suite/success/transparency_multi_hintdb.v diff --git a/doc/changelog/08-vernac-commands-and-options/19761-hintdb_doc.rst b/doc/changelog/08-vernac-commands-and-options/19761-hintdb_doc.rst new file mode 100644 index 000000000000..1dcb8f4f9558 --- /dev/null +++ b/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 `_, + by Jim Fehrle). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index f5f429813594..10d81ae26b02 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/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 diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 71d857526e30..645f3a6a3ce4 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -141,9 +141,8 @@ or :term:`constants ` defined in the :term:`global environment` with t -------------- E[Γ] ⊢ c~\triangleright_δ~t -:term:`Delta-reduction ` only unfolds :term:`constants ` that are -marked :gdef:`transparent`. :gdef:`Opaque ` is the opposite of -transparent; :term:`delta-reduction` doesn't unfold opaque constants. +:term:`Delta-reduction ` unfolds constants when permitted by their +:term:`opaqueness ` settings. ι-reduction ~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 483925c00bb6..877408e35d69 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/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 `. If :n:`@as_name` is not diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 8a47a5bf82a6..a5ea8321e066 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -24,6 +24,10 @@ Tactics tries to apply one of them. This process is recursively applied to the generated subgoals. + .. comment "introduces the newly generated hyps as hints": done in + Hints.make_local_hint_db, which also adds constructor hints. eauto + also calls this, tc eauto uses different code + Within each hintbase, lower cost tactics are tried before higher-cost tactics. When multiple hintbases are specified, all hints in the first database are tried before any in the second database (and so forth) @@ -107,7 +111,7 @@ Tactics Generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, :tacn:`eauto` will try them. Also, :tacn:`eauto` internally uses :tacn:`eassumption` - instead of :tacn:`assumption` and a tactic similar to :tacn:`simple eapply` + instead of :tacn:`assumption` and, when needed, a tactic similar to :tacn:`simple eapply` instead of a tactic similar to :tacn:`simple apply`. As a consequence, :tacn:`eauto` can solve goals such as: @@ -318,35 +322,78 @@ 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 `_). + 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 + `_), + treating everything as hint opaque. - By default, hint databases are undiscriminated. + Otherwise (if there is no pattern), all hints will be tried. (Therefore, provide a + pattern in `Extern` hints whenever possible.) + +.. 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 ``````````````````````````````````````````````````` Several hint databases are defined in the Rocq standard library. The -database contains all hints declared -to belong to it in the currently loaded modules. -In particular, requiring new modules may extend the database. +database contains all hints declared for it in the currently loaded modules. +Requiring additional modules (:cmd:`Require`) may add more hints. At Rocq startup, only the core database is nonempty and ready to be used immediately. :core: This special database is automatically used by ``auto``, except when @@ -380,7 +427,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 +479,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 +518,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 +546,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,10 +562,68 @@ 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 ` 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, where bar is *) + Fail typeclasses eauto with db1 db2 nocore. (* fails with tc eauto *) + Succeed eauto with db1 db2 nocore. (* ignores the distinction *) + Succeed auto with db1 db2 nocore. (* ignores the distinction *) + + 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: @@ -514,10 +631,10 @@ Creating Hints .. 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 } } @@ -525,6 +642,10 @@ Creating Hints :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 `, should be prefaced with :tacn:`progress` to avoid needless repetition of the tactic. @@ -539,8 +660,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 +844,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 ` 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 ````````````` diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst index b94ea85d6bf8..6510b274b09c 100644 --- a/doc/sphinx/proofs/writing-proofs/equality.rst +++ b/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 `_ 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 ` is used to control whether constants can be +:term:`unfolded ` with :term:`delta-reduction`. Opaque means not to +do unfolding is some cases, while :gdef:`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 `_). +- 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. diff --git a/test-suite/output/disc_uses_patterns.out b/test-suite/output/disc_uses_patterns.out new file mode 100644 index 000000000000..800d2d2fe2df --- /dev/null +++ b/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. diff --git a/test-suite/output/disc_uses_patterns.v b/test-suite/output/disc_uses_patterns.v new file mode 100644 index 000000000000..676412c42a1e --- /dev/null +++ b/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. diff --git a/test-suite/output/disc_with_transparent.out b/test-suite/output/disc_with_transparent.out new file mode 100644 index 000000000000..83885fd77a7e --- /dev/null +++ b/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. diff --git a/test-suite/output/disc_with_transparent.v b/test-suite/output/disc_with_transparent.v new file mode 100644 index 000000000000..87a6b540ffbe --- /dev/null +++ b/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. diff --git a/test-suite/output/extern_no_pattern.out b/test-suite/output/extern_no_pattern.out new file mode 100644 index 000000000000..e0b45526df0e --- /dev/null +++ b/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: diff --git a/test-suite/output/extern_no_pattern.v b/test-suite/output/extern_no_pattern.v new file mode 100644 index 000000000000..95917310c5a4 --- /dev/null +++ b/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. diff --git a/test-suite/output/nondisc_ignores_pattern.out b/test-suite/output/nondisc_ignores_pattern.out new file mode 100644 index 000000000000..3b6c02beb11b --- /dev/null +++ b/test-suite/output/nondisc_ignores_pattern.out @@ -0,0 +1,28 @@ +(* debug auto: *) +* assumption. (*fail*) +* intro. (*fail*) +* exact bar2 (in db). (*fail*) +* exact bar (in db). (*fail*) +File "./output/nondisc_ignores_pattern.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.1: exact bar2 on (3 = 3) failed with: Unable to unify +"2 = 2" with "3 = 3". +Debug: 1.1: exact bar on (3 = 3) failed with: Unable to unify +"1 = 1" with "3 = 3". +Debug: 1: no match for (3 = 3), 2 possibilities +Debug: +Goal 1 has no more solutions, returning exception: Proof-search failed. +File "./output/nondisc_ignores_pattern.v", line 14, characters 5-37: +The command has indeed failed with message: +Tactic failure: Proof search failed. diff --git a/test-suite/output/nondisc_ignores_pattern.v b/test-suite/output/nondisc_ignores_pattern.v new file mode 100644 index 000000000000..3f1b36e418a6 --- /dev/null +++ b/test-suite/output/nondisc_ignores_pattern.v @@ -0,0 +1,15 @@ +(* nondiscriminated uses head const, ignores patterns *) +Theorem bar: 1=1. reflexivity. Qed. +Theorem bar2: 2=2. reflexivity. Qed. + +Create HintDb db. (* not discriminated *) +Hint Resolve bar : db. +Hint Resolve bar2 : db. + +Set Typeclasses Debug Verbosity 2. + +Goal 3=3. +(* no matching; both theorems are tried. *) +Fail progress debug auto with db nocore. +Fail typeclasses eauto with db nocore. +Abort. diff --git a/test-suite/success/hint_extern_syntactic_unify.v b/test-suite/success/hint_extern_syntactic_unify.v new file mode 100644 index 000000000000..680fd9ad6a17 --- /dev/null +++ b/test-suite/success/hint_extern_syntactic_unify.v @@ -0,0 +1,14 @@ +(* Hint Extern uses syntactic unification *) +Definition one := 1. +Theorem bar: 1=one. reflexivity. Qed. + +Create HintDb db discriminated. +Hint Extern 1 (1=one) => apply bar : db. + +Set Typeclasses Debug Verbosity 2. + +Goal one=1. +(* fail as expected; "one" is not expanded *) +Fail progress debug auto with db nocore. +Fail typeclasses eauto with db nocore. +Abort. diff --git a/test-suite/success/tceauto_nocore.v b/test-suite/success/tceauto_nocore.v new file mode 100644 index 000000000000..fdc870751dbe --- /dev/null +++ b/test-suite/success/tceauto_nocore.v @@ -0,0 +1,4 @@ +(* tc eauto doesn't automatically include core *) +Goal True. +Fail typeclasses eauto. +Succeed typeclasses eauto with core. diff --git a/test-suite/success/transparency_multi_hintdb.v b/test-suite/success/transparency_multi_hintdb.v new file mode 100644 index 000000000000..d5b4c86d13fa --- /dev/null +++ b/test-suite/success/transparency_multi_hintdb.v @@ -0,0 +1,17 @@ +(* constant transparent in one hintdb but not the other *) + +Definition one := 1. +Theorem thm : one = 1. reflexivity. Qed. +Create HintDb db1 discriminated. +Hint Opaque one : db1. +Hint Resolve thm | 1 : db1. +Create HintDb db2 discriminated. + +Goal 1 = 1. +Fail typeclasses eauto with db1 db2 nocore. +Succeed eauto with db1 db2 nocore. (* bug! *) +Succeed auto with db1 db2 nocore. (* bug! *) + +Hint Resolve thm | 2 : db2. +Succeed typeclasses eauto with db1 db2 nocore. +Abort.