Zulip Chat Archive

Stream: new members

Topic: How to write this in proof in tactic style


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Rob Lewis (Aug 15 2019 at 20:24):

He has the classical namespace open.

view this post on Zulip 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

view this post on Zulip Luis Berlioz (Aug 15 2019 at 20:28):

added the import. Thanks!

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 15 2019 at 20:28):

Another way to achieve the same goal.

view this post on Zulip Luis Berlioz (Aug 15 2019 at 20:39):

Nice! Thanks.


Last updated: May 12 2021 at 05:19 UTC