## Stream: new members

### Topic: How to write this in proof in tactic style

#### Luis Berlioz (Aug 15 2019 at 20:10):

Hi, I am trying to write the following proof completely in tactic mode. I don't know how to use tactics with the second by_contradiction statement. Even though the proof works as it written now, currently I am learning about tactic mode so I want to know how to do it even if it is not practical. Thanks.

open classical
example : (¬∀ x, p x) → (∃ x, ¬p x) :=
begin
intros hnA,
apply by_contradiction,
intro hnE,
have : ∀ (x : α), p x, from
assume s: α,
by_contradiction
(assume hs: ¬p s,
show false, from hnE ⟨ s, hs ⟩),
show false, from absurd this hnA,
end


#### Yury G. Kudryashov (Aug 15 2019 at 20:23):

Copy+pasted your example, defined {α : Type*} {p : α → Prop}. It doesn't work. Do you have any imports?

#### Rob Lewis (Aug 15 2019 at 20:24):

He has the classical namespace open.

#### Rob Lewis (Aug 15 2019 at 20:24):

One way to do it is this, which uses the by_contradiction tactic:

example : (¬∀ x, p x) → (∃ x, ¬p x) :=
begin
intro hnA,
by_contradiction hne,
have : ∀ (x : α), p x,
{ intro s,
by_contradiction hs,
show false, from hne ⟨s, hs⟩ },
show false, from absurd this hnA,
end


#### Luis Berlioz (Aug 15 2019 at 20:28):

added the import. Thanks!

#### Yury G. Kudryashov (Aug 15 2019 at 20:28):

section
local attribute [instance] classical.prop_decidable

example {α : Type} {p : α → Prop} : (¬∀ x, p x) → (∃ x, ¬p x) :=
begin
intros hnA,
by_contradiction hne,
apply hnA,
intro x,
by_contradiction hx,
apply hne,
exact ⟨x, hx⟩
end
end


#### Yury G. Kudryashov (Aug 15 2019 at 20:28):

Another way to achieve the same goal.

#### Luis Berlioz (Aug 15 2019 at 20:39):

Nice! Thanks.

Last updated: May 12 2021 at 05:19 UTC