Stream: Coq users

Topic: eauto shelve vs Hint extern


view this post on Zulip Jonas Oberhauser (Nov 08 2021 at 15:30):

Require Import Utf8.

Ltac destruct_inh := match goal with H : inhabited _ |- _ => destruct H end.
Local Hint Extern 5 => destruct_inh : help.

Goal  T (Q: T  Prop),  inhabited T  (∀ x : T, Q x  False)  (∀ x, Q x)  False.
Proof. eauto with help. Unshelve. (** can't solve here anymore **) Fail destruct H. Abort.

Goal  T (Q: T  Prop),  inhabited T  (∀ x : T, Q x  False)  (∀ x, Q x)  False.
Proof. intros. destruct_inh. eauto with help. Unshelve. (** not ideal ...**) eauto. Qed.

I would like eauto with help to just solve the goal, instead it makes it unsolvable by forcing me to destruct the proof of inhabited T when trying to generate a proof of T : Type. What is the best way to teach eauto to do the right thing here?

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 15:48):

use priority 1 to get it to destruct earlier
I don't know about the unshelve issue

view this post on Zulip Paolo Giarrusso (Nov 08 2021 at 23:23):

Stupid Q: would typeclasses_eauto handle shelving better here?

view this post on Zulip Jonas Oberhauser (Nov 10 2021 at 18:50):

@Gaëtan Gilbert
Do you mean Hint Extern 1 ? I tried that in my original example and it didn't work, same with Extern 0. Or do you mean something else? EDIT: I just noticed that it does work in the sense that it does destruct earlier; before I just noticed that it still strangely puts T on the shelf, and didn't check with Unshelve that the goal is now actually solvable.

view this post on Zulip Jonas Oberhauser (Nov 10 2021 at 18:57):

@Paolo Giarrusso Do you mean that I should trytypeclasses eauto with help? Even with Hint Extern 1, the goal T ends up on the shelf when using typeclasses eauto with help

view this post on Zulip Paolo Giarrusso (Nov 10 2021 at 20:34):

Hm, that's indeed what I was wondering :-|


Last updated: Feb 08 2023 at 22:03 UTC