Zulip Chat Archive

Stream: general

Topic: Getting a witness out of ∃


Sebastian Zivota (Jan 30 2023 at 11:11):

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 (Jan 30 2023 at 11:15):

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

Kyle Miller (Jan 30 2023 at 11:15):

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

Kyle Miller (Jan 30 2023 at 11:16):

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 (Jan 30 2023 at 11:18):

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 (Jan 30 2023 at 11:20):

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 (Jan 30 2023 at 11:25):

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 (Jan 30 2023 at 11:25):

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

Yakov Pechersky (Jan 30 2023 at 12:36):

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

Jannis Limperg (Jan 30 2023 at 12:46):

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 (Jan 30 2023 at 13:02):

why so, Jannis?

Eric Rodriguez (Jan 30 2023 at 13:03):

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 (Jan 30 2023 at 13:06):

(ctrl+f for syntactic subsingleton here)

Jannis Limperg (Jan 30 2023 at 14:06):

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 (Jan 30 2023 at 14:16):

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 (Jan 30 2023 at 14:17):

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 (Jan 30 2023 at 14:19):

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

Kyle Miller (Jan 30 2023 at 14:21):

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 (Jan 30 2023 at 14:23):

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 (Jan 30 2023 at 14:26):

(@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 (Jan 30 2023 at 14:27):

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 (Jan 30 2023 at 14:30):

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 (Jan 30 2023 at 14:33):

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 (Jan 30 2023 at 14:36):

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

Reid Barton (Jan 30 2023 at 14:37):

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

Kyle Miller (Jan 30 2023 at 14:38):

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 (Jan 30 2023 at 14:39):

By which you mean a sloooooooow algorithm.

Kyle Miller (Jan 30 2023 at 14:39):

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

Reid Barton (Jan 30 2023 at 14:40):

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

Reid Barton (Jan 30 2023 at 14:41):

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 (Jan 30 2023 at 14:42):

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 (Jan 30 2023 at 14:43):

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 (Jan 30 2023 at 14:44):

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

Kevin Buzzard (Jan 30 2023 at 14:51):

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


Last updated: Dec 20 2023 at 11:08 UTC