Zulip Chat Archive

Stream: new members

Topic: How do I prove ¬¬p → p


view this post on Zulip Lars Ericson (Nov 22 2020 at 02:16):

This is probably dead simple but I am really going in circles. This:

lemma not_iff_imp_false (P : Prop) : ¬ P  P  false := iff.rfl

theorem negneg (p : Prop) : ¬¬p  p :=
begin
  intro h,
  rw not_iff_imp_false (¬p) at h,
  rw not_iff_imp_false p at h,
  by_cases hp : p  false,
  exfalso,
  apply hp,
  exfalso,
  exact h hp,
  end

leaves me in goal state

p : Prop,
h : (p  false)  false,
hp : ¬(p  false)
 p

view this post on Zulip Donald Sebastian Leung (Nov 22 2020 at 02:37):

In negneg, introduce the ¬¬p hypothesis then use proof by_contradiction.

view this post on Zulip Lars Ericson (Nov 22 2020 at 02:43):

Thank you @Donald Sebastian Leung that's actually my first successful use of by_contra:

theorem negneg (p : Prop) : ¬¬p  p :=
begin
  intro h,
  by_contra h1,
  exact h h1,
end

Last updated: May 11 2021 at 22:14 UTC