Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# eric-wieser/choosable.lean

Created Feb 3, 2021
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
to join this conversation on GitHub. Already have an account? Sign in to comment