The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

       Hi Michel,

You are right. Notice however that solving intuitionistic tautoligies
is in general more complex than solving their classical counter-parts.

So for complex formulae, one could imagine that going back to
intuitionistic procedures may be cumbersome ; in that case, one might
want a specificaly classical procedure. But this would only apply
to particulary big formulae.

Cheers,


Benjamin



> Hi,
> 
> There is no need of a tactic dedicated to classical logic. As you can
> read in the book "Logic and Structure of Van Dalen" p174 , in
> propositionnal logic you have the Glivenko's theorem :
> 
> P is classically provable iff ~~P is intuitionistically provable.
> 
> So as you can guess with the Coq tutorial, you can prove any classically
> valid P with :
> 
> Require Classical.
> Goal P.
> Apply NNPP; Tauto.
> 
> I explain, NNPP is defined in the Classical Module as 
> NNPP : (p:Prop)~~p -> p
> When you apply NNPP to big P, you get the new goal ~~P, which is
> instuitionistically valid. So you can use Tauto to solve automatically
> your problem.
>