Zulip Chat Archive

Stream: new members

Topic: dne implies em


view this post on Zulip Luis O'Shea (Oct 20 2019 at 23:20):

TPiL 3.5 suggests proving em (excluded middle) using dne (double-negation elimination). I found this trickier than expected (as a Lean noob) and was wondering what tricks I'm missing. Below is my attempt. Some concrete questions include: Did I really need to define demorgan_nor? Do I need to use the inference symbol (_) so much? Is my attempt too long?

variables p q : Prop

lemma demorgan_nor (h : ¬(p  q)) : ¬p  ¬q :=
 assume : p, h $ or.inl this, assume : q, h $ or.inr this 

section
open classical

theorem dne (h : ¬¬p) : p :=
or.elim (em p)
  (assume : p, this)
  (assume : ¬p, absurd this h)

end

lemma nnem : ¬¬(p  ¬p) :=
assume h : ¬(p  ¬p),
have hpnp : ¬p  ¬¬p, from demorgan_nor _ _ h,
have hnpp : ¬p  p, from and.intro hpnp.left (dne _ hpnp.right),
hnpp.left hnpp.right

theorem em_alt : p  ¬p := dne _ $ nnem _

view this post on Zulip Kenny Lau (Oct 20 2019 at 23:34):

you shouldn't use classical because that is the point, I think.

view this post on Zulip Kenny Lau (Oct 20 2019 at 23:35):

you don't need _ if you make the variables implicit

view this post on Zulip Luis O'Shea (Oct 20 2019 at 23:35):

you shouldn't use classical because that is the point, I think.

I only used classical to prove dne

view this post on Zulip Mario Carneiro (Oct 20 2019 at 23:36):

you should be able to prove nnem without dne or any classical stuff

view this post on Zulip Kenny Lau (Oct 20 2019 at 23:38):

Spoilers:
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

axiom dne {p : Prop} : ¬¬p  p

theorem em {p : Prop} : p  ¬p :=
dne $ assume h : ¬(p  ¬p),
have hnp : ¬p, from assume hp : p, h $ or.inl hp,
h $ or.inr hnp

view this post on Zulip Luis O'Shea (Oct 20 2019 at 23:39):

you should be able to prove nnem without dne or any classical stuff

Duh! Yes:

lemma nnem : ¬¬(p  ¬p) :=
assume h : ¬(p  ¬p),
have hpnp : ¬p  ¬¬p, from demorgan_nor _ _ h,
hpnp.right hpnp.left

view this post on Zulip Kenny Lau (Oct 20 2019 at 23:39):

Golfed version:
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

axiom dne {p : Prop} : ¬¬p  p

theorem em {p : Prop} : p  ¬p :=
dne $ λ h, h $ or.inr $ λ hp, h $ or.inl hp

view this post on Zulip Luis O'Shea (Oct 20 2019 at 23:46):

Thanks! So regarding avoiding _s, is it generally preferable to write variable {p : Prop} rather than variable p : Prop? (Or if not when is one preferred over the other?)

view this post on Zulip Mario Carneiro (Oct 20 2019 at 23:49):

The braces mean "let lean figure it out", i.e. always put a _ in that slot. The convention is to make the variable implicit if it can be deduced from the type of later assumptions (not counting the conclusion). So that means dne should have p implicit but em should have it explicit


Last updated: May 17 2021 at 22:15 UTC