coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "plastyx" <plastyx AT free.fr>
To: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?
Date: Mon, 22 Dec 2014 21:57:33 +0100

That's false !

Because it doesn't mean

( forall B:Prop, ~P B ) ->~(exists A:Prop,P A).

but

forall B:Prop, ( ~P B ->~(exists A:Prop,P A) ).

Theorem T1' (P:Prop->Prop): ( forall B:Prop, ~P B ) ->~(exists A:Prop,P A).
Proof. intros. intros [ A PA ]. apply (H A). exact PA. Qed.

----- Original Message -----

From: ....

To: coq-club

Sent: Saturday, August 23, 2014 7:55 AM

Subject: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?

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?

Thank you ! Xiejun Ni.

Re: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?, plastyx, 12/22/2014