coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Catalin Hritcu <catalin.hritcu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?
- Date: Sat, 23 Aug 2014 09:03:10 +0200
On Sat, Aug 23, 2014 at 8:55 AM, ....
<nixiejun AT 163.com>
wrote:
> Dear everyone:
> I'mc confused with the following subgoal:
> Theorem T1(P:Prop->Prop): forall B:Prop,~P B->~(exists A:Prop,P A).
> Is it possible to prove?
No, because it's wrong. If you put the parentheses the right way, then yes:
Theorem T1_fixed (P:Prop->Prop): (forall B:Prop,~P B)->~(exists A:Prop,P A).
Proof. intros H [x Hc]. eapply H. eassumption. Qed.
Hope this helps,
Catalin
- [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?, ...., 08/23/2014
- Re: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?, Catalin Hritcu, 08/23/2014
Archive powered by MHonArc 2.6.18.