exists with member constraint confusion

Stream: general

[Bernd Losert]

What does ∃ x ∈ xs, p x translate to? The lean output shows ∃ (x : a) (_h : x ∈ xs), p x, but what does this translate to? What does a value of this type look like?

[Mario Carneiro]

it literally means ∃ (x : a), ∃ (_h : x ∈ xs), p x

[Bernd Losert]

Ah, so it's iterated.

[Bernd Losert]

So values are triples then.

[Mario Carneiro]

The part that is weird there is the second existential, which says that there exists a proof of x in xs such that p x holds. This is just the same as x ∈ xs /\ p x

[Mario Carneiro]

All binders like this are iterated when you use multiple variables in the binder group

[Bernd Losert]

It's not exactly the same as that though because I tried giving it that type and it didn't work.

[Mario Carneiro]

in surprisingly many cases this turns out to be the right thing

[Mario Carneiro]

right, it's not defeq but it is logically equivalent

[Bernd Losert]

Right.

[Mario Carneiro]

and there is a simp lemma that will rewrite it to a conjunction if you prefer

[Bernd Losert]

Which?

[Mario Carneiro]

but you can construct and destruct it with \<h1, h2\> either way

[Mario Carneiro]

the simp lemma will turn the existential into a conjunction

[Mario Carneiro]

docs#exists_prop

[Bernd Losert]

Cool. Thanks.