From 5ef510f29066c585e30483f11180ccb17c5fd1f0 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 1 Feb 2015 11:16:30 -0500
Subject: [PATCH] feat(library/logic/axioms/prop_complete): add by_cases,
 by_contradiction

---
 library/logic/axioms/prop_complete.lean | 12 ++++++++++--
 library/logic/identities.lean           |  7 ++-----
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/library/logic/axioms/prop_complete.lean b/library/logic/axioms/prop_complete.lean
index 64df2602b..7c2b9d55e 100644
--- a/library/logic/axioms/prop_complete.lean
+++ b/library/logic/axioms/prop_complete.lean
@@ -5,9 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: logic.axioms.classical
 Author: Leonardo de Moura
 -/
-
 import logic.connectives logic.quantifiers logic.cast algebra.relation
-
 open eq.ops
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
@@ -28,6 +26,16 @@ or.elim (prop_complete a)
   (assume Ht : a = true,  or.inl (of_eq_true Ht))
   (assume Hf : a = false, or.inr (not_of_eq_false Hf))
 
+-- this supercedes by_cases in decidable
+definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
+or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
+
+-- this supercedes by_contradiction in decidable
+theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
+by_cases
+  (assume H1 : p, H1)
+  (assume H1 : ¬p, false.rec _ (H H1))
+
 theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
 cases (λ x, x = false ∨ x = true)
   (or.inr rfl)
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index cbf8afb63..b5c386d6d 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -8,9 +8,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Useful logical identities. Since we are not using propositional extensionality, some of the
 calculations use the type class support provided by logic.instances.
 -/
-
 import logic.connectives logic.instances logic.quantifiers logic.cast
-
 open relation decidable relation.iff_ops
 
 theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
@@ -19,7 +17,7 @@ calc
     ... ↔ a ∨ (c ∨ b)       : {or.comm}
      ... ↔ (a ∨ c) ∨ b      : iff.symm or.assoc
 
-theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
+theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
 calc
   a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc
     ... ↔ (b ∨ a) ∨ c       : {or.comm}
@@ -31,13 +29,12 @@ calc
     ... ↔ a ∧ (c ∧ b)       : {and.comm}
      ... ↔ (a ∧ c) ∧ b      : iff.symm and.assoc
 
-theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
+theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
 calc
   a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc
     ... ↔ (b ∧ a) ∧ c       : {and.comm}
      ... ↔ b ∧ (a ∧ c)      : and.assoc
 
-
 theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a :=
 iff.intro
   (assume H : ¬¬a,