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 04 2023 at 23:01 UTC