Stream: Coq users

Topic: Cant get Hint Cut to work


view this post on Zulip Wessel de Weijer (Feb 20 2022 at 15:03):

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?

view this post on Zulip Kenji Maillard (Feb 20 2022 at 15:23):

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.

view this post on Zulip Wessel de Weijer (Feb 20 2022 at 15:52):

Ah, thanks. That does explain eauto not working. I guess my brain always subconsiously ignores warnings... :upside_down:


Last updated: Jan 31 2023 at 12:01 UTC