set.indefinite_description

Stream: general

[Kenny Lau]

Is it possible to fill in this sorry?

universes u
protected def set.indefinite_description {α : Type u}
  {p : set α → Prop} (h : ∃ s, p s) : { s : set α // p s} := sorry

[Reid Barton]

I guess you mean without adding noncomputable? Interesting question

[Mario Carneiro]

yes

universes u
protected def set.indefinite_description {α : Type u}
  {p : set α → Prop} (h : ∃ s, p s) : { s : set α // p s} :=
⟨{x : α | x ∈ classical.some h}, classical.some_spec h⟩

[Mario Carneiro]

I've mentioned before about "trivially computable" types, which includes subtypes of functions returning Prop

[Mario Carneiro]

Any term of such a type can be made computable with appropriate wrapping

[Mario Carneiro]

If you meant "without axioms", then no it's not possible, it would imply the axiom of choice

[Mario Carneiro]

However there is an interesting construction here for definite description with no axioms (well extensionality)

import data.set.basic

universes u
protected def set.definite_description {α : Type u}
  {p : set α → Prop} (h : ∃! s, p s) : { s : set α // p s} :=
⟨{x : α | ∃ s, x ∈ s ∧ p s ∧ ∀ y, p y → y = s},
let ⟨s, ps, al⟩ := h in
have s = {x : α | ∃ s, x ∈ s ∧ p s ∧ ∀ y, p y → y = s},
from set.ext $ λ x, ⟨λ xs, ⟨_, xs, ps, al⟩,
  λ ⟨s', xs', ps', al'⟩, (al' _ ps).symm ▸ xs'⟩,
this ▸ ps⟩

[Kenny Lau]

@Mario Carneiro so... we can have a "computable" basis?

[Mario Carneiro]

"computable" but not computable

[Mario Carneiro]

when I revisited bases recently, we discussed changing the definition of a basis from a set to a family over a type. In that case it wouldn't be computationally irrelevant