The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

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).

I have chosen unfortunate notation. I thought, it is obvious. E was
meant as a "environment" (set of hypotheses) from which we want to prove
succedent. E is not a proposition.


Yves Bertot wrote:
> 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,

Thank you. The step I describe would actually help me to prove NNPP
which was the original problem I have tried to solve.

Ezra Cooper wrote:
> If I understand you right, the goal of your rule is on top and the
> supporting reason is on the bottom.

indeed

>
> In that case, the latter step is a classical, rather than
> intuitionistic, inference, and so is not supported by default in Coq.
> You can get this sort of reasoning by importing the Classical module.
> This assumes the classical law of excluded middle, P \/ ~P, and derives
> other classical lemmas, which you can find in the standard library (for
> example, in Classical_Prop).
>
> However, it may well be better to redesign your assumptions so that you
> don't have to go via ~~P. It is rarely simpler, let alone clearer, to
> find contradiction in a hypothesis ~P than to prove P directly.

There was no other reason to prove it just as an excercie I decided to do.

Jean-Marc Notin wrote:
> This is not possible in "pure' Coq. You need to switch to classical
> logic and admit the excluded middle axiom:
>
> Require Import Classical_Prop.
>
> Goal forall P : Prop, P.
>   intro P.
>   apply NNPP.

Yes. This is (also) the answer to my question. However, I was in fact
exactly trying to prove NNPP in Coq :-)

Thank you all for your quick answers.