Skip to Content.
Sympa Menu

coq-club - Re: beginner's question 2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: beginner's question 2


chronological Thread 
  • From: David Delahaye <david.delahaye AT inria.fr>
  • To: rbauer AT rational.com (Bauer, Robert)
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: beginner's question 2
  • Date: Thu, 11 Oct 2001 01:53:34 +0200 (MET DST)

    Hi Robert,

> I seem unable to prove demorgan's law:
>  
> Variable a,b:Prop.
> Goal ~(a /\ b) -> (~a \/ ~b).
> Tauto.
>  
> Fails
>  
> So, I am thinking - must be an issue of constructive logic,
> so Quit. and try:

    Right, this way is only classical.

> Require Classical.
> Goal ~(a /\ b) -> (~a \/ ~b).
> Tauto.
>  
> Fails (again).
>  
> Now, I wonder why?

    Tauto is a proof search method only for intuitionistic propositional 
logic.
You don't change its behavior requiring the module "Classical". Currently,
there is no tactic dedicated to classical logic.

> Note, I only tried to use Tauto to figure how to get the proof past this
> point:
>  
> H: ~(a /\ b)
> ============
> ~a \/ ~b

    Here is a full detailed proof script (without automatic tactics) in order
to show you the way:

    Require Classical.
    Parameters a,b:Prop.
    Goal ~(a /\ b) -> (~a \/ ~b).
    Elim (classic a);Intros;
      [Right;Red;Red in H0;Intro;Apply H0;Split;Assumption
      |Left;Assumption].

    This lemma is already defined in the standard library (see not_and_or).

    BTW, you can notice that you can also use Tauto if you provide the right
instance of the excluded middle:

    Parameters a,b:Prop.
    Goal ~a \/ a -> ~(a /\ b) -> (~a \/ ~b).
    Tauto.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The LogiCal Project                              <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://logical.inria.fr/~delahaye/
===============================================================================

[Computers are like air conditioners - they stop working properly when you 
open
 Windows.]





Archive powered by MhonArc 2.6.16.

Top of Page