Stream: Coq devs & plugin devs

Topic: Help binding Hint Resolve


view this post on Zulip Enrico Tassi (Feb 07 2022 at 11:09):

Apparently Hint Resolve takes an optional pattern.
Can someone give me an example where the pattern is used (makes a difference)?

view this post on Zulip Janno (Feb 07 2022 at 11:41):

Do you want a real-world example or would an artificial one suffice?

view this post on Zulip Enrico Tassi (Feb 07 2022 at 11:49):

The tiniest the better.

view this post on Zulip Janno (Feb 07 2022 at 12:03):

Here is one that loops if you don't specify the pattern:

Class mypred {A} (l : list A) := {}.
Lemma mypred_general {A} (l : list A) : @mypred A nil -> mypred l -> mypred l. Admitted.
#[local] Hint Resolve mypred_general | (mypred nil) : typeclass_instances.
Goal forall A (l : list A), mypred l. Fail apply _. Abort.

view this post on Zulip Janno (Feb 07 2022 at 12:04):

I guess you could use Timeout 1 Fail apply _. With the pattern the search fails instantly so one second should be plenty even for CI.

view this post on Zulip Enrico Tassi (Feb 07 2022 at 12:15):

OK, so it is relevant for typeclasses_eauto... I was trying calling trivial :-/

view this post on Zulip Kazuhiko Sakaguchi (Feb 07 2022 at 12:40):

It seems that we can replace this line: https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrnum.v#L1565
with Hint Resolve normr_ge0 | (is_true (0 <= norm _)) : core. So it is orthogonal to type classes. Right?

view this post on Zulip Gaëtan Gilbert (Feb 07 2022 at 12:43):

It seems that we can replace this line

Only if the differences between ssr apply: and Hint Resolve don't matter

view this post on Zulip Enrico Tassi (Feb 07 2022 at 12:44):

We call trivial, what the game of apply:?

view this post on Zulip Enrico Tassi (Feb 07 2022 at 12:44):

Looking at the doc, anyway, I can't see where the pattern is used.

view this post on Zulip Janno (Feb 07 2022 at 13:05):

You can see the pattern in Print HintDb

view this post on Zulip Janno (Feb 07 2022 at 13:06):

It's the exact same kind of pattern as the one derived by Hint Resolve without an explicit pattern. Not to be confused with the pattern of Hint Extern which is printed the same way but behaves entirely different. (Hint Extern patterns are matching purely syntactically, disregarding hint transparency.)

view this post on Zulip Enrico Tassi (Feb 07 2022 at 15:00):

I see it, but I could not find a place where the manual explain when it is used, exactly.


Last updated: Mar 29 2024 at 01:40 UTC