refactor(library/init): move subsingleton to init folder

library/data/empty.lean

@@ -5,8 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.empty
 Author: Jeremy Avigad, Floris van Doorn
 -/
-
-import logic.cast logic.subsingleton
+import logic.cast
 
 namespace empty
   protected theorem elim (A : Type) (H : empty) : A :=

library/data/unit.lean

@@ -5,8 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.unit
 Author: Leonardo de Moura
 -/
-
-import logic.eq logic.subsingleton
+import logic.eq
 
 namespace unit
   notation `⋆` := star

library/init/logic.lean

@@ -396,6 +396,40 @@ nonempty.rec H2 H1
 theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A :=
 nonempty.intro (default A)
 
+/- subsingleton -/
+
+inductive subsingleton [class] (A : Type) : Prop :=
+intro : (∀ a b : A, a = b) → subsingleton A
+
+protected definition subsingleton.elim {A : Type} [H : subsingleton A] : ∀(a b : A), a = b :=
+subsingleton.rec (fun p, p) H
+
+definition subsingleton_prop [instance] (p : Prop) : subsingleton p :=
+subsingleton.intro (λa b, !proof_irrel)
+
+definition subsingleton_decidable [instance] (p : Prop) : subsingleton (decidable p) :=
+subsingleton.intro (λ d₁,
+  match d₁ with
+  | inl t₁ := (λ d₂,
+    match d₂ with
+    | inl t₂ := eq.rec_on (proof_irrel t₁ t₂) rfl
+    | inr f₂ := absurd t₁ f₂
+    end)
+  | inr f₁ := (λ d₂,
+    match d₂ with
+    | inl t₂ := absurd t₂ f₁
+    | inr f₂ := eq.rec_on (proof_irrel f₁ f₂) rfl
+    end)
+  end)
+
+protected theorem rec_subsingleton {p : Prop} [H : decidable p]
+    {H1 : p → Type} {H2 : ¬p → Type}
+    [H3 : Π(h : p), subsingleton (H1 h)] [H4 : Π(h : ¬p), subsingleton (H2 h)]
+  : subsingleton (decidable.rec_on H H1 H2) :=
+decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
+
+/- if-then-else -/
+
 definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
 decidable.rec_on H (λ Hc, t) (λ Hnc, e)
 

library/logic/default.lean

@@ -5,6 +5,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: logic.default
 Author: Jeremy Avigad
 -/
-
-import logic.eq logic.connectives logic.cast logic.subsingleton
+import logic.eq logic.connectives logic.cast
 import logic.quantifiers logic.instances logic.identities

library/logic/subsingleton.lean

@@ -1,38 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: logic.subsingleton
-Author: Floris van Doorn
--/
-
-import logic.eq
-
-inductive subsingleton [class] (A : Type) : Prop :=
-intro : (∀ a b : A, a = b) → subsingleton A
-
-namespace subsingleton
-definition elim {A : Type} {H : subsingleton A} : ∀(a b : A), a = b := subsingleton.rec (fun p, p) H
-end subsingleton
-
-protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
-subsingleton.intro (λa b, !proof_irrel)
-
-theorem irrelevant [instance] (p : Prop) : subsingleton (decidable p) :=
-subsingleton.intro (fun d1 d2,
-  decidable.rec
-    (assume Hp1 : p, decidable.rec
-      (assume Hp2  : p,  congr_arg decidable.inl (eq.refl Hp1)) -- using proof irrelevance for Prop
-      (assume Hnp2 : ¬p, absurd Hp1 Hnp2)
-      d2)
-    (assume Hnp1 : ¬p, decidable.rec
-      (assume Hp2  : p,  absurd Hp2 Hnp1)
-      (assume Hnp2 : ¬p, congr_arg decidable.inr (eq.refl Hnp1)) -- using proof irrelevance for Prop
-      d2)
-   d1)
-
-protected theorem rec_subsingleton [instance] {p : Prop} [H : decidable p]
-    {H1 : p → Type} {H2 : ¬p → Type}
-    [H3 : Π(h : p), subsingleton (H1 h)] [H4 : Π(h : ¬p), subsingleton (H2 h)]
-  : subsingleton (decidable.rec_on H H1 H2) :=
-decidable.rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"