feat(library/init/classical): simpler choice axiom

library/init/classical.lean

@@ -1,7 +1,7 @@
 /-
 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
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import init.data.subtype.basic init.funext
@@ -11,7 +11,11 @@ namespace classical
 universes u v
 
 /- the axiom -/
-axiom indefinite_description {α : Sort u} (p : α → Prop) : (∃ x, p x) → {x // p x}
+axiom choice {α : Sort u} : nonempty α → α
+
+noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop) :
+  (∃ x, p x) → {x // p x} :=
+λ h, choice (let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩)
 
 /- Diaconescu's theorem: using function extensionality and propositional extensionality,
    we can get excluded middle from this. -/

tests/lean/print_ax1.lean.expected.out

@@ -1,3 +1,3 @@
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b

tests/lean/print_ax2.lean.expected.out

@@ -1,3 +1,3 @@
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b

tests/lean/print_ax3.lean.expected.out

@@ -2,7 +2,7 @@ print_ax3.lean:13:6: warning: declaration 'foo5' uses sorry
 no axioms
 ------
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=