Jonas Oberhauser (Nov 08 2021 at 15:30): 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?
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
Paolo Giarrusso (Nov 08 2021 at 23:23):Stupid Q: would typeclasses_eauto handle shelving better here?
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.
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
Paolo Giarrusso (Nov 10 2021 at 20:34):Hm, that's indeed what I was wondering :-|
Last updated: Oct 13 2024 at 01:02 UTC