Cleanup of `let`/`have` syntaxes

Stream: lean4

[Kyle Miller]

I'm working through cleaning up and unifying the various let/have binding syntaxes in Lean, so that they have the same features (e.g. allowing let := v) and also adding things like let (eq := h) x := v to get an h : x = v in context, which also works with pattern matching by the way, as a synonym for doing match h : v with | x => ....

There are a couple things that are causing issues, to the point where it should get community feedback.

I'll try to explain using some stream-of-conciousness bullet points:

• Design assumption: we want let and have to parse using the exact same rules. Rationale: differences make Lean more difficult to learn, and the only difference should be whether or not the value of the binding is visible in the local context.
• The "anaphoric" syntaxes let := v and have := v support binders, as in have (x y) (h) := ..., which creates a this function of three arguments.
• The syntaxes also support pattern matching, as in let (x,y) := p
• However, there is an ambiguity with let (rfl) := h, which looks like a one-binder anaphoric let.
• I gave patterns in parentheses higher priority to compensate for this. So, let (rfl) := h parses as a pattern, rather than as a this function taking rfl as an argument.
• However, people legitimately are writing things like have (x) := ... in mathlib.
• That's easy to work around by writing have (x : _) := ... or have this x := ... or have := fun x => .... (One-argument anaphoric have is kind of weird, right?)
• Anaphoric have with any number of binders is kind of weird, but it's well-used in mathlib, so it's staying.
• Another solution to the pattern problem could be to require more parentheses, like let ((rfl)) := h. Pattern matching seems more important than supporting anaphoric let/have with a single (x) binder. It's already confusing how let ctor x y z := v parses as a function definition rather than as let (ctor x y z) := v. Needing double parentheses seems rather obscure! How likely would someone guess to use double parentheses? (That all said, rfl is one of the few argument-free constructors — maybe let rfl := ... should be special syntax!)

[Kyle Miller]

I don't have any specific question here, other than perhaps "Is breaking have (x) := ... OK given that there are many easy workarounds?" (This breakage is for the case of a single typeless explicit binder in an anaphoric let/have only.)

[Kyle Miller]

I considered another solution where there could be special support looking for specifically the case have (ctor) := ... where ctor resolves to a constructor, then reinterpreting it as a pattern. However, I'm very uncomfortable with these sorts of reinterpretations, since it can make for brittle macros (in this case, a macro that thinks it's making an anaphoric have, and in fact the Syntax shows it thinks its making an anaphoric have, would sometimes result in a pattern match have if the user supplies the macro a length-one binder list with a binder of the form (ctor). Not great!)

[Yaël Dillies]

Hmm... I use have (x) := ... a huge lot, but maybe switching to have this (x) := ... is fine

[Kyle Miller]

Thanks for the feedback. Other alternatives include have this x := ... and have (x : _) := ....

(I might try to make a code action to propose one of these when x isn't a constructor.)

[Ruben Van de Velde]

I think I've used it, but wouldn't mind losing it if I get rfl patterns instead

[Marcus Rossel]

I wasn't aware that anaphoric have could bind variables and find it looks super strange. So I guess we have all opinions covered :sweat_smile:

[Kevin Buzzard]

+1 for "let and have should behave in the same way" for sure, this has confused me several times in the past

[Mario Carneiro]

I would rather have let (x) := than let rfl :=, if I had to choose between them. You can write things like let .rfl := if you want to make it clearly not a binder, vice versa is harder

[Mario Carneiro]

You can also have the syntax be ambiguous and just reinterpret it if you parsed it the wrong way. I recall there is some example of this already in lean where have (x y) := ends up parsing x y as an application, and then it is destructured and turned back into a binder list

[Mario Carneiro]

Kyle Miller said:

(in this case, a macro that thinks it's making an anaphoric have, and in fact the Syntax shows it thinks its making an anaphoric have, would sometimes result in a pattern match have if the user supplies the macro a length-one binder list with a binder of the form (ctor). Not great!)

That would be a weird thing for a macro to do if it's not explicitly trying to break the system. You can always just put in have this in such cases.

[Kyle Miller]

Mario Carneiro said:

You can always just put in have this in such cases.

As a macro author you'd have to know that writing `(have $bs* := $v; $b) is dangerous, since when bs.size = 1 then the have elaborator would be liable to reinterpret the binder as a pattern. I don't think it's fair to say that someone who writes this syntax quotation is "explicitly trying to break the system".

[Mario Carneiro]

you can write have this $bs* in that example though

[Mario Carneiro]

it's a hygienic this anyway, you would probably want the user to be able to name the binder