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: May 10 2021 at 00:31 UTC