From 1d87016f033dfcce422325eee51a2e514726da2b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Apr 2015 07:46:11 -0700
Subject: [PATCH] refactor(library): move some theorems to init

---
 library/init/logic.lean       | 28 ++++++++++++++++++++++++++++
 library/logic/identities.lean | 10 ----------
 2 files changed, 28 insertions(+), 10 deletions(-)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index ea5ac417f..9945b03aa 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -23,6 +23,11 @@ false.rec b (H2 H1)
 theorem not_false : ¬false :=
 assume H : false, H
 
+definition non_contradictory (a : Prop) : Prop := ¬¬a
+
+theorem non_contradictory_intro {a : Prop} (Ha : a) : ¬¬a :=
+assume Hna : ¬a, absurd Ha Hna
+
 /- eq -/
 
 notation a = b := eq a b
@@ -171,6 +176,12 @@ namespace or
   or.rec H₂ H₃ H₁
 end or
 
+theorem non_contradictory_em (a : Prop) : ¬¬(a ∨ ¬a) :=
+assume not_em : ¬(a ∨ ¬a),
+  have neg_a : ¬a, from
+    assume pos_a : a, absurd (or.inl pos_a) not_em,
+  absurd (or.inr neg_a) not_em
+
 /- iff -/
 
 definition iff (a b : Prop) := (a → b) ∧ (b → a)
@@ -227,6 +238,23 @@ iff.mp (iff.symm H) trivial
 theorem not_of_iff_false (H : a ↔ false) : ¬a :=
 assume Ha : a, iff.mp H Ha
 
+theorem iff_true_intro (H : a) : a ↔ true :=
+iff.intro
+  (λ Hl, trivial)
+  (λ Hr, H)
+
+theorem iff_false_intro (H : ¬a) : a ↔ false :=
+iff.intro
+  (λ Hl, absurd Hl H)
+  (λ Hr, false.rec _ Hr)
+
+theorem not_non_contradictory_iff_absurd (a : Prop) : ¬¬¬a ↔ ¬a :=
+iff.intro
+  (assume Hl : ¬¬¬a,
+    assume Ha : a, absurd (non_contradictory_intro Ha) Hl)
+  (assume Hr : ¬a,
+    assume Hnna : ¬¬a, absurd Hr Hnna)
+
 calc_refl iff.refl
 calc_trans iff.trans
 
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 1862936a3..799fcb96c 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -110,16 +110,6 @@ theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidabl
   have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x),
   absurd H3 H)
 
-theorem iff_true_intro {a : Prop} (H : a) : a ↔ true :=
-iff.intro
-  (assume H1 : a,    trivial)
-  (assume H2 : true, H)
-
-theorem iff_false_intro {a : Prop} (H : ¬a) : a ↔ false :=
-iff.intro
-  (assume H1 : a,     absurd H1 H)
-  (assume H2 : false, false.elim H2)
-
 theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
 iff.intro
   (assume H, false.of_ne H)