From cb9830beaf6acdd93dd39409fec579fc05994d45 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Aug 2015 17:06:15 -0700
Subject: [PATCH] refactor(library/logic/choice): move prop_decidable instance
 into namespace 'classical'

---
 library/algebra/group_set_bigops.lean      | 2 +-
 library/data/hf.lean                       | 4 ++++
 library/data/real/complete.lean            | 3 +--
 library/data/real/division.lean            | 2 +-
 library/data/set/card.lean                 | 2 +-
 library/data/set/classical_inverse.lean    | 2 +-
 library/data/set/filter.lean               | 2 +-
 library/data/set/finite.lean               | 2 +-
 library/logic/choice.lean                  | 5 ++---
 library/logic/examples/leftinv_of_inj.lean | 2 +-
 tests/lean/704.lean                        | 2 +-
 11 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean
index 3a3dc4196b..5e233f4548 100644
--- a/library/algebra/group_set_bigops.lean
+++ b/library/algebra/group_set_bigops.lean
@@ -6,7 +6,7 @@ Author: Jeremy Avigad
 Set-based version of group_bigops.
 -/
 import .group_bigops data.set.finite
-open set
+open set classical
 
 namespace algebra
 namespace set
diff --git a/library/data/hf.lean b/library/data/hf.lean
index 14e1d6da75..33150001b7 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -65,6 +65,10 @@ definition not_mem (a : hf) (s : hf) : Prop := ¬ a ∈ s
 
 infix `∉` := not_mem
 
+open decidable
+protected definition decidable_mem [instance] : ∀ a s, decidable (a ∈ s) :=
+λ a s, finset.decidable_mem a (to_finset s)
+
 lemma not_mem_empty (a : hf) : a ∉ ∅ :=
 begin unfold [not_mem, mem, empty], rewrite to_finset_of_finset, apply finset.not_mem_empty end
 
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index e4b28d96d7..f9cb6e763a 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -17,8 +17,7 @@ open -[coercions] rat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 open -[coercions] nat
-open eq.ops
-open pnat
+open eq.ops pnat classical
 
 local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
 local notation 3 := subtype.tag (nat.of_num 3) dec_trivial
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index c65dd74259..34671cecdd 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -12,7 +12,7 @@ and excluded middle.
 import data.real.basic data.real.order data.rat data.nat logic.choice
 open -[coercions] rat
 open -[coercions] nat
-open eq.ops pnat
+open eq.ops pnat classical
 
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
diff --git a/library/data/set/card.lean b/library/data/set/card.lean
index 8afb5d98a1..01681f03ae 100644
--- a/library/data/set/card.lean
+++ b/library/data/set/card.lean
@@ -6,7 +6,7 @@ Author: Jeremy Avigad
 Cardinality of finite sets.
 -/
 import .finite data.finset.card
-open nat
+open nat classical
 
 namespace set
 
diff --git a/library/data/set/classical_inverse.lean b/library/data/set/classical_inverse.lean
index fa9fda7458..be1e387585 100644
--- a/library/data/set/classical_inverse.lean
+++ b/library/data/set/classical_inverse.lean
@@ -7,7 +7,7 @@ Using classical logic, defines an inverse function.
 -/
 import .function .map
 import logic.choice
-open eq.ops
+open eq.ops classical
 
 namespace set
 
diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean
index b2c98e560d..e23a9e9a9a 100644
--- a/library/data/set/filter.lean
+++ b/library/data/set/filter.lean
@@ -7,8 +7,8 @@ Filters, following Hölzl, Immler, and Huffman, "Type classes and filters for ma
 analysis in Isabelle/HOL".
 -/
 import data.set.function logic.identities logic.choice algebra.complete_lattice
-
 namespace set
+open classical
 
 structure filter (A : Type) :=
 (sets           : set (set A))
diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean
index 58cd7873a8..bc53dd1526 100644
--- a/library/data/set/finite.lean
+++ b/library/data/set/finite.lean
@@ -8,7 +8,7 @@ an element  s : set A  satsifies  finite s  doesn't mean that we can compute the
 a computational representation, use the finset type.
 -/
 import data.set.function data.finset.to_set logic.choice
-open nat
+open nat classical
 
 variable {A : Type}
 
diff --git a/library/logic/choice.lean b/library/logic/choice.lean
index 8af0dc6766..370edbfb37 100644
--- a/library/logic/choice.lean
+++ b/library/logic/choice.lean
@@ -161,9 +161,8 @@ propext (iff.intro
 end aux
 
 /- All propositions are decidable -/
-section all_decidable
+namespace classical
 open decidable sum
-
 noncomputable definition decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
 inhabited_of_nonempty
   (or.elim (em a)
@@ -178,4 +177,4 @@ match prop_decidable (nonempty A) with
 | inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
 | inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)
 end
-end all_decidable
+end classical
diff --git a/library/logic/examples/leftinv_of_inj.lean b/library/logic/examples/leftinv_of_inj.lean
index 3a1dd8d2c4..561c546f2f 100644
--- a/library/logic/examples/leftinv_of_inj.lean
+++ b/library/logic/examples/leftinv_of_inj.lean
@@ -10,7 +10,7 @@ The excluded middle is being used "behind the scenes" to allow us to write the i
 with (∃ a : A, f a = b).
 -/
 import logic.choice
-open function
+open function classical
 
 noncomputable definition mk_left_inv {A B : Type} [h : nonempty A] (f : A → B) : B → A :=
 λ b : B, if ex : (∃ a : A, f a = b) then some ex else inhabited.value (inhabited_of_nonempty h)
diff --git a/tests/lean/704.lean b/tests/lean/704.lean
index 36e74eef51..bd3562c918 100644
--- a/tests/lean/704.lean
+++ b/tests/lean/704.lean
@@ -1,4 +1,4 @@
-import classical
+import classical open classical
 eval if true then 1 else 0
 attribute prop_decidable [priority 0]
 eval if true then 1 else 0