I want to create a simple Hint database and I'm trying to reduce the search tree (mostly just to make the debug eauto
output easier to parse). I believe Hint Cut
is supposed to do exactly that but I can't get it to work and the documentation is a little sparse. Here's a minimal example that I think should work but doesn't:
Inductive foo : Prop := f : foo -> foo.
Create HintDb foodb.
Goal foo. debug eauto with foodb. Abort.
Global Hint Resolve f : foodb.
Goal foo. debug eauto with foodb. Abort.
Global Hint Cut [_* f f] : foodb.
Print HintDb foodb.
Goal foo. debug eauto with foodb. Abort.
Global Hint Cut [_*] : foodb.
Print HintDb foodb.
Goal foo. debug eauto with foodb. Abort.
As expected, without any cut, eauto will recurse until max depth. Adding the [_* f f]
cut I would expect eauto to not try to apply f
more than once but it still recurses. In fact, adding the degenerated [_*]
cut doesn't do anything either.
Is there something simple I'm not getting or should I really be switching to a newer tactic language?
I have never used Hint Cut
but in the documentation there is a warning at the end saying
These hints currently only apply to typeclass proof search and the typeclasses eauto tactic.
Ah, thanks. That does explain eauto
not working. I guess my brain always subconsiously ignores warnings... :upside_down:
Last updated: Oct 13 2024 at 01:02 UTC