feat(library/standard/logic): add class nonempty

library/standard/logic/axioms/examples/diaconescu.lean

@@ -18,15 +18,10 @@ definition u [private] := epsilon (λx, x = true ∨ p)
 definition v [private] := epsilon (λx, x = false ∨ p)
 
 lemma u_def [private] : u = true ∨ p :=
-sorry
--- previous proof:
--- epsilon_spec (exists_intro true (or_inl (refl true))
--- fully elaborated: 
--- @epsilon_spec Prop (λx : Prop, x = true ∨ p) (exists_intro true (or_inl (refl true)))
+epsilon_spec (exists_intro true (or_inl (refl true)))
 
 lemma v_def [private] : v = false ∨ p :=
-sorry
--- epsilon_spec (exists_intro false (or_inl (refl false))
+epsilon_spec (exists_intro false (or_inl (refl false)))
 
 lemma uv_implies_p [private] : ¬(u = v) ∨ p :=
 or_elim u_def

library/standard/logic/axioms/hilbert.lean

@@ -2,7 +2,8 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq logic.connectives.quantifiers
+import logic.connectives.eq logic.connectives.quantifiers
+import logic.classes.inhabited logic.classes.nonempty
 import data.subtype data.sum
 
 using subtype
@@ -19,33 +20,36 @@ axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A)
 -- 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 :=
+nonempty_elim H (take x, exists_intro x trivial)
+
 theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
-let u : {x : A | nonempty A → true} := strong_indefinite_description (λa, true) H in
+let u : {x : A | (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in
 inhabited_intro (elt_of u)
 
 theorem inhabited_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
-nonempty_imp_inhabited (obtain w Hw, from H, exists_intro w trivial)
+nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w)
 
 
 -- the Hilbert epsilon function
 -- ----------------------------
 
-definition epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A :=
+definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A :=
 let u : {x : A | (∃y, P y) → P x} :=
-  strong_indefinite_description P (inhabited_imp_nonempty H) in
+  strong_indefinite_description P H in
 elt_of u
 
-theorem epsilon_spec_aux {A : Type} (H : inhabited A) (P : A → Prop) (Hex : ∃y, P y) :
+theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
     P (@epsilon A H P) :=
 let u : {x : A | (∃y, P y) → P x} :=
-  strong_indefinite_description P (inhabited_imp_nonempty H) in
+  strong_indefinite_description P H in
 has_property u Hex
 
 theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
-    P (@epsilon A (inhabited_exists Hex) P) :=
-epsilon_spec_aux (inhabited_exists Hex) P Hex
+    P (@epsilon A (exists_imp_nonempty Hex) P) :=
+epsilon_spec_aux (exists_imp_nonempty Hex) P Hex
 
-theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a :=
+theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty_intro a) (λx, x = a) = a :=
 epsilon_spec (exists_intro a (refl a))
 
 
@@ -54,7 +58,7 @@ epsilon_spec (exists_intro a (refl a))
 
 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) :=
-let f [inline] := λx, @epsilon _ (inhabited_exists (H x)) (λy, R x y),
+let f [inline] := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
     H [inline] := take x, epsilon_spec (H x)
 in exists_intro f H
 

library/standard/logic/connectives/quantifiers.lean

@@ -1,10 +1,8 @@
-----------------------------------------------------------------------------------------------------
 -- 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 .basic .eq ..classes.inhabited
+import .basic .eq ..classes.nonempty
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 | exists_intro : ∀ (a : A), P a → Exists P
@@ -78,9 +76,5 @@ iff_intro
     (assume H2, obtain (w : A) (Hw : ψ w), from H2,
       exists_intro w (or_inr Hw)))
 
-abbreviation nonempty (A : Type) := ∃x : A, true
-
-theorem nonempty_intro {A : Type} (x : A) : nonempty A := exists_intro x trivial
-
-theorem inhabited_imp_nonempty {A : Type} (H : inhabited A) : nonempty A :=
-exists_intro (default A) trivial
+theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
+obtain w Hw, from H, nonempty_intro w