coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] eauto with destruct
- Date: Fri, 24 Jan 2014 15:13:44 +0100
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
- [Coq-Club] eauto with destruct, Bruno Woltzenlogel Paleo, 01/24/2014
- Re: [Coq-Club] eauto with destruct, Cedric Auger, 01/24/2014
- Re: [Coq-Club] eauto with destruct, Bruno Woltzenlogel Paleo, 01/24/2014
- Re: [Coq-Club] eauto with destruct, Cedric Auger, 01/24/2014
Archive powered by MHonArc 2.6.18.