absurd

Stream: maths

[orlando]

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

[Alex J. Best]

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

[Bryan Gin-ge Chen]

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

[orlando]

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

[orlando]

and @Bryan Gin-ge Chen