refactor(library/standard): begin reorganization into hierarchy

library/standard/data/bool.lean

@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic decidable
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
 using eq_proofs decidable
 
 namespace bool
@@ -137,4 +139,5 @@ induction_on a (refl (!!ff)) (refl (!!tt))
 theorem bnot_false : !ff = tt := refl _
 
 theorem bnot_true  : !tt = ff := refl _
+
 end

library/standard/data/list/basic.lean

@@ -9,10 +9,10 @@
 --
 -- Basic properties of lists.
 
-import tactic
-import nat
-import congr
-import if -- for find
+import tools.tactic
+import data.nat
+import logic
+-- import if -- for find
 
 using nat
 using congr
@@ -21,16 +21,6 @@ using eq_proofs
 namespace list
 
 
--- TODO: move this
-theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
-calc
-  (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
-    ... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c)
-    ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
-
--- TODO: add or_left_comm, and_right_comm, and_left_comm
-
-
 -- Type
 -- ----
 

library/standard/data/nat/nat1.lean

@@ -3,7 +3,8 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
-import logic num tactic decidable binary
+
+import logic data.num tools.tactic struc.binary
 using tactic num binary eq_proofs
 using decidable (hiding induction_on rec_on)
 

library/standard/data/num.lean

@@ -1,8 +1,13 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.inhabited
+
 namespace num
+
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
@@ -20,4 +25,5 @@ inhabited_intro one
 
 theorem inhabited_num [instance] : inhabited num :=
 inhabited_intro zero
+
 end

library/standard/data/string.lean

@@ -1,7 +1,9 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import bool
+----------------------------------------------------------------------------------------------------
+
+import data.bool
 using bool
 
 namespace string
@@ -17,4 +19,5 @@ inhabited_intro (ascii ff ff ff ff ff ff ff ff)
 
 theorem inhabited_string [instance] : inhabited string :=
 inhabited_intro empty
+
 end

library/standard/logic/classes/congr.lean

@@ -4,11 +4,8 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import logic
-import function
-
+import logic.connectives.basic logic.connectives.function
 using function
-
 namespace congr
 
 -- TODO: move this somewhere else

library/standard/logic/classes/decidable.lean

@@ -1,9 +1,13 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.basic logic.connectives.eq
 
 namespace decidable
+
 inductive decidable (p : Prop) : Type :=
 | inl : p  → decidable p
 | inr : ¬p → decidable p

library/standard/logic/classes/inhabited.lean

@@ -0,0 +1,22 @@
+----------------------------------------------------------------------------------------------------
+-- 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 logic.connectives.quantifiers
+
+inductive inhabited (A : Type) : Prop :=
+| inhabited_intro : A → inhabited A
+
+theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B :=
+inhabited_rec H2 H1
+
+theorem inhabited_Prop [instance] : inhabited Prop :=
+inhabited_intro true
+
+theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
+inhabited_elim H (take b, inhabited_intro (λa, b))
+
+theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
+obtain w Hw, from H, inhabited_intro w

library/standard/logic/connectives/basic.lean

@@ -1,8 +1,13 @@
+----------------------------------------------------------------------------------------------------
 -- 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
+----------------------------------------------------------------------------------------------------
 
-definition Prop [inline] := Type.{0}
+import logic.connectives.prop
+
+-- implication
+-- -----------
 
 abbreviation imp (a b : Prop) : Prop := a → b
 
@@ -142,103 +147,6 @@ or_elim H1
   (assume H2 : a, or_inr (H H2))
 
 
--- eq
--- --
-
-inductive eq {A : Type} (a : A) : A → Prop :=
-| refl : eq a a
-
-infix `=`:50 := eq
-
-theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
-eq_rec H2 H1
-
-theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
-subst H2 H1
-
-calc_subst subst
-calc_refl  refl
-calc_trans trans
-
-theorem true_ne_false : ¬true = false :=
-assume H : true = false,
-  subst H trivial
-
-theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
-subst H (refl a)
-
-namespace eq_proofs
-  postfix `⁻¹`:100 := symm
-  infixr `⬝`:75     := trans
-  infixr `▸`:75    := subst
-end
-using eq_proofs
-
-theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
-H ▸ refl (f a)
-
-theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
-H ▸ refl (f a)
-
-theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b :=
-H1 ▸ H2 ▸ refl (f a)
-
-theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
-take x, congr1 H x
-
-theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) :=
-congr2 not H
-
-theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
-H1 ▸ H2
-
-infixl `<|`:100 := eqmp
-infixl `◂`:100 := eqmp
-
-theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
-H1⁻¹ ◂ H2
-
-theorem eqt_elim {a : Prop} (H : a = true) : a :=
-H⁻¹ ◂ trivial
-
-theorem eqf_elim {a : Prop} (H : a = false) : ¬a :=
-assume Ha : a, H ◂ Ha
-
-theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
-assume Ha, H2 (H1 Ha)
-
-theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
-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)
-
-
--- ne
--- --
-
-definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
-infix `≠`:50 := ne
-
-theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H
-
-theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := H1 H2
-
-theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
-
-theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
-
-theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
-assume H1 : b = a, H (H1⁻¹)
-
-theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := H1⁻¹ ▸ H2
-
-theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := H2 ▸ H1
-
-calc_trans eq_ne_trans
-calc_trans ne_eq_trans
-
-
 -- iff
 -- ---
 
