The Coq mailing list

[Ezra Cooper <e.e.k.cooper AT sms.ed.ac.uk>]

Matej Kosik wrote:
> 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
>
> ?
>
> (I am new to Coq.)

If I understand you right, the goal of your rule is on top and the 
supporting reason is on the bottom.

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.

HTH,
Ezra


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.