Choice without the axiom of choice

choosable.lean

import data.quot
import tactic


variables {α : Type*} (P : α → Prop)

/-- A choosable instance is like decidable, but over `Type` instead of `Prop` -/
@[class] def choosable (α : Type*) := psum α (α → false)

/-- inhabited types are always choosable -/
instance inhabited.choosable {α : Type*} [inhabited α]: choosable α := psum.inl (default _)

/-- other types are choosable via the axiom of choice-/
noncomputable def classical_choosable (α : Type*) : choosable α :=
by classical; exact (if h : nonempty α then psum.inl (classical.choice h) else psum.inr (λ x, h ⟨x⟩))

/-- the ability to choose from a subtype is an algorithm to extract a witness from an existential -/
def decidable.indefinite_description (h : ∃ x, P x) [i : choosable (subtype P)] : {x // P x} :=
match i with
| (psum.inl x) := x
| (psum.inr pnx) := false.elim $ let ⟨x, px⟩ := h in pnx (⟨x, px⟩)
end

/-- the ability to choose from a subtype is an algorithm to decide an existential -/
instance {α : Type*} (P : α → Prop) : ∀ [choosable (subtype P)], decidable (∃ x, P x)
| (psum.inl ⟨x, px⟩) := is_true ⟨x, px⟩
| (psum.inr pnx) := is_false (not_exists.mpr $ λ x px, pnx ⟨x, px⟩)

/-- this probably isn't that useful -/
def decidable.choose {α : Type*} [nonempty α] [i : choosable α] : α :=
match i with
| (psum.inl x) := x
| (psum.inr pnx) := false.elim $ let ⟨x⟩ := ‹nonempty α› in pnx x
end