## Stream: new members

### Topic: negated forall

#### 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
)
)


#### 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

#### Kenny Lau (Sep 19 2020 at 18:31):

you need classical.em

#### Kenny Lau (Sep 19 2020 at 18:31):

as a "source of extra knowledge"

Huh.

#### Patrick Thomas (Sep 19 2020 at 18:32):

Ok. But the direction I did prove does not?

#### Kenny Lau (Sep 19 2020 at 18:33):

yep, as you demonstrated

Interesting.

#### Kevin Buzzard (Sep 19 2020 at 18:36):

import tactic

theorem thm1 (α : Type) (P : α → Prop) : (¬ ∀ x : α, P x) ↔ (∃ x : α, ¬ P x) :=
by simp


#### 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

#### Kevin Buzzard (Sep 19 2020 at 18:37):

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

#### 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

#### 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.

#### Kevin Buzzard (Sep 19 2020 at 18:39):

#print axioms not_forall


#### 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?

#### Kevin Buzzard (Sep 19 2020 at 18:46):

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

#### Patrick Thomas (Sep 19 2020 at 18:47):

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

#### 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.

#### Patrick Thomas (Sep 19 2020 at 18:48):

Yeah, I want it to look nice :)

#### 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.

#### Johan Commelin (Sep 19 2020 at 18:50):

You might still glean some useful theorem names from the output

#### 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,
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' : α,
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' : α,

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