## Stream: new members

### Topic: de morgan

#### Patrick Thomas (Oct 03 2020 at 23:18):

Is there a more elegant way to prove this (without tactics)? It seems kind of brute force.

example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
assume a1 : ¬ (P ∧ Q),
have s1 : P ∨ ¬ P := classical.em P,
or.elim s1
(
assume a2 : P,
have s2 : Q ∨ ¬ Q := classical.em Q,
or.elim s2
(
assume a3 : Q,
have s3 : P ∧ Q := and.intro a2 a3,
false.elim (a1 s3)
)
(
assume a3 : ¬ Q,
or.intro_right (¬ P) a3
)
)
(
assume a2 : ¬ P,
or.intro_left (¬ Q) a2
)


#### Mario Carneiro (Oct 03 2020 at 23:26):

import logic.basic
example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) := not_and_distrib.1


:stuck_out_tongue_wink:

Nice :)

#### Mario Carneiro (Oct 03 2020 at 23:28):

Without logic.basic:

example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
λ h, classical.by_contradiction $λ h', h ⟨classical.by_contradiction$ λ h₁, h' (or.inl h₁),
classical.by_contradiction \$ λ h₁, h' (or.inr h₁)⟩


#### Mario Carneiro (Oct 03 2020 at 23:30):

To be fair, if I formatted this proof the same way as you I don't think it's much shorter

#### Patrick Thomas (Oct 03 2020 at 23:30):

Would it be the same basic approach?

#### Patrick Thomas (Oct 03 2020 at 23:32):

I'm not really sure how to read it.

#### Mario Carneiro (Oct 03 2020 at 23:32):

Here's your proof with golfy formatting

example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
λ a1, (classical.em P).elim
(λ a2, (classical.em Q).elim (λ a3, (a1 ⟨a2, a3⟩).elim) or.inr) or.inl


#### Mario Carneiro (Oct 03 2020 at 23:33):

I think that using by_contradiction leads to more linear arguments

#### Patrick Thomas (Oct 03 2020 at 23:35):

I'll see if I can figure out how to use it in my verbose version.

#### Mario Carneiro (Oct 03 2020 at 23:35):

Here's my proof with tactic formatting

import tactic

example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
begin
classical,
intro h,
by_contra h',
apply h, split,
{ by_contra h₁,
apply h',
exact or.inl h₁ },
{ by_contra h₁,
apply h',
exact or.inr h₁ },
end


Thank you.

#### Patrick Thomas (Oct 03 2020 at 23:55):

Cool. Thank you again.

example {P Q : Prop} : ¬ (P ∧ Q) → (¬ P ∨ ¬ Q) :=
assume a1 : ¬ (P ∧ Q),
assume a2 : ¬ (¬ P ∨ ¬ Q),
have s1 : P := (
assume a3 : ¬ P,
have s2 : ¬ P ∨ ¬ Q := or.intro_left (¬ Q) a3,
a2 s2
)
),
have s2 : Q := (
assume a3 : ¬ Q,
have s2 : ¬ P ∨ ¬ Q := or.intro_right (¬ P) a3,
a2 s2
)
),
have s3 : P ∧ Q := and.intro s1 s2,
a1 s3
)


Last updated: May 09 2021 at 18:17 UTC