Zulip Chat Archive

Stream: new members

Topic: Existential witness in ite


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 13 2021 at 20:30):

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

view this post on Zulip Eric Wieser (Feb 13 2021 at 20:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Eric Wieser (Feb 13 2021 at 23:09):

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

view this post on Zulip 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