The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

It is not provable in Coq, whose core logic is an extension of intuitionistic logic (where this is not provable) rather than classic logic. Another way to think of this is that there is no program with type ((A -> False) -> False) -> A.

You can, however, prove intuitionistically that ~~~A -> ~A: you cannot collapse two levels of negation into zero, but you can collapse three into one. Coming up with a program of that type is an interesting exercize.

If you really need classical logic for your problem (it's actually surprising how much stuff you can do without it), you can add it on top of Coq's base logic as an axiom -- it has been proven that adding this axiom doesn't make the whole system inconcistent; it is not provable, but admissible. This is easy to do, just import the standard library module Logic.Classical_Prop.
  http://coq.inria.fr/stdlib/Coq.Logic.Classical_Prop.html

On Sat, Oct 26, 2013 at 11:54 AM, hao chen <chrihop AT gmail.com> wrote:

Hi,

I am learning coq, but encounter a problem. I cannot prove "forall A, ~~A <-> A". 'exfalso', 'destruct' and 'intros' are all used, and I have searched it in google, but still cannot find the solution. Could someone tell me that is it provable? and how to prove it?

Thanks,

ch