Zulip Chat Archive

Stream: new members

Topic: de morgan


view this post on Zulip 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
)

view this post on Zulip 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:

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:26):

Nice :)

view this post on Zulip 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₁)⟩

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:30):

Would it be the same basic approach?

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:32):

I'm not really sure how to read it.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 03 2020 at 23:33):

I think that using by_contradiction leads to more linear arguments

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:35):

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

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:36):

Thank you.

view this post on Zulip Patrick Thomas (Oct 03 2020 at 23:55):

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
)

Last updated: May 09 2021 at 18:17 UTC