Zulip Chat Archive

Stream: maths

Topic: absurd


view this post on Zulip orlando (Apr 22 2020 at 19:29):

Hello
I don't very use often proof by contradiction, and it's my first in lean

i don't understand how to start i proof by contradiction, introducing x0 s.t not P x to use hyp on x0 ?

example (X :Type) (P : X  Prop ) (hyp : ( x : X, ¬ (P x))  false ) :  x, P x := begin
    sorry,
end

view this post on Zulip Alex J. Best (Apr 22 2020 at 19:39):

Using @Patrick Massot 's contrapose tactic

import tactic.push_neg
example (X :Type) (P : X  Prop ) (hyp : ( x : X, ¬ (P x))  false ) :  x, P x := begin
    contrapose! hyp,
    use hyp,
end

view this post on Zulip Bryan Gin-ge Chen (Apr 22 2020 at 19:40):

This particular result is already in the library as one direction of not_exists_not. Here are a few other ways to prove it:

import tactic

open_locale classical

#check @not_exists_not

example (X :Type) (P : X  Prop ) (hyp : ( x : X, ¬ (P x))  false ) :  x, P x := begin
  by_contra H,
  rw not_forall at H,
  exact hyp H,
end

example (X :Type) (P : X  Prop ) (hyp : ( x : X, ¬ (P x))  false ) :  x, P x := begin
  change ¬ _ at hyp,
  push_neg at hyp,
  assumption,
end

view this post on Zulip orlando (Apr 22 2020 at 19:43):

ohh thx @Patrick Massot and @Alex J. Best :big_smile:

view this post on Zulip orlando (Apr 22 2020 at 19:44):

and @Bryan Gin-ge Chen


Last updated: May 11 2021 at 16:22 UTC