feat(frontends/lean/brackets): notation for set replacement (#402)

[As discussed on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.204.20notation).

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.

src/frontends/lean/brackets.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/placeholder.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/structure_instance.h"
@@ -37,6 +38,36 @@ static expr parse_set_of(parser & p, pos_info const & pos, expr const & local) {
     return p.mk_app(set_of, pred, pos);
 }
 
+/* Parse rest of the set_replacement expression prefix '{' '(' expr ')' '|' ... */
+static expr parse_set_replacement(parser & p, pos_info const & pos, expr const & hole_expr) {
+    // At this point, we have parsed `hole_expr`, assuming all identifiers are local variables.
+    // This will work, as long as we later update any identifiers that actually are globals.
+    // So we parse the binders, assemble an expression for the characteristic predicate,
+    // then use `patexpr_to_expr` to do the updating.
+    buffer<expr> params;
+    auto env = p.parse_binders(params, false);
+    p.check_token_next(get_rcurly_tk(), "invalid set_replacement, '}' expected");
+
+    // The predicate will look like `λ _x, ∃ p_1, ∃ p_2, ..., hole_expr[p_1, p_2, ...] = _x`.
+    name x_name = name("_x");
+    expr x = p.id_to_expr(x_name, pos);
+    // `hole_expr[p1, p2, ...] = _x`
+    expr pred = p.mk_app(mk_constant(get_eq_name()), hole_expr, pos);
+    pred = p.mk_app(pred, x, pos);
+
+    expr exists = mk_constant(get_Exists_name());
+    for (int i = params.size() - 1; i >= 0; i--) {
+        // `∃ p_i, ∃ p_(i+1) ..., hole_expr[p_1, p_2, ...] = _x`
+        pred = p.mk_app(exists, p.save_pos(Fun(params[i], pred), pos), pos);
+    }
+    // `λ _x, ∃ p_1, ∃ p_2, ..., hole_expr[p_1, p_2, ...] = _x`
+    pred = p.save_pos(Fun(x, pred), pos);
+    // Update identifiers so globals are actually globals.
+    pred = p.patexpr_to_expr(pred);
+    // `{_x | ∃ p_1, ∃ p_2, ..., hole_expr[p_1, p_2, ...] = _x}`
+    return p.mk_app(mk_constant(get_set_of_name()), pred, pos);
+}
+
 /* Create singletoncollection for '{' expr '}' */
 static expr mk_singleton(parser & p, pos_info const & pos, expr const & e) {
     return p.mk_app(p.save_pos(mk_constant(get_has_singleton_singleton_name()), pos), e, pos);
@@ -186,6 +217,17 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
             }
             e = left;
         }
+    } else if (p.curr_is_token(get_lparen_tk())) {
+        // '{' '(' expr ')' '|' binders '}'
+        p.next();
+        // The expression is parsed before the binders, so we need to make a new scope here.
+        // We assume for now all identifiers are in this scope,
+        // and parse_set_replacement will update any variables once it determines the actual binders.
+        parser::local_scope scope(p);
+        parser::all_id_local_scope scope_assumption(p);
+        e = parse_lparen(p, 0, NULL, pos); // parses the `expr ')'` part of the expression
+        p.check_token_next(get_bar_tk(), "invalid set replacement notation, '|' expected");
+        return parse_set_replacement(p, pos, e);
     } else if (p.curr_is_token(get_period_tk())) {
         p.next();
         p.check_token_next(get_rcurly_tk(), "invalid empty structure instance, '}' expected");

src/frontends/lean/builtin_exprs.cpp

@@ -854,7 +854,7 @@ static expr parse_infix_paren(parser & p, list<notation::accepting> const & accs
     return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
 }
 
-static expr parse_lparen(parser & p, unsigned, expr const *, pos_info const & pos) {
+expr parse_lparen(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (auto accs = is_infix_paren_notation(p))
         return parse_infix_paren(p, accs, pos);
     expr e = p.parse_expr();

src/frontends/lean/builtin_exprs.h

@@ -26,4 +26,6 @@ expr update_hole_args(expr const & e, expr const & new_args);
 
 void initialize_builtin_exprs();
 void finalize_builtin_exprs();
+
+expr parse_lparen(parser & p, unsigned, expr const *, pos_info const & pos);
 }

tests/lean/set_replacement.lean

@@ -0,0 +1,26 @@
+def successors : set nat := {(x + 1) | x : nat}
+lemma successors_correct : successors = {x | ∃ y, y + 1 = x} := rfl
+
+variables {x' : nat}
+
+def successors' : set nat := {(x' + 1) | x'}
+lemma successors_correct' : successors = successors' := rfl
+
+def x'' := 0
+
+def successors'' : set nat := {(x'' + 1) | x''}
+lemma successors_correct'' : successors = successors'' := rfl
+
+def f : nat -> nat := λ x, x + 1
+
+def successors''' : set nat := {(f x) | x}
+lemma successors_correct''' : successors = successors''' := rfl
+
+def between_1_and_5 : set nat := {(x + 1) | x < 5}
+lemma between_1_and_5_correct :
+  between_1_and_5 = {y | ∃ (x : nat) (h : x < 5), x + 1 = y} := rfl
+
+def triangle : set (nat × nat) := {(x, y) | (x y) (h : x + y < 5)}
+lemma triangle_correct :
+  triangle = {xy | ∃ (x y : nat) (h : x + y < 5), (x, y) = xy} := rfl
+