negations in propositional logic

Stream: new members

[Claus-Peter Becke]

I'm trying to prove de Morgan's laws. I don't know of how to deal with negations for example in the following situation:

example : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q :=

begin
  split,
  intro h, ...
end

After having imported the logic.basic library the work is done. But I would like to prove the goals using the tactics as proposed for example in the Natural Number Game.

[Mario Carneiro]

negation ¬ pis just notation for p -> false. So intro h can be used to prove one

[Chris Wong]

Note that one of the de Morgan identities (I forget which) is classical, so you'll need to use by_contra or by_cases at some point

[Anne Baanen]

This one should be provable without using by_contra or by_cases. For ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q, you will need them.

[Claus-Peter Becke]

@Anne Baanen, Chris Wong, Mario Carneiro,
thank you for hints. Using the following way to rewrite the theorem I proved one goal. Is it ok, to rewrite the theorem the following way?

``

[Claus-Peter Becke]

example : (p ∨ q) → false ↔ p → false ∧ q → false :=

[Eric Wieser]

You should find that the proof you wrote works for the way you originally wrote it too