# Zulip Chat Archive

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

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

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

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

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