## Stream: new members

### Topic: Existential witness in ite

#### Horatiu Cheval (Feb 13 2021 at 17:53):

Can I get the witness from h constructively here (given that h : q a has a constructive proof)?

constant α : Type
constant p : α → α → Prop

def q (a : α) := ∃ x, p a x

instance decq (a : α) : decidable (q a) := sorry

noncomputable
def f (a : α) : α := if h : q a then classical.some h else a


My understanding is that in general you can't get the witness from the proof of an existential when defining computational data,
and that you should use subtypes for that. But then I can't if-then-else on a subtype.

#### Eric Wieser (Feb 13 2021 at 20:30):

You can use psum (subtype p) (subtype p -> false) and do cases on that

#### Horatiu Cheval (Feb 13 2021 at 22:02):

Nice! I imagined there would be something analogous to decidable for subtypes, but couldn't figure out how to do it, thanks

#### Eric Wieser (Feb 13 2021 at 23:07):

Perhaps mathlib is too classical for it to make sense, but IMO it would be great to have something like my gist in mathlib

#### Eric Wieser (Feb 13 2021 at 23:08):

Which would mean instead of a lemma saying "assume the axiom of choice", it can say "assume an algorithm for computing this witness exists", and the caller can say "the axiom of choice provides such an algorithm"

#### Eric Wieser (Feb 13 2021 at 23:09):

Which is roughly what mathlib already does anyway for algorithms about deciding the truth of propositions

#### Bryan Gin-ge Chen (Feb 13 2021 at 23:28):

I don't think it would hurt to have it in mathlib, though as you point out it might not end up used too much.

Last updated: May 10 2021 at 00:31 UTC