The Coq mailing list

["Bauer, Robert" <rbauer AT rational.com>]

Hi,

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:

Require Classical.
Goal ~(a /\ b) -> (~a \/ ~b).
Tauto.

Fails (again).

Now, I wonder why?

Note, I only tried to use Tauto to figure how to get the proof past this
point:

H: ~(a /\ b)
============
~a \/ ~b

which I thought could be done with a rewrite on the assumption, but
well, I couldn't figure out how to do that - so I thought use Tauto
and study the output (though intuitively I know that in general you
can't simply reverse a forward proof).

Any help would be appreciated.

Thanks