dne implies em

Stream: new members

[Luis O'Shea]

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 _

[Kenny Lau]

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

[Kenny Lau]

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

[Luis O'Shea]

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

I only used classical to prove dne

[Mario Carneiro]

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

[Kenny Lau]

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

[Luis O'Shea]

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

[Kenny Lau]

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

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

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

[Luis O'Shea]

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

[Mario Carneiro]

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