From 6dbcf86fd4da1bd12a20f2bd5f427c16607961f6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jul 2015 09:53:31 -0700
Subject: [PATCH] feat(library/logic/axioms): use diaconescu to prove em

With the new "noncomputable" feature we can use Hilbert's choice without
being concerned it may accidentaly "leak" inside definitions we don't
want to use it.
---
 library/logic/axioms/em.lean                  | 54 +++++++++++++++--
 library/logic/axioms/examples/diaconescu.lean | 58 -------------------
 tests/lean/print_ax2.lean.expected.out        |  1 -
 3 files changed, 49 insertions(+), 64 deletions(-)
 delete mode 100644 library/logic/axioms/examples/diaconescu.lean

diff --git a/library/logic/axioms/em.lean b/library/logic/axioms/em.lean
index 7b644e359..e989b0736 100644
--- a/library/logic/axioms/em.lean
+++ b/library/logic/axioms/em.lean
@@ -3,9 +3,53 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 
-Excluded middle
-
-Remark: This axiom can be derived from propext funext and hilbert.
-See examples/diaconescu
+Prove excluded middle using: excluded middle follows from Hilbert's choice operator, function extensionality,
+and Prop extensionality
 -/
-axiom em (a : Prop) : a ∨ ¬a
+import logic.axioms.hilbert logic.eq
+open eq.ops
+
+section
+parameter  p : Prop
+
+private definition U (x : Prop) : Prop := x = true ∨ p
+private definition V (x : Prop) : Prop := x = false ∨ p
+
+private noncomputable definition u := epsilon U
+private noncomputable definition v := epsilon V
+
+private lemma u_def : U u :=
+epsilon_spec (exists.intro true (or.inl rfl))
+
+private lemma v_def : V v :=
+epsilon_spec (exists.intro false (or.inl rfl))
+
+private lemma not_uv_or_p : ¬(u = v) ∨ p :=
+or.elim u_def
+  (assume Hut : u = true,
+    or.elim v_def
+      (assume Hvf : v = false,
+        have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
+        or.inl Hne)
+      (assume Hp : p, or.inr Hp))
+  (assume Hp : p, or.inr Hp)
+
+private lemma p_implies_uv : p → u = v :=
+assume Hp : p,
+have Hpred : U = V, from
+  funext (take x : Prop,
+    have Hl : (x = true ∨ p) → (x = false ∨ p), from
+      assume A, or.inr Hp,
+    have Hr : (x = false ∨ p) → (x = true ∨ p), from
+      assume A, or.inr Hp,
+    show (x = true ∨ p) = (x = false ∨ p), from
+      propext (iff.intro Hl Hr)),
+have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
+show u = v, from H'
+
+theorem em : p ∨ ¬p :=
+have H : ¬(u = v) → ¬p, from mt p_implies_uv,
+  or.elim not_uv_or_p
+    (assume Hne : ¬(u = v), or.inr (H Hne))
+    (assume Hp : p, or.inl Hp)
+end
diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean
deleted file mode 100644
index 0fa6956e8..000000000
--- a/library/logic/axioms/examples/diaconescu.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-
-import logic.axioms.hilbert logic.eq
-open eq.ops
-
-/-
-Diaconescu’s theorem: excluded middle follows from Hilbert's choice operator, function extensionality,
-  and Prop extensionality
--/
-
-section
-parameter  p : Prop
-
-private definition U (x : Prop) : Prop := x = true ∨ p
-private definition V (x : Prop) : Prop := x = false ∨ p
-
-private noncomputable definition u := epsilon U
-private noncomputable definition v := epsilon V
-
-private lemma u_def : U u :=
-epsilon_spec (exists.intro true (or.inl rfl))
-
-private lemma v_def : V v :=
-epsilon_spec (exists.intro false (or.inl rfl))
-
-private lemma not_uv_or_p : ¬(u = v) ∨ p :=
-or.elim u_def
-  (assume Hut : u = true,
-    or.elim v_def
-      (assume Hvf : v = false,
-        have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
-        or.inl Hne)
-      (assume Hp : p, or.inr Hp))
-  (assume Hp : p, or.inr Hp)
-
-private lemma p_implies_uv : p → u = v :=
-assume Hp : p,
-have Hpred : U = V, from
-  funext (take x : Prop,
-    have Hl : (x = true ∨ p) → (x = false ∨ p), from
-      assume A, or.inr Hp,
-    have Hr : (x = false ∨ p) → (x = true ∨ p), from
-      assume A, or.inr Hp,
-    show (x = true ∨ p) = (x = false ∨ p), from
-      propext (iff.intro Hl Hr)),
-have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
-show u = v, from H'
-
-theorem em : p ∨ ¬p :=
-have H : ¬(u = v) → ¬p, from mt p_implies_uv,
-  or.elim not_uv_or_p
-    (assume Hne : ¬(u = v), or.inr (H Hne))
-    (assume Hp : p, or.inl Hp)
-end
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index da3bfe503..ca8b82d0b 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,4 +1,3 @@
 quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
-em : ∀ (a : Prop), a ∨ ¬a
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}