From 1011a8022c5fe82cfd7446cf77123ca8ac139dfd Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Wed, 27 Aug 2014 20:46:07 -0400
Subject: [PATCH] refactor(library/logic/connectives): make dependence prop <-
 eq <- basic

---
 library/logic/classes/nonempty.lean  |  2 +-
 library/logic/connectives/basic.lean | 61 +++-------------------------
 library/logic/connectives/eq.lean    |  5 +--
 library/logic/connectives/prop.lean  | 59 ++++++++++++++++++++++++++-
 4 files changed, 65 insertions(+), 62 deletions(-)

diff --git a/library/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean
index 9fb8ffe37a..b11fdc021d 100644
--- a/library/logic/classes/nonempty.lean
+++ b/library/logic/classes/nonempty.lean
@@ -11,7 +11,7 @@ namespace nonempty
 inductive nonempty (A : Type) : Prop :=
 nonempty_intro : A → nonempty A
 
-definition nonempty_elim {A : Type} {B : Type} (H1 : nonempty A) (H2 : A → B) : B :=
+definition nonempty_elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
 nonempty_rec H2 H1
 
 theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
diff --git a/library/logic/connectives/basic.lean b/library/logic/connectives/basic.lean
index 237d9aaea8..08db34fb70 100644
--- a/library/logic/connectives/basic.lean
+++ b/library/logic/connectives/basic.lean
@@ -2,61 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import general_notation .prop
-
--- implication
--- -----------
-
-abbreviation imp (a b : Prop) : Prop := a → b
-
-
--- true and false
--- --------------
-
-inductive false : Prop
-
-theorem false_elim (c : Prop) (H : false) : c :=
-false_rec c H
-
-inductive true : Prop :=
-trivial : true
-
-abbreviation not (a : Prop) := a → false
-prefix `¬` := not
-
-
--- not
--- ---
-
-theorem not_intro {a : Prop} (H : a → false) : ¬a := H
-
-theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
-
-theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1
-
-theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
-assume Hna : ¬a, absurd Ha Hna
-
-theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
-assume Ha : a, absurd (H1 Ha) H2
-
-theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
-false_elim b (absurd H1 H2)
-
-theorem absurd_not_true (H : ¬true) : false :=
-absurd trivial H
-
-theorem not_false_trivial : ¬false :=
-assume H : false, H
-
-theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
-assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
-
-theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
-assume Hb : b, absurd (assume Ha : a, Hb) H
-
-theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
-assume Hnb Ha, Hnb (Hab Ha)
+import general_notation .eq
 
 
 -- and
@@ -154,6 +100,8 @@ definition iff (a b : Prop) := (a → b) ∧ (b → a)
 infix `<->` := iff
 infix `↔` := iff
 
+theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl
+
 theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
 
 theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
@@ -190,6 +138,9 @@ iff_intro
 calc_refl iff_refl
 calc_trans iff_trans
 
+theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
+iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
+
 
 -- comm and assoc for and / or
 -- ---------------------------
diff --git a/library/logic/connectives/eq.lean b/library/logic/connectives/eq.lean
index 073f06e374..ca23f521d9 100644
--- a/library/logic/connectives/eq.lean
+++ b/library/logic/connectives/eq.lean
@@ -7,7 +7,7 @@
 
 -- Equality.
 
-import .basic
+import .prop
 
 -- eq
 -- --
@@ -100,9 +100,6 @@ assume Ha, H2 ▸ (H1 Ha)
 theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
 assume Ha, H2 (H1 ▸ Ha)
 
-theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
-iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
-
 
 -- ne
 -- --
diff --git a/library/logic/connectives/prop.lean b/library/logic/connectives/prop.lean
index 68bb68734e..d0e53ce5aa 100644
--- a/library/logic/connectives/prop.lean
+++ b/library/logic/connectives/prop.lean
@@ -1,7 +1,62 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
-----------------------------------------------------------------------------------------------------
+
+import general_notation
 
 definition Prop [inline] := Type.{0}
+
+
+-- implication
+-- -----------
+
+abbreviation imp (a b : Prop) : Prop := a → b
+
+
+-- true and false
+-- --------------
+
+inductive false : Prop
+
+theorem false_elim (c : Prop) (H : false) : c :=
+false_rec c H
+
+inductive true : Prop :=
+trivial : true
+
+abbreviation not (a : Prop) := a → false
+prefix `¬` := not
+
+
+-- not
+-- ---
+
+theorem not_intro {a : Prop} (H : a → false) : ¬a := H
+
+theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
+
+theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1
+
+theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
+assume Hna : ¬a, absurd Ha Hna
+
+theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
+assume Ha : a, absurd (H1 Ha) H2
+
+theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
+false_elim b (absurd H1 H2)
+
+theorem absurd_not_true (H : ¬true) : false :=
+absurd trivial H
+
+theorem not_false_trivial : ¬false :=
+assume H : false, H
+
+theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
+assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
+
+theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
+assume Hb : b, absurd (assume Ha : a, Hb) H
+
+theorem contrapos {a b : Prop} (Hab : a → b) : (¬b → ¬a) :=
+assume Hnb Ha, Hnb (Hab Ha)