refactor(library/logic/axioms): rename theorems

library/algebra/category/constructions.lean

@@ -49,9 +49,9 @@ namespace category
   mk (λa b, a → b)
      (λ a b c, function.compose)
      (λ a, function.id)
-     (λ a b c d h g f, symm (function.compose_assoc h g f))
-     (λ a b f, function.compose_id_left f)
-     (λ a b f, function.compose_id_right f)
+     (λ a b c d h g f, symm (function.compose.assoc h g f))
+     (λ a b f, function.compose.left_id f)
+     (λ a b f, function.compose.right_id f)
 
   definition Type_category [reducible] : Category := Mk type_category
 

library/logic/axioms/classical.lean

@@ -12,6 +12,8 @@ open eq.ops
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
 
+definition eq_true_or_eq_false := prop_complete
+
 theorem cases (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
 or.elim (prop_complete a)
   (assume Ht : a = true,  Ht⁻¹ ▸ H1)
@@ -26,7 +28,7 @@ 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))
 
-theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true :=
+theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
 cases (λ x, x = false ∨ x = true)
   (or.inr rfl)
   (or.inl rfl)

library/logic/axioms/default.lean

@@ -1,8 +1,10 @@
-----------------------------------------------------------------------------------------------------
---- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Jeremy Avigad
-----------------------------------------------------------------------------------------------------
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.axioms.default
+Author: Jeremy Avigad
+-/
 
 import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert
 import logic.axioms.prop_decidable

library/logic/axioms/funext.lean

@@ -14,13 +14,13 @@ axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π a, B a} (H : ∀ a, f a
 namespace function
   variables {A B C D: Type}
 
-  theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
+  theorem compose.assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
   funext (take x, rfl)
 
-  theorem compose_id_left (f : A → B) : id ∘ f = f :=
+  theorem compose.left_id (f : A → B) : id ∘ f = f :=
   funext (take x, rfl)
 
-  theorem compose_id_right (f : A → B) : f ∘ id = f :=
+  theorem compose.right_id (f : A → B) : f ∘ id = f :=
   funext (take x, rfl)
 
   theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=

library/logic/axioms/hilbert.lean

@@ -1,40 +1,36 @@
--- 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
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- logic.axioms.hilbert
--- ====================
+Module: logic.axioms.hilbert
+Authors: Leonardo de Moura, Jeremy Avigad
+
+Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the constructive one).
+-/
 
--- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
--- constructive one).
 import logic.quantifiers
 import data.subtype data.sum
 
 open subtype inhabited nonempty
 
+/- the axiom -/
 
--- the axiom
--- ---------
-
+-- In the presence of classical logic, we could prove this from a weaker statement:
+-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
 axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
   { x | (∃y : A, P y) → P x}
 
--- In the presence of classical logic, we could prove this from the weaker
--- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
-
-theorem nonempty_imp_exists_true {A : Type} (H : nonempty A) : ∃x : A, true :=
+theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
 nonempty.elim H (take x, exists.intro x trivial)
 
-theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
+theorem inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
 let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
 inhabited.mk (elt_of u)
 
-theorem exists_imp_inhabited {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
-nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w)
+theorem inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
+inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
 
-
--- the Hilbert epsilon function
--- ----------------------------
+/- the Hilbert epsilon function -/
 
 opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
 let u : {x | (∃y, P y) → P x} :=
@@ -54,9 +50,7 @@ epsilon_spec_aux (nonempty_of_exists Hex) P Hex
 theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
 epsilon_spec (exists.intro a (eq.refl a))
 
-
--- the axiom of choice
--- -------------------
+/- the axiom of choice -/
 
 theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
   ∃f, ∀x, R x (f x) :=

library/logic/axioms/prop_decidable.lean

@@ -1,9 +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
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- logic.axioms.prop_decidable
--- ===========================
+Module: logic.axioms.prop_decidable
+Author: Leonardo de Moura
+-/
 
 import logic.axioms.classical logic.axioms.hilbert
 open decidable inhabited nonempty
@@ -12,7 +13,7 @@ open decidable inhabited nonempty
 
 -- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle
 theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
-nonempty_imp_inhabited
+inhabited_of_nonempty
   (or.elim (em a)
     (assume Ha, nonempty.intro (inl Ha))
     (assume Hna, nonempty.intro (inr Hna)))