Computing the witness of an existential

Stream: Is there code for X?

[Alex Keizer]

Say I have a finite type A, a decidable property p : A -> Prop and a proof of exists a, P a, do we have code to compute an element a : A that satisfies P a?

[Eric Wieser]

It's not possible, because what if there are two elements that satisfy P?

[Eric Wieser]

docs#Fintype.choose is the version that is possible

[Alex Keizer]

Thanks! My existential should be unique, so that works

[Alex Keizer]

I should have phrased my question slightly different, maybe. I don't care that the element that is returned is the same as the witness, just that I can compute any element that satisfies P a. That should still be possible in the non-unique case, shouldn't it?

[Eric Wieser]

If there are two matching elements, which one should it return?

[Alex Keizer]

Ah, Finset is (transitively) implemented as a quotient, so our choice has to be irrespective of the ordering of the elements. That is problematic, yeah.

[Alex Keizer]

It would work if we have a FinEnum A instance , then we can just pick the first element (according to the enumeration) that satisfies P

[Eric Wieser]

Exactly!