Choice is computable!

Stream: general

[Alex Meiburg]

Good news guys -- Choice can now be built in an entirely computable fashion! :) Behold the demonstration below:

import Mathlib

-- Multi-sorted version of `Option`
inductive POption (α : Sort u) where
  /-- No value. -/
  | none : POption α
  /-- Some value of type `α`. -/
  | some (val : α) : POption α

instance : Inhabited (POption α) := ⟨POption.none⟩

noncomputable instance aux_1_sound {α : Sort u} (p : { p' : α → Prop // ∃ x, p' x}) :
    Inhabited {x // p.val x} :=
  let h : Nonempty (Subtype _) := Exists.elim p.property (fun w h => ⟨w, h⟩);
  Classical.inhabited_of_nonempty h

partial def aux_1 {α : Sort u} (p : { p' : α → Prop // ∃ x, p' x}) (f₁ : Prop → POption {x // p.val x}
    := (inferInstance : Inhabited _).default) : {x // p.val x} :=
  conf (type_of% @proof_irrel_heq) where --proof irrelevance
  conf (q : Prop) : {x // p.val x} :=
  match f₁ q with
  | POption.some x => x
  | _ => conf (¬q ∨ q) --law of excluded middle

--and now the main event:

/-computable-/
def computable_indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
  aux_1 ⟨p,h⟩

/-computable-/
def computable_choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
  (computable_indefiniteDescription p h).val

theorem computable_choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (computable_choose h) :=
  (computable_indefiniteDescription p h).property

--double check that the new `computable_choose` is identical in type to `Classical.choose`:
#check (@Classical.choose : type_of% @computable_choose)
#check (@computable_choose : type_of% @Classical.choose)

My computable_choose isn't marked noncomputable, and as we can see it has the exact same type signature as that stinky old noncomputable Classical.choose. And it all typechecks and compiles fine without any sorrys or extra axioms :tada: !

(I know I'm about two days overdue here, but I only had the idea just now... :relieved: )

EDIT: an older version of this was about the law of the excluded middle, preserved below so that the following few messages make sense, but this was an error.

old text

Good news guys -- the law of the excluded middle can now be built in an entirely computable fashion! :) Behold the demonstration below:

import Mathlib

inductive POption (α : Sort u) where
/-- No value. -/
| none : POption α
/-- Some value of type α. -/
| some (val : α) : POption α

instance aux_nat_1_sound (p : Prop) : Inhabited (p ∨ ¬p) :=
⟨Classical.em p⟩

partial def aux_nat_1 (p : Prop) (f₁ : ℕ → POption p) (f₂ : ℕ → POption ¬p) : p ∨ ¬p :=
conf 0 where
conf (n : ℕ) : p ∨ ¬p :=
match f₁ n with
| POption.some x => Or.inl x
| _ => match f₂ n with
| POption.some y => Or.inr y
| _ => conf n.succ

/-computable-/
def computable_em (p : Prop) : p ∨ ¬p :=
let proof_1 := fun _ ↦ POption.none;
let proof_2 := fun _ ↦ POption.none;
aux_nat_1 (p) (proof_1) (proof_2)

theorem computable_em_is_Classical_em : (type_of% @computable_em) = (type_of% @Classical.em) :=
rfl

My computable_em isn't marked noncomputable, and computable_em_is_Classical_em proves it has the exact same type signature as that stinky old noncomputable Classical.em. And it all checks and compiles fine without any sorrys or extra axioms :tada:

(I know I'm about two days overdue here, but I only had the idea just now... :relieved: )

[Kim Morrison]

I'm not sure what you're claiming here. You know you can write def computable_em' := Classical.em?

[Matt Diamond]

it's a belated April Fool's joke, though Scott's point deflates it a bit

[Kim Morrison]

Oops, I'm terrible at noticing April. :-)

[Alex Meiburg]

Alright, I admit I kind of botched the joke there since the law of the excluded middle is computable. I think the new version is more surprising / entertaining -- that I can make an entirely computable version of Classical.choose. :)

[Mario Carneiro]

the trick

partial def aux_nat_1 is a partial recursive function, and computable_indefiniteDescription calls aux_nat_1 in a way which guarantees it will not halt. Here's a way of generalizing it to make any term of any type computable:

axiom T : Type
axiom foo : T
@[instance] axiom repr_T : Repr T

#eval foo  -- failed to compile definition, consider marking it as 'noncomputable'

noncomputable local instance : Inhabited T := ⟨foo⟩ in
partial def foo' : T := go () where go : Unit → T := go

noncomputable local instance : Inhabited (Repr T) := ⟨repr_T⟩ in
@[instance] partial def repr_T' : Repr T := go () where go : Unit → Repr T := go

-- #eval foo' -- all better