Zulip Chat Archive

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

Eric Wieser (Feb 13 2021 at 20:34):

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

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: Dec 20 2023 at 11:08 UTC