De Morgan's Proof

Stream: general

[Stephanie Wang]

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
  )

[Kevin Buzzard]

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
  )

[Kevin Buzzard]

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...

[Kevin Buzzard]

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

[Stephanie Wang]

a comprehensible solution would be nice!

[Kevin Buzzard]

Then you want to use tactic mode!

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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
  )

[Stephanie Wang]

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