refactor(library/logic): move logic/choice.lean to init/classical.lean

choice axiom is now in the classical namespace.

doc/lean/tutorial.org

@@ -125,13 +125,13 @@ Because we use _proposition as types_, we must support _empty types_. For exampl
 the type =false= must be empty, since we don't have a proof for =false=.
 
 Most systems based on the _propositions as types_ paradigm are based on constructive logic.
-In Lean, we support classical and constructive logic. We can load
+In Lean, we support classical and constructive logic. We can use
-_classical choice axiom_ by using =import logic.choice= or =import classical=. When the classical
+_classical choice axiom_ by using =open classical=. When the classical
 extensions are loaded, the _excluded middle_ is a theorem,
 and =em p= is a proof for =p ∨ ¬ p=.
 
 #+BEGIN_SRC lean
-  import logic.choice
+  open classical
   constant p : Prop
   check em p
 #+END_SRC

library/classical.lean

@@ -1,8 +0,0 @@
-/-
-Copyright (c) 2014 Jeremy Avigad. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jeremy Avigad
-
-The standard library together with the classical axioms.
--/
-import standard logic.choice

library/data/bag.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 Finite bags.
 -/
-import data.nat data.list.perm data.subtype algebra.binary
+import data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
 open [declarations] perm
 

library/data/default.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
 import .empty .unit .bool .num .string .nat .int .rat .fintype
-import .prod .sum .sigma .option .subtype .quotient .list .finset .set .stream
+import .prod .sum .sigma .option .quotient .list .finset .set .stream
 import .fin

library/data/encodable.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 Type class for encodable types.
 Note that every encodable type is countable.
 -/
-import data.fintype data.list data.list.sort data.sum data.nat.div data.subtype data.countable data.equiv data.finset
+import data.fintype data.list data.list.sort data.sum data.nat.div data.countable data.equiv data.finset
 open option list nat function
 
 structure encodable [class] (A : Type) :=

library/data/finset/basic.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura, Jeremy Avigad
 
 Finite sets.
 -/
-import data.fintype.basic data.nat data.list.perm data.subtype algebra.binary
+import data.fintype.basic data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
 open [declarations] perm
 

library/data/fixed_list.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 The length of a list is encoded into its type.
 It is implemented as a subtype.
 -/
-import logic data.list data.subtype data.fin
+import logic data.list data.fin
 open nat list subtype function
 
 definition fixed_list [reducible] (A : Type) (n : nat) := {l : list A | length l = n}

library/data/nat/bquant.lean

@@ -14,7 +14,7 @@ without assuming classical axioms.
 
 More importantly, they can be reduced inside of the Lean kernel.
 -/
-import data.subtype data.nat.order data.nat.div
+import data.nat.order data.nat.div
 
 namespace nat
   open subtype

library/data/nat/find.lean

@@ -10,7 +10,7 @@ This module provides the following two declarations:
 choose      {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat
 choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex)
 -/
-import data.subtype data.nat.basic data.nat.order
+import data.nat.basic data.nat.order
 open nat subtype decidable well_founded
 
 namespace nat

library/data/quotient/basic.lean

@@ -5,7 +5,7 @@ Author: Floris van Doorn
 
 An explicit treatment of quotients, without using Lean's built-in quotient types.
 -/
-import logic data.subtype logic.cast algebra.relation data.prod
+import logic logic.cast algebra.relation data.prod
 import logic.instances
 import .util
 

library/data/quotient/classical.lean

@@ -5,12 +5,11 @@ Author: Floris van Doorn
 
 A classical treatment of quotients, using Hilbert choice.
 -/
-import algebra.relation data.subtype logic.choice
+import algebra.relation
 import .basic
 
 namespace quotient
-
+open relation nonempty subtype classical
-open relation nonempty subtype
 
 /- abstract quotient -/
 

library/data/real/complete.lean

@@ -12,7 +12,6 @@ Here, we show that ℝ is complete.
 -/
 
 import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat
-import logic.choice
 open -[coercions] rat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1

library/data/real/division.lean

@@ -9,7 +9,7 @@ At this point, we no longer proceed constructively: this file makes heavy use of
 and excluded middle.
 -/
 
-import data.real.basic data.real.order data.rat data.nat logic.choice
+import data.real.basic data.real.order data.rat data.nat
 open -[coercions] rat
 open -[coercions] nat
 open eq.ops pnat classical

library/data/set/classical_inverse.lean

@@ -6,7 +6,6 @@ Author: Jeremy Avigad, Andrew Zipperer
 Using classical logic, defines an inverse function.
 -/
 import .function .map
-import logic.choice
 open eq.ops classical
 
 namespace set

library/data/set/filter.lean

@@ -6,7 +6,7 @@ Author: Jeremy Avigad
 Filters, following Hölzl, Immler, and Huffman, "Type classes and filters for mathematical
 analysis in Isabelle/HOL".
 -/
