Skip to content

Instantly share code, notes, and snippets.

@eric-wieser
Created February 3, 2021 16:59
Show Gist options
  • Save eric-wieser/103ad49e8c5c4415991b7622f77c48e0 to your computer and use it in GitHub Desktop.
Save eric-wieser/103ad49e8c5c4415991b7622f77c48e0 to your computer and use it in GitHub Desktop.
Choice without the axiom of choice
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment