Zulip Chat Archive

Stream: new members

Topic: negated forall


view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:30):

I can't seem to figure out how to deal with the negated forall to prove the sorry in the following. I feel like I'm missing something obvious, but I don't know what.

theorem thm1 (α : Type) (P : α  Prop) : (¬  x : α, P x)  ( x : α, ¬ P x) :=
iff.intro
(
  show (¬  x : α, P x)  ( x : α, ¬ P x), from sorry
)
(
  show ( x : α, ¬ P x)  (¬  x : α, P x), from
  assume a1 :  x : α, ¬ P x,
  exists.elim a1 (
    assume x' : α,
    assume a2 : ¬ P x',
    assume a3 :  x : α, P x,
    have s1 : P x' := a3 x',
    show false, from a2 s1
  )
)

view this post on Zulip Kenny Lau (Sep 19 2020 at 18:31):

it's a classical theorem, that's why you can't prove it using just the usual operations

view this post on Zulip Kenny Lau (Sep 19 2020 at 18:31):

you need classical.em

view this post on Zulip Kenny Lau (Sep 19 2020 at 18:31):

as a "source of extra knowledge"

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:32):

Huh.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:32):

Ok. But the direction I did prove does not?

view this post on Zulip Kenny Lau (Sep 19 2020 at 18:33):

yep, as you demonstrated

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:34):

Interesting.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:36):

import tactic

theorem thm1 (α : Type) (P : α  Prop) : (¬  x : α, P x)  ( x : α, ¬ P x) :=
by simp

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:36):

And then you can use squeeze_simp to find out what the lemma it used is called

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:37):

and then you can #check that lemma and see what assumptions it uses

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:37):

and maybe you'd find some decidability nonsense, although after the recent refactor I am now less sure of this

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:39):

Indeed I just tried it and the clues that it is classical are now more well-hidden.

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:39):

#print axioms not_forall

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:44):

I would be interested in seeing what it looks like without tactics. I should be able to prove it from not P or P?

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:46):

You can prove it from forall P, P or not P, yes.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:47):

Ok. I'll give it a try. Thank you.

view this post on Zulip Johan Commelin (Sep 19 2020 at 18:47):

Patrick Thomas said:

I would be interested in seeing what it looks like without tactics.

You can see what the tactics did by writing #print my_lemma_name. I don't promise that it will look nice.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 18:48):

Yeah, I want it to look nice :)

view this post on Zulip Kevin Buzzard (Sep 19 2020 at 18:50):

In practice in tactic mode, by_contra is much more useful than EM. So I would first establish not not P implies P and then apply rhat function when things are getting sticky. It banks you a "not P" hypothesis which you can apply the next time you play this trick.

view this post on Zulip Johan Commelin (Sep 19 2020 at 18:50):

You might still glean some useful theorem names from the output

view this post on Zulip Patrick Thomas (Sep 24 2020 at 17:03):

I think I got it?

open classical


lemma not_not {P : Prop} : ¬ ¬ P  P :=
assume a1 :  ¬ ¬ P,
by_contradiction (
  assume a2 : ¬ P,
  show false, from a1 a2
)


example {α : Type} {P : α  Prop} : ( x : α, ¬ P x)  ¬ ( x : α, P x) :=
assume a1 :  x : α, ¬ P x,
exists.elim a1 (
  assume x' : α,
  assume a2 : ¬ P x',
  assume a3 :  x : α, P x,
  have s1 : P x' := a3 x',
  show false, from a2 s1
)


example {α : Type} {P : α  Prop} : ¬ ( x : α, ¬ P x)  ( x : α, P x) :=
assume a1 : ¬ ( x : α, ¬ P x),
assume x' : α,
by_contradiction (
  assume a2 : ¬ P x',
  have s1 :  x : α, ¬ P x := exists.intro x' a2,
  show false, from a1 s1
)


example {α : Type} {P : α  Prop} : ( x : α, P x)  ¬ ( x : α, ¬ P x) :=
assume a1 :  x : α, P x,
exists.elim a1 (
  assume x' : α,
  assume a2 : P x',
  assume a3 :  x : α, ¬ P x,
  have s1 : ¬ P x' := a3 x',
  show false, from s1 a2
)


example {α : Type} {P : α  Prop} : ¬ ( x : α, P x)  ( x : α, ¬ P x) :=
assume a1 : ¬ ( x : α, P x),
assume x' : α,
by_contradiction (
  assume a2 : ¬ ¬ P x',
  have s1 : P x' := not_not a2,
  have s2 :  x : α, P x := exists.intro x' s1,
  show false, from a1 s2
)

If I import tactic I seem to get an issue with by_contradiction also being a tactic. Is there a way around that?


Last updated: May 14 2021 at 12:18 UTC