Existential quantifier set mem

Stream: lean4

[Brandon Brown]

In Lean3 there is the shorthand ∃ x ∈ s, p for some set S and Prop P, which gets translated to ∃ x, x ∈ s ∧ p under-the-hood. Has anyone implemented this in Lean4 yet?

[Patrick Massot]

Note this is not what it gets translated to in Lean 3.

[Patrick Massot]

example {α : Type*} {s : set α} {p : Prop} : (∃ x ∈ s, p) ↔ ∃ x, x ∈ s ∧ p :=
iff.rfl -- fails

example {α : Type*} {s : set α} {p : Prop} : (∃ x ∈ s, p) ↔ ∃ (x : α) (h : x ∈ s), p :=
iff.rfl -- works

[Brandon Brown]

Ah thanks

[Patrick Massot]

I'm sorry this isn't answering your question at all, but I thought it was good to know.

[Brandon Brown]

Definitely good to know!

[Mario Carneiro]

Brandon Brown said:

Has anyone implemented this in Lean4 yet?

Kevin implemented something similar to this in his Data.Set.Basic

[Kevin Buzzard]

I stole all of this stuff from other people. Maybe it was @Jason KY. who actually wrote this?

[Kevin Buzzard]

Here's a link. Note that hasLessEq changed to LE recently. I will probably port this code to the official mathlib4 repo on Thursday.

[Jason KY.]

| `(∃ $x:ident ∈ $s, $p) => `(∃ $x:ident, $x ∈ $s ∧ $p)`

It seems that I wrote shorthand Brandon is thinking about instead of the lean3 version

[Kevin Buzzard]

Thanks for pointing this out! I will almost certainly change it to the Lean 3 version on Thursday (if I can figure out how to) (hopefully you'll be at Xena Jason :D)

[Mario Carneiro]

The exists-and version is better than exists-exists, but this was a limitation of the way the lean 3 desugaring works

[Mario Carneiro]

the limitation of the lean 4 desugaring is that it has to be defined individually for all binops and binders

[Mario Carneiro]

By the way this macro in Data.Set.Basic is wrong:

| `({ $x:ident ∈ $s | $p }) => `(setOf (λ $x => $x ∈ $s → $p))

it should use ∧ on the rhs

[Eric Wieser]

So that means every new binder has to introduce new notation for its interaction with le and mem?

[Eric Wieser]

Even if that interaction is always "just nest the binders"

[Mario Carneiro]

I think it is possible to separate the two, using something like the index syntax class introduced in Data.Set.Basic, but right now the binder group syntax class is rather underdeveloped, I don't think we are ready to handle the desugaring of \exists (x \in A) (y \in B), p yet

[Patrick Massot]

Mario Carneiro said:

The exists-and version is better than exists-exists, but this was a limitation of the way the lean 3 desugaring works

Oh yes, the Lean 3 version is very painful for teaching. Things got better only thanks to #5440