negated forall

Stream: new members

[Patrick Thomas]

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]

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

[Kenny Lau]

you need classical.em

[Kenny Lau]

as a "source of extra knowledge"

[Patrick Thomas]

Huh.

[Patrick Thomas]

Ok. But the direction I did prove does not?

[Kenny Lau]

yep, as you demonstrated

[Patrick Thomas]

Interesting.

[Kevin Buzzard]

import tactic

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

#print axioms not_forall

[Patrick Thomas]

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]

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

[Patrick Thomas]

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

[Johan Commelin]

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]

Yeah, I want it to look nice :)

[Kevin Buzzard]

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]

You might still glean some useful theorem names from the output

[Patrick Thomas]

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?