@@ -276,9 +184,6 @@ iff_intro
 
 calc_trans iff_trans
 
-theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
-iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
-
 
 -- comm and assoc for and / or
 -- ---------------------------
@@ -310,58 +215,3 @@ iff_intro
     (assume H1, or_elim H1
       (assume Hb, or_inl (or_inr Hb))
       (assume Hc, or_inr Hc)))
-
-
--- exists
--- ------
-
-inductive Exists {A : Type} (P : A → Prop) : Prop :=
-| exists_intro : ∀ (a : A), P a → Exists P
-
-notation `exists` binders `,` r:(scoped P, Exists P) := r
-notation `∃` binders `,` r:(scoped P, Exists P) := r
-
-theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
-Exists_rec H2 H1
-
-theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
-assume H1 : ∀x, ¬p x,
-  obtain (w : A) (Hw : p w), from H,
-  absurd Hw (H1 w)
-
-theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
-assume H1 : ∃x, ¬p x,
-  obtain (w : A) (Hw : ¬p w), from H1,
-  absurd (H2 w) Hw
-
-definition exists_unique {A : Type} (p : A → Prop) :=
-∃x, p x ∧ ∀y, y ≠ x → ¬p y
-
-notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
-
-theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬p y) : ∃!x, p x :=
-exists_intro w (and_intro H1 H2)
-
-theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
-                           (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬p y) → b) : b :=
-obtain w Hw, from H2,
-H1 w (and_elim_left Hw) (and_elim_right Hw)
-
-
--- inhabited
--- ---------
-
-inductive inhabited (A : Type) : Prop :=
-| inhabited_intro : A → inhabited A
-
-theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B :=
-inhabited_rec H2 H1
-
-theorem inhabited_Prop [instance] : inhabited Prop :=
-inhabited_intro true
-
-theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
-inhabited_elim H (take b, inhabited_intro (λa, b))
-
-theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
-obtain w Hw, from H, inhabited_intro w

library/standard/logic/connectives/cast.lean

@@ -1,7 +1,11 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.eq logic.connectives.quantifiers
+
 using eq_proofs
 
 definition cast {A B : Type} (H : A = B) (a : A) : B :=
@@ -22,7 +26,8 @@ definition heq {A B : Type} (a : A) (b : B) :=
 
 infixl `==`:50 := heq
 
-theorem heq_elim {A B : Type} {C : Prop} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C :=
+theorem heq_elim {A B : Type} {C : Prop} {a : A} {b : B} (H1 : a == b)
+  (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C :=
 obtain w Hw, from H1, H2 w Hw
 
 theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B :=
@@ -44,7 +49,8 @@ eqt_elim (heq_to_eq H)
 
 opaque_hint (hiding cast)
 
-theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 : a == b) (H2 : P A a) : P B b :=
+theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 : a == b)
+  (H2 : P A a) : P B b :=
 have Haux1 : ∀ H : A = A, P A (cast H a), from
   assume H : A = A, (cast_eq H a)⁻¹ ▸ H2,
 obtain (Heq : A = B) (Hw : cast Heq a = b), from H1,
@@ -79,7 +85,8 @@ theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H1 : cast H a =
 calc a  == cast H a : hsymm (cast_heq H a)
     ... =  b        : H1
 
-theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) : cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
+theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) :
+  cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
 heq_to_eq (calc cast Hbc (cast Hab a)   == cast Hab a        : cast_heq Hbc (cast Hab a)
                                    ...  == a                 : cast_heq Hab a
                                    ...  == cast (Hab ⬝ Hbc) a : hsymm (cast_heq (Hab ⬝ Hbc) a))
@@ -96,7 +103,8 @@ cast_eq_to_heq e3
 theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) :=
 subst H (refl (Π x, B x))
 
-theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : cast (pi_eq H) f a == f a :=
+theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
+  cast (pi_eq H) f a == f a :=
 have H1 : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
   assume H, eq_to_heq (congr1 (cast_eq H f) a),
 have H2 : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
