Getting a witness out of ∃

Stream: general

[Sebastian Zivota]

Is my understanding correct that I can't in general get the witness out of an existential formula? I.e., it's not possible to write the function

getWitness (h : ∃ x : T, P x) : T :=
  -- get the x that supposedly exists

without invoking Exists.choose?

[Riccardo Brasca]

You can use obtain ⟨x, hx⟩ := h if you are proving a Prop.

[Kyle Miller]

Yes you are correct. Defining getWitness is equivalent to defining Exists.choose.

[Kyle Miller]

Regarding what Riccardo said, this is what the following error is referring to:

def getWitness {T : Type _} (P : T → Prop) (h : ∃ x : T, P x) : T :=
begin
  cases h
  -- induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
end

This is saying that you're only allowed to get a witness (using the built-in theory) if your goal is a Prop.

[Sebastian Zivota]

I assume this is to preserve proof irrelevance? As in, I'm allowed to get the witness, but only in a context where it doesn't matter which specific value the witness has.

[Kyle Miller]

Yeah, when paired with the computation rule associated to the recursor (that Exists.dcases_on (Exists.mk x h) f = f x h in this case, I believe)

[Kyle Miller]

In fact, there was temporarily a bug in Lean 4 where you could prove false by eliminating an existential using projection notation. The kernel was allowing you to get the witness that was in the proof term when you weren't eliminating to Prop.

[Jannis Limperg]

If you need a proof-relevant variant of Exists, use Sigma.

[Yakov Pechersky]

There is also a way to get the witness provided you're over a fintype, docs#fintype.choose

[Jannis Limperg]

So this enumerates all elements of the type and checks the predicate for each? The type theorist in me is shocked and horrified.

[Eric Rodriguez]

why so, Jannis?

[Eric Rodriguez]

and furthermore there's also subsingleton elimination, which allows you to eliminate into from types that are syntactically a subsingleton or something along those lines

[Eric Rodriguez]

(ctrl+f for syntactic subsingleton here)

[Jannis Limperg]

Because we have a computable thing (otherwise the predicate would not be decidable or the type would not be a fintype), then we make it a Prop by wrapping it in an existential (saying, roughly, 'we don't care about computation here') and then we re-introduce computation in the slowest way possible. I'm sure there are good reasons for this in the context of mathlib, it just hurts a little bit. ;)

[Eric Rodriguez]

i think it's in some ways just done because people hate seeing noncomputable instinctively, even if it doesn't matter at all really

[Kyle Miller]

It's saying that if someone gives you the mere proof that there's a unique element, then there's at least some way to recover that value. It's the best you can do without knowing anything else about the type or the predicate. Wouldn't you agree it's better to have it around than not having it all?

Of course, given the specifics of your type and predicates, if you can use a better algorithm (and you care about runtime characteristics rather than just whether something can be computed), you should.

[Kyle Miller]

I doubt that fintype.choose is used much in definitions. Most of the time mathlib provides definitions rather than proving existentials.

[Kyle Miller]

It can also be used to avoid the axiom of choice inside of proofs, if that's something you care about doing. I'm not sure I've ever heard of anyone caring about algorithmic complexity of algorithms that appear inside of proofs yet.

[Eric Wieser]

Yakov Pechersky said:

There is also a way to get the witness provided you're over a fintype, docs#fintype.choose

docs#nat.find is another version for nat which obviously isn't a fintype

[Kyle Miller]

(@Jannis Limperg And maybe you'll like that nat.find works by testing each natural number successively until the predicate is true :wink:)

[Sebastian Zivota]

The reason I hit on this question in the first place is my toy axiomatization of the projective plane. One of the axioms says that for any two points there is a line containing both of them, and this allows defining the connecting line of any two points using Exists.choose. So the connecting line would be essentially noncomputable, even in cases where there should be no problem computing it. I'm now wondering if it wouldn't be better to take the function connecting_line (p q : P) : L as fundamental, as opposed to the existence statement.

[Kyle Miller]

I was actually thinking about that before. One wrinkle is that connecting_line p p can be any line that passes through p, which isn't very unique.

Another solution is to keep the projective plane axiomatization the same but have a separate typeclass that provides a computable connecting_line that provides a witness for the existential.

[Jannis Limperg]

Kyle Miller said:

It's saying that if someone gives you the mere proof that there's a unique element, then there's at least some way to recover that value. It's the best you can do without knowing anything else about the type or the predicate. Wouldn't you agree it's better to have it around than not having it all?

Sure, I don't hate the lemma at all, it does what it can with the information provided. My question would just be why the information provided is not a Sigma. (And again, there may be good reasons for that.)

[Kyle Miller]

What do you mean, providing a Sigma to the lemma?

[Reid Barton]

Like if you are working constructively, why did you make an Exists in the first place

[Kyle Miller]

Maybe you have a general lemma that's not proved constructively, but in your specific circumstances you can use this lemma with fintype.choose to get a quick algorithm.

[Reid Barton]

By which you mean a sloooooooow algorithm.

[Kyle Miller]

Maybe it's fin 5 or something else of small cardinality and it's not so bad.

[Reid Barton]

Then you can probably do it faster in your head as well

[Reid Barton]

I remember when the odd order theorem was proved in Coq, Gonthier would talk about how the proof was purely constructive and so it gave an algorithm for finding a composition series for any group of odd order. That always seemed like a strange thing to point out.

[Reid Barton]

Since "we already know the odd order theorem is true so just test every subset to see if it's a normal subgroup" is also such an algorithm.

[Kyle Miller]

Another thing about fintype.choose is that it's implementing the function from Exists_unique to Sigma, which is nice to know it exists, hence why mathlib should have it.

[Kyle Miller]

Do you happen to know what sort of algorithm falls out of Gonthier's proof?

[Kevin Buzzard]

If we're taking bets, then my bet is that it's a lot worse than Reid's suggestion, which is...already not great.