lean#402: set builder notation

Stream: PR reviews

[Gabriel Ebner]

I like it and and would be fine with merging it, but I haven't been following the discussion. Is this what people want?
@Kevin Buzzard requested this AFAICT.

[Johan Commelin]

Since p : X \times Y is not defeq to (p.1, p.2), can we make

{(x, y) | (x y : ℕ) (h : x + y < 10)}

syntactic sugar for

{p | (p : ℕ \times ℕ) (h : p.1 + p.2 < 10)}

because the latter has better defeq behaviour...

[Anne Baanen]

Making the comma have special behaviour should be possible and in fact it is already a special case in the parser. The rewriting of x to p.1 and y to p.2 is more complicated though, and it would get even worse if we also want to support {(x, (y, z), w) | ...} : set (nat × (nat × nat) × nat)

[Johan Commelin]

Aha... (maybe it's easier to make p be defeq to (p.1, p.2) :oops: )

[Kevin Buzzard]

Why would it get worse? rintro can do it?

[Johan Commelin]

We've had lots of trouble with such definitions right? Wasn't uncurry broken (maybe it still is?)

[Johan Commelin]

It means you can't apply your predicate to a pair that is not of the form (x,y) and hope that it works. You'll have to manually do cases all the time.

[Anne Baanen]

I mean the rewriting in the parser would be difficult to implement correctly. The outcome would be easier to use indeed.

[Rob Lewis]

This is causing trouble here. The changes are all fixable but the fixes feel like regressions. I'm wondering if we should reconsider the syntax here.

[Mario Carneiro]

Why is {(a, b)} not working anymore?

[Gabriel Ebner]

lean#415

[Anne Baanen]

Oops, I should have realized this.

[Anne Baanen]

A quick fix (the syntax of the code is correct but otherwise untested) is to change the lines changed in #415 into the following instead:

        if (p.curr_is_token(get_bar_tk())) {
            return parse_set_replacement(p, pos, e);
        } else if (p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_rcurly_tk())) {
            return parse_fin_set(p, pos, p.patexpr_to_expr(e));
        } else {
            return p.parser_error_or_expr({"invalid '{' expression, ',', '}', or `|` expected", p.pos()});
        }

We need to accept a , as well as a } to parse it as a singleton + insert (as in lines 247 onwards) fixing lean#418. We also need to call patexpr_to_expr to ensure all variables are bound (because the syntax has binders after the expression, we cannot put anything in scope until we have reached the closing bracket).

[Anne Baanen]

I assume calling patexpr_to_expr will fix lean#419, although I would have expected the error to look more like "unbound variable α".

[Gabriel Ebner]

Thanks @Anne Baanen! lean#419