-import data.set.function logic.identities logic.choice algebra.complete_lattice
+import data.set.function logic.identities algebra.complete_lattice
 namespace set
 open classical
 

library/data/set/finite.lean

@@ -7,7 +7,7 @@ The notion of "finiteness" for sets. This approach is not computational: for exa
 an element  s : set A  satsifies  finite s  doesn't mean that we can compute the cardinality. For
 a computational representation, use the finset type.
 -/
-import data.set.function data.finset.to_set logic.choice
+import data.set.function data.finset.to_set
 open nat classical
 
 variable {A : Type}

library/init/classical.lean

@@ -3,10 +3,11 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
-import logic.quantifiers logic.eq
+prelude
-import data.subtype data.sum
+import init.subtype init.funext
 
-open subtype inhabited nonempty
+namespace classical
+open subtype
 
 /- the axiom -/
 
@@ -161,8 +162,7 @@ propext (iff.intro
 end aux
 
 /- All propositions are decidable -/
-namespace classical
+open decidable
-open decidable sum
 noncomputable definition decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
 inhabited_of_nonempty
   (or.elim (em a)
@@ -172,7 +172,7 @@ inhabited_of_nonempty
 noncomputable definition prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
 arbitrary (decidable a)
 
-noncomputable definition type_decidable (A : Type) : A + (A → false) :=
+noncomputable definition type_decidable (A : Type) : sum A (A → false) :=
 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)

library/init/default.lean

@@ -7,4 +7,4 @@ prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod init.priority
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
-import init.funext init.function
+import init.funext init.function init.subtype init.classical

library/init/logic.lean

@@ -21,6 +21,9 @@ prefix `¬` := not
 definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
 false.rec b (H2 H1)
 
+theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
+assume Ha : a, absurd (H1 Ha) H2
+
 /- not -/
 
 theorem not_false : ¬false :=
@@ -31,6 +34,12 @@ definition non_contradictory (a : Prop) : Prop := ¬¬a
 theorem non_contradictory_intro {a : Prop} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna
 
+/- false -/
+
+theorem false.elim {c : Prop} (H : false) : c :=
+false.rec c H
+
+
 /- eq -/
 
 notation a = b := eq a b
@@ -129,6 +138,20 @@ end ne
 
 theorem false.of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl
 
+section
+  open eq.ops
+  variables {p : Prop}
+
+  theorem ne_false_of_self : p → p ≠ false :=
+  assume (Hp : p) (Heq : p = false), Heq ▸ Hp
+
+  theorem ne_true_of_not : ¬p → p ≠ true :=
+  assume (Hnp : ¬p) (Heq : p = true), (Heq ▸ Hnp) trivial
+
+  theorem true_ne_false : ¬true = false :=
+  ne_false_of_self trivial
+end
+
 infixl `==`:50 := heq
 
 namespace heq
@@ -471,6 +494,9 @@ nonempty.rec H2 H1
 theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A :=
 nonempty.intro !default
 
+theorem nonempty_of_exists {A : Type} {P : A → Prop} : (∃x, P x) → nonempty A :=
+Exists.rec (λw H, nonempty.intro w)
+
 /- subsingleton -/
 
 inductive subsingleton [class] (A : Type) : Prop :=

library/init/subtype.lean

@@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Jeremy Avigad
 -/
+prelude
+import init.datatypes init.logic
 open decidable
 
 set_option structure.proj_mk_thm true

library/logic/connectives.lean

@@ -9,18 +9,10 @@ open eq.ops
 
 variables {a b c d : Prop}
 
-/- false -/
-
-theorem false.elim {c : Prop} (H : false) : c :=
-false.rec c H
-
 /- implies -/
 
 definition imp (a b : Prop) : Prop := a → b
 
-theorem mt (H1 : a → b) (H2 : ¬b) : ¬a :=
-assume Ha : a, absurd (H1 Ha) H2
-
 theorem imp.id (H : a) : a := H
 
 theorem imp.intro (H : a) (H₂ : b) : a := H

library/logic/eq.lean

@@ -102,16 +102,3 @@ section
   theorem eq_imp_trans (H₁ : a = b) (H₂ : b → c) : a → c :=
   assume Ha, H₂ (H₁ ▸ Ha)
 end
-
-section
-  variables {p : Prop}
-
-  theorem ne_false_of_self : p → p ≠ false :=
-  assume (Hp : p) (Heq : p = false), Heq ▸ Hp
-
-  theorem ne_true_of_not : ¬p → p ≠ true :=
-  assume (Hnp : ¬p) (Heq : p = true), (Heq ▸ Hnp) trivial
-end
-
-theorem true_ne_false : ¬true = false :=
-ne_false_of_self trivial

library/logic/examples/leftinv_of_inj.lean

@@ -9,7 +9,6 @@ The proof uses the classical axioms: choice and excluded middle.
 The excluded middle is being used "behind the scenes" to allow us to write the if-then-else expression
 with (∃ a : A, f a = b).
 -/
-import logic.choice
 open function classical
 
 noncomputable definition mk_left_inv {A B : Type} [h : nonempty A] (f : A → B) : B → A :=

library/logic/quantifiers.lean

@@ -52,9 +52,6 @@ iff.intro
   (or.rec (exists_imp_exists (λx, or.inl))
           (exists_imp_exists (λx, or.inr)))
 
-theorem nonempty_of_exists {A : Type} {P : A → Prop} : (∃x, P x) → nonempty A :=
-Exists.rec (λw H, intro w)
-
 section
   open decidable eq.ops
 

tests/lean/704.lean

@@ -1,4 +1,4 @@
-import classical open classical
+open classical
 eval if true then 1 else 0
 attribute prop_decidable [priority 0]
 eval if true then 1 else 0

tests/lean/empty.lean

@@ -1,5 +1,5 @@
-import logic logic.choice
+import logic
-open inhabited nonempty
+open inhabited nonempty classical
 
 noncomputable definition v1 : Prop := epsilon (λ x, true)
 inductive Empty : Type

tests/lean/extra/bag.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 Finite bags.
 -/
-import data.nat data.list.perm data.subtype algebra.binary
+import data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
 open [declarations] perm
 

tests/lean/interactive/class_bug.lean

@@ -1,5 +1,5 @@
-import logic.choice data.nat.basic
+import data.nat.basic
-open nonempty inhabited nat
+open nonempty inhabited nat classical
 
 theorem int_inhabited [instance] : inhabited nat := inhabited.mk zero
 

tests/lean/interactive/findp.input.expected.out

@@ -3,6 +3,7 @@
 -- BEGINFINDP STALE
 false|Prop
 false.rec|Π (C : Type), false → C
+false.elim|false → ?c
 false.of_ne|?a ≠ ?a → false
 false.rec_on|Π (C : Type), false → C
 false.cases_on|Π (C : Type), false → C
@@ -12,6 +13,8 @@ nat.lt_self_iff_false|∀ (n : nat), nat.lt n n ↔ false
 not_of_is_false|is_false ?c → ¬?c
 not_of_iff_false|(?a ↔ false) → ¬?a
 is_false|Π (c : Prop) [H : decidable c], Prop
+classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false
+classical.eq_false_or_eq_true|∀ (a : Prop), a = false ∨ a = true
 nat.lt_zero_iff_false|∀ (a : nat), nat.lt a nat.zero ↔ false
 not_of_eq_false|?p = false → ¬?p
 nat.succ_le_self_iff_false|∀ (n : nat), nat.le (nat.succ n) n ↔ false
@@ -19,6 +22,7 @@ decidable.rec_on_false|Π (H3 : ¬?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
 not_false|¬false
 decidable_false|decidable false
 of_not_is_false|¬is_false ?c → ?c
+classical.cases_true_false|∀ (P : Prop → Prop), P true → P false → (∀ (a : Prop), P a)
 iff_false_intro|¬?a → (?a ↔ false)
 ne_false_of_self|?p → ?p ≠ false
 nat.succ_le_zero_iff_false|∀ (n : nat), nat.le (nat.succ n) nat.zero ↔ false

tests/lean/interactive/t4.input.expected.out

@@ -5,7 +5,7 @@
 (ℕ → Prop) → ℕ
 -- ACK
 -- IDENTIFIER|6|6
-epsilon
+classical.epsilon
 -- ACK
 -- SYMBOL|6|14
 (

tests/lean/print_ax1.lean.expected.out

@@ -1,2 +1,3 @@
 quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b

tests/lean/print_ax2.lean

@@ -1,3 +1 @@
-import logic.choice
-
 print axioms

tests/lean/print_ax2.lean.expected.out

@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
-strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}

tests/lean/print_ax3.lean.expected.out

@@ -1,6 +1,7 @@
 no axioms
 ------
 quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
+classical.strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=

tests/lean/run/print_poly.lean

@@ -1,4 +1,4 @@
-import classical
+import data.nat
 open nat
 
 print pp.max_depth
@@ -9,7 +9,7 @@ print nat
 print nat.zero
 print nat.add
 print nat.rec
-print em
+print classical.em
 print quot.lift
 print nat.of_num
 print nat.add.assoc

tests/lean/run/sub.lean

@@ -1,4 +1,4 @@
-import data.subtype data.nat
+import data.nat
 open nat
 
 notation `{` binders:55 `|` r:(scoped P, subtype P) `}` := r

tests/lean/run/sub_bug.lean

@@ -1,3 +1,3 @@
-import data.subtype data.nat
+import data.nat
 open nat
 check { x : nat | x > 0}

tests/lean/subpp.lean

@@ -1,4 +1,4 @@
-import data.subtype
+-- import data.subtype
 open nat
 
 check {x : nat| x > 0 }