@@ -108,8 +116,9 @@ theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a
 heq_to_eq (calc cast (pi_eq H) f a == f a                     : cast_app' H f a
                              ...   == cast (congr1 H a) (f a) : hsymm (cast_heq (congr1 H a) (f a)))
 
-theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H1 : f == f') (H2 : B = B')
-                 : f a == f' a :=
+theorem hcongr1' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
+    (H1 : f == f') (H2 : B = B')
+  : f a == f' a :=
 heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
   calc f a == cast (pi_eq H2) f a  : hsymm (cast_app' H2 f a)
        ... =  cast Ht f a          : refl (cast Ht f a)

library/standard/logic/connectives/eq.lean

@@ -0,0 +1,107 @@
+----------------------------------------------------------------------------------------------------
+-- 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 logic.connectives.basic
+
+
+-- eq
+-- --
+
+inductive eq {A : Type} (a : A) : A → Prop :=
+| refl : eq a a
+
+infix `=`:50 := eq
+
+theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
+eq_rec H2 H1
+
+theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
+subst H2 H1
+
+calc_subst subst
+calc_refl  refl
+calc_trans trans
+
+theorem true_ne_false : ¬true = false :=
+assume H : true = false,
+  subst H trivial
+
+theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
+subst H (refl a)
+
+namespace eq_proofs
+  postfix `⁻¹`:100 := symm
+  infixr `⬝`:75     := trans
+  infixr `▸`:75    := subst
+end
+using eq_proofs
+
+theorem congr1 {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
+H ▸ refl (f a)
+
+theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
+H ▸ refl (f a)
+
+theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b :=
+H1 ▸ H2 ▸ refl (f a)
+
+theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
+take x, congr1 H x
+
+theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) :=
+congr2 not H
+
+theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
+H1 ▸ H2
+
+infixl `<|`:100 := eqmp
+infixl `◂`:100 := eqmp
+
+theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
+H1⁻¹ ◂ H2
+
+theorem eqt_elim {a : Prop} (H : a = true) : a :=
+H⁻¹ ◂ trivial
+
+theorem eqf_elim {a : Prop} (H : a = false) : ¬a :=
+assume Ha : a, H ◂ Ha
+
+theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
+assume Ha, H2 (H1 Ha)
+
+theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
+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
+-- --
+
+definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
+infix `≠`:50 := ne
+
+theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H
+
+theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := H1 H2
+
+theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
+
+theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
+
+theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
+assume H1 : b = a, H (H1⁻¹)
+
+theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := H1⁻¹ ▸ H2
+
+theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := H2 ▸ H1
+
+calc_trans eq_ne_trans
+calc_trans ne_eq_trans

library/standard/logic/connectives/if.lean

@@ -1,7 +1,11 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import decidable tactic
+----------------------------------------------------------------------------------------------------
+
+import logic.classes.decidable tools.tactic
+
 using decidable tactic
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=

library/standard/logic/connectives/prop.lean

@@ -0,0 +1,7 @@
+----------------------------------------------------------------------------------------------------
+-- 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
+----------------------------------------------------------------------------------------------------
+
+definition Prop [inline] := Type.{0}

library/standard/logic/connectives/quantifiers.lean

@@ -0,0 +1,39 @@
+----------------------------------------------------------------------------------------------------
+-- 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 logic.connectives.basic logic.connectives.eq
+
+inductive Exists {A : Type} (P : A → Prop) : Prop :=
+| exists_intro : ∀ (a : A), P a → Exists P
+
+notation `exists` binders `,` r:(scoped P, Exists P) := r
+notation `∃` binders `,` r:(scoped P, Exists P) := r
+
+theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
+Exists_rec H2 H1
+
+theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
+assume H1 : ∀x, ¬p x,
+  obtain (w : A) (Hw : p w), from H,
+  absurd Hw (H1 w)
+
+theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
+assume H1 : ∃x, ¬p x,
+  obtain (w : A) (Hw : ¬p w), from H1,
+  absurd (H2 w) Hw
+
+definition exists_unique {A : Type} (p : A → Prop) :=
+∃x, p x ∧ ∀y, y ≠ x → ¬p y
+
+notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
+
+theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬p y) : ∃!x, p x :=
+exists_intro w (and_intro H1 H2)
+
+theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
+                           (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬p y) → b) : b :=
+obtain w Hw, from H2,
+H1 w (and_elim_left Hw) (and_elim_right Hw)

library/standard/logic/default.lean

@@ -0,0 +1,9 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.basic logic.connectives.eq logic.connectives.quantifiers
+import logic.classes.decidable logic.classes.inhabited logic.classes.congr
+import logic.connectives.if

library/standard/tools/tactic.lean

@@ -1,7 +1,10 @@
+----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic string num
+----------------------------------------------------------------------------------------------------
+
+import data.string data.num
 using string
 using num