Existential witness in ite

Stream: new members

[Horatiu Cheval]

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]

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

[Eric Wieser]

I made a gist of that at https://gist.github.com/eric-wieser/103ad49e8c5c4415991b7622f77c48e0

[Horatiu Cheval]

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

[Eric Wieser]

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]

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]

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

[Bryan Gin-ge Chen]

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.