The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

I believe Edsko misunderstood Matej's question.  The problem is not to 
prove.

forall (E p : Prop) (E -> p) -> (E -> ~p -> False)

Rather the problem is to prove :

forall (E p : Prop) (E -> ~p -> False) -> E -> p

The question was " how do you get from a goal of the following shape:

....
==========
p

To a goal of the following shape:
...
H' : ~p
=======
False

?"

If my interpretation of the question is right, then here is an answer:

By default, the Coq system lets you reason in a logical system that does 
not allow this step.  There is a well-known distinction between two 
variants of logic, where one, called "intuitionistic logic" does not 
allow this kind of reasoning.  There are advantages to restricting logic 
in this manner, and it appears that a lot of mathematics or computer 
science can still be done and reasoned about in this kind of restricted 
logic. If you work in this restricted logic, then there is no way to do 
what you want.

Now, if you don't want the restriction, you should load a logic 
complement, called "classical logic".

Require Import Classical.

Now, the step you want to perform can be done using the theorem NNPP, as 
in :

apply NNPP; intros <some hypothesis name>.

I hope this helps,

Yves

Edsko de Vries wrote:
> Hi,
>
> > In Coq, it is possible to make the following reasoning steps:
> >
> >        E |- ~p
> >     E, p |- False
> >
> > with the `intro' tactics. Both that lines above are meant to be
> > "sequents" where |- separates the antecedent and the succedent.
> >
> > With what tactics can I perform the following reasoning step:
> >
> >         E |- p
> >     E, ~p |- False
>
> Remember that ~ is a function (~p is syntactic sugar for p -> False). 
> Hence, you can do this reasoning step as follows:
>
> Variable E p : Prop.
>
> Lemma foo : (E -> p) -> (E /\ ~p -> False).
> Proof.
>   intros H1 H2.
>   destruct H2 as (e, not_p).
>   apply not_p.
>   apply H1.
>   apply e.
> Qed.
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club