Stream: Coq users

Topic: Using Hint Extern to progress

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 10:16):

Hi all, maybe it's a silly question but is there a way to use hints defined with Hint Extern to progress even if it does not conclude the goal?
I use them to do some typeclass inference and in case it does find an instance eauto with typeclass_instances seems to behave mostly has exact _. But in some cases, it will not find an instance, but I would still like to apply the hints and get the sub-goal it failed to solve as a sub-goal.

Is there already a tactic that does this? eauto with typeclass_instances or even eauto with mydb don't seem to apply the hint if it doesn't solve the goal.

Thanks.

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 10:42):

You can use || shelve I guess to get the subgoal

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 10:42):

(using typeclasses eauto)

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 10:43):

This PR https://github.com/coq/coq/pull/13952 should also help in the future

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 10:57):

You mean this?

unshelve (typeclasses eauto || shelve).

For me it still doesn't do anything.

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:00):

Matthieu Sozeau said:

This PR https://github.com/coq/coq/pull/13952 should also help in the future

Sounds interesting, but this only for error reporting (which is great).
I would like to actually get the subgoal and then solve it interactively.

I guess my question is: when does eauto apply hints even if they do not conclude the goal?

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:02):

There is a new best_effort option that could give you subgoals

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:03):

Can you show your Hint Extern?

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:03):

You shouldn't unshelve

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:04):

My Hint is

#[export] Hint Extern 2 (ValidPackage ?L ?I ?E (mkfmap ((?i, mkdef ?A ?B ?f) :: ?p)))
  =>
  eapply valid_package_cons ; [
    eapply valid_package_from_class
  | intro ; eapply valid_code_from_class
  | unfold "\notin" ; rewrite imfset_fset ; rewrite in_fset ; eauto
  ]
  : typeclass_instances packages.

Sorry for no context.

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:05):

Matthieu Sozeau said:

You shouldn't unshelve

typeclasses eauto || shelve.
Unshelve.

is also the identity.

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:06):

The idea is that if you want a goal to remain after resolution, you just need to shelve it, so you shelve in the Hint Extern or you add a Hint with low precedence which shelves the subgoal if not other hint could apply. Then resolution proceeds on the rest of the goals and keeps the shelved subgoals until the end

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:06):

Matthieu Sozeau said:

There is a new best_effort option that could give you subgoals

https://coq.inria.fr/refman/search.html?q=best_effort&check_keywords=yes&area=default gives no result. How should I use it?

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:06):

That's introduced by the PR above, so not there yet

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:06):

Matthieu Sozeau said:

The idea is that if you want a goal to remain after resolution, you just need to shelve it, so you shelve in the Hint Extern or you add a Hint with low precedence which shelves the subgoal if not other hint could apply. Then resolution proceeds on the rest of the goals and keeps the shelved subgoals until the end

I see, thanks.

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:07):

It is not advised to use eauto in a hint extern. You should rather give back control to the proof-search. But you might want to do typeclasses eauto || shelve in this case.

view this post on Zulip Matthieu Sozeau (Apr 19 2021 at 11:08):

Another PR allows to have more control in Hint Extern: https://github.com/coq/coq/pull/6285, but again, it's not there yet

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 11:46):

Matthieu Sozeau said:

It is not advised to use eauto in a hint extern. You should rather give back control to the proof-search. But you might want to do typeclasses eauto || shelve in this case.

I was using eauto there because the goal there is not a class.

Thanks for your help!

view this post on Zulip Théo Zimmermann (Apr 19 2021 at 12:23):

I was using eauto there because the goal there is not a class.

This isn't relevant. You should probably always rely on typeclasses eauto even when solving non-class goals. Just use different hint databases with the with clause.

view this post on Zulip Théo Zimmermann (Apr 19 2021 at 12:24):

And BTW, see also https://hal.archives-ouvertes.fr/hal-01671994 (it's becoming quite old as a reference, I know that @Clément Pit-Claudel and others have been using these techniques recently but I don't think anyone else has written about them yet).

view this post on Zulip Théo Winterhalter (Apr 19 2021 at 12:31):

Théo Zimmermann said:

I was using eauto there because the goal there is not a class.

This isn't relevant. You should probably always rely on typeclasses eauto even when solving non-class goals. Just use different hint databases with the with clause.

Oh thanks, that's the thing I was missing!

view this post on Zulip Clément Pit-Claudel (Apr 19 2021 at 15:01):

I'm using this technique here: https://github.com/mit-plv/rupicola/blob/d1daf657df0518f3590acb9b16faa331fb4cfeaa/src/Rupicola/Lib/Compiler.v#L1273

Last updated: Sep 23 2023 at 13:01 UTC