The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

"try now firstorder." ?

There are "intuition" and "firstorder" tactics which might help.
These tactics can bring many changes to your goal(s) and hypotheses, so I advise to restore to the previous state in case of an error.
This leads to tactics of the form "intuition/firstorder; auto/eauto/easy/other_tactics; fail.".
"now _tactic_." does a similar stuff for you.
If you do not want to fail, but still rollback, you can put a "try" at the beginning of the tactic. (or you can also do: "_tactic_ || idtac.")
Don’t forget to put parenthesis around tactic sequences to group them, like: "try (firstorder; auto; fail)".

2014-01-24 Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>

Hi,

I have the following simple goal which is not solved by “eauto.” but is solved by "destruct H1 as [w1 [R1 H1]]. eauto.”  . Is there any other “auto-like” tactic that would try “destruct” automatically for me?

w : i

p : o

q : o

H1 : exists w1 : i, r w w1 /\ p w1

H2 : forall w1 : i, r w w1 -> p w1 -> q w1

______________________________________(1/1)

exists w1 : i, r w w1 /\ q w1

Best regards,

Bruno

--
.../Sedrikov\...