Zulip Chat Archive

Stream: general

Topic: De Morgan's Proof


view this post on Zulip Stephanie Wang (Dec 13 2018 at 21:35):

I'm new to Lean, can someone help me out with this proof of this version of De Morgan's Law? I'm having trouble coming up with the forward proof

theorem demorgans_law : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  iff.intro(
  --
  )
  (
  assume h : ¬p ∧ ¬q,
  not_or h.left h.right
  )

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:39):

I'd start like this:

theorem demorgans_law (p q : Prop) : ¬(p  q)  ¬p  ¬q :=
  iff.intro(
    λ h,⟨_,_⟩
  )
  (
  assume h : ¬p  ¬q,
  not_or h.left h.right
  )

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:40):

and there is a red error on each of the _'s. I'd then try and figure out how to solve them. Actually, I'm a mathematician, so really I'd go straight into tactic mode...

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:41):

Ok so I can do it but it might look incomprehensible. Do you just want a solution or a hint?

view this post on Zulip Stephanie Wang (Dec 13 2018 at 21:43):

a comprehensible solution would be nice!

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:45):

Then you want to use tactic mode!

view this post on Zulip Chris Hughes (Dec 13 2018 at 21:47):

assume h, and intro (assume hp, h (or.inl hp)) (assume hq, h (or.inr hq))

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:47):

theorem demorgans_law' (p q : Prop) : ¬(p  q)  ¬p  ¬q :=
begin
  split,
  { intro hnpq,
    split,
    { intro hp,
      apply hnpq,
      left,
      assumption
    },
    { intro hq,
      apply hnpq,
      right,
      assumption
    }
  },
  sorry
end

half way there

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:49):

theorem demorgans_law' (p q : Prop) : ¬(p  q)  ¬p  ¬q :=
begin
  split,
  { intro hnpq,
    split,
    { intro hp,
      apply hnpq,
      left,
      assumption
    },
    { intro hq,
      apply hnpq,
      right,
      assumption
    }
  },
  intro hnpnq,
  intro hpq,
  cases hnpnq with hnp hnq,
  cases hpq,
    contradiction,
    contradiction
end

My impression is that computer scientists prefer these term mode things that you were writing, but I've been teaching mathematicians this stuff and tactic mode seems to be far easier for them.

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:49):

theorem demorgans_law (p q : Prop) : ¬(p  q)  ¬p  ¬q :=
⟨λ h, ⟨λ hp, h $ or.inl hp, λ hq, h $ or.inr hq,
  λ hnp, hnq hn, or.elim hn hnp hnq

Computer science proof, incomprehensibled to the max. Chris posted the perhaps happy medium you were looking for.

view this post on Zulip Kevin Buzzard (Dec 13 2018 at 21:51):

theorem demorgans_law'' (p q : Prop): ¬(p  q)  ¬p  ¬q :=
  iff.intro(
    assume h, and.intro (assume hp, h (or.inl hp)) (assume hq, h (or.inr hq))
  )
  (
  assume h : ¬p  ¬q,
  not_or h.left h.right
  )

view this post on Zulip Stephanie Wang (Dec 13 2018 at 21:53):

Ok this makes a lot of sense to me, thanks so much.


Last updated: May 14 2021 at 12:18 UTC