coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.]
- beginner's question 2, Bauer, Robert
- Re: beginner's question 2, David Delahaye
- Re: beginner's question 2,
Michel Levy
- Re: beginner's question 2, Benjamin Werner
- Re: beginner's question 2,
Michel Levy
- Re: beginner's question 2, David Delahaye
Archive powered by MhonArc 2.6.16.