[Merged by Bors] - feat(frontends/lean/brackets): notation for set replacement

[Vierkantor]

As discussed on Zulip.

This PR introduces notation for set replacement, so that {(f x) | x ∈ s} is equivalent to set.image f s. More generally, {(expr) | binders} parses to something like set_of (λ _x, ∃ binders, expr = _x). The expression needs to be between parentheses to ensure it is not ambiguous with the { id | predicate } notation for separation and to decrease the amount of backtracking. Expressions of the form {(x, y) | (x y : ℕ) (p : x + y < 10)} also work as expected.

[gebner]

I like it, and the implementation looks good. Is set_of ... the term that we want?

[fpvandoorn]

{(f x) | x ∈ s} is equivalent to set.image f s

Too bad they are not definitionally equal. But I guess we can have simp lemmas rewriting them.

[Vierkantor]

{(f x) | x ∈ s} is equivalent to set.image f s

Too bad they are not definitionally equal. But I guess we can have simp lemmas rewriting them.

The issue is that the notation expands to ∃ (h : x ∈ s), ... instead of x ∈ s \and ..., right? simp should already fix that with the exists_prop lemma.

[gebner]

Another option would be to move set.image to the core library. I can't tell at first glance if this would make things easier or harder.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build linux Release
• Build linux Debug
• Build macos Release
• Build emscripten
• Build windows Release
• Build macos Debug

[fpvandoorn]

Another option would be to move set.image to the core library. I can't tell at first glance if this would make things easier or harder.

set.image is already in core: https://github.com/leanprover-community/lean/blob/05d7184/library/init/data/set.lean#L83

{(f x) | x ∈ s} is equivalent to set.image f s

Too bad they are not definitionally equal. But I guess we can have simp lemmas rewriting them.

The issue is that the notation expands to ∃ (h : x ∈ s), ... instead of x ∈ s \and ..., right? simp should already fix that with the exists_prop lemma.

Correct, then you get something definitionally equal, but presumably you want to actually rewrite it to set.image instead of (the definiens of set.image)