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?
use priority 1 to get it to destruct earlier
I don't know about the unshelve issue
Stupid Q: would typeclasses_eauto handle shelving better here?
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.
@Paolo Giarrusso Do you mean that I should try
typeclasses eauto with help? Even with Hint Extern 1, the goal T ends up on the shelf when using
typeclasses eauto with help
Hm, that's indeed what I was wondering :-|
Last updated: Feb 08 2023 at 22:03 UTC