Skip to Content.
Sympa Menu

coq-club - [Coq-Club] eauto with destruct

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] eauto with destruct


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page