de morgan

Stream: new members

[Patrick Thomas]

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]

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

:stuck_out_tongue_wink:

[Patrick Thomas]

Nice :)

[Mario Carneiro]

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]

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

[Patrick Thomas]

Would it be the same basic approach?

[Patrick Thomas]

I'm not really sure how to read it.

[Mario Carneiro]

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]

I think that using by_contradiction leads to more linear arguments

[Patrick Thomas]

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

[Mario Carneiro]

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

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Cool. Thank you again.

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