Lean 4's new proof syntax (a beginner's perspective)

Stream: new members

[Hungry Applicative]

In my limited time with lean it seems that the new Lean 4 has a much more unpleasant syntax for writing structured proofs. In Lean 3 you seem to have at least the following:

• assume h: p, t
• have h: p, from s, t
• suffices h: p, from s, t
• show p, from t

So far I have identified the following equivalents for lean 4:

• fun h: p => t
• have h: p := s; t
• suffices h: p from s; t
• show p from t

Is it just me or are these constructs more inconsistent? The Lean 3 syntax seems much more readable and many of the constructs even have much nicer shorthands (e.g. omitting the colon in have : p from s). Does anyone know the reason for this change? Is it just temporary?

[Horatiu Cheval]

I actually think Lean4 is the cleaner version, with its move away from all the commas from Lean3 (note that you don't have to write the ; if you write t on a new line)

[Horatiu Cheval]

Also, with Lean4's flexible syntax you can maybe recover stuff you miss from Lean3. For instance, if you want assume you could do something like

macro "assume" var:bracketedBinder exp:term : term => `(fun $var => $exp)

theorem f : True → True :=
  assume (h : True)
  h

(poorly written, I don't know how to write macros. For instance, could anoyne show how to have the parentheses around h : True be optional, what to replace bracketedBinder with?)

[Hungry Applicative]

This is what I have been thinking, but I am a bit hesitant about creating custom notation for my own uses because it alienates me/my code from the rest of the community. I'm worried that if everyone invents their own notation for things like this it makes it harder to collaborate. I am saying this as a complete beginner, but I believe it is better to have common notational conventions like this be a part of the standard library. Unless of course, this sort of notation is now less popular?

[Horatiu Cheval]

I agree with that. Though with Lean you kind of have two standard libraries, core Lean and mathlib, and it might be possible for mathlib to add in the future notations beyond core Lean. For example I see Mathlib4 adds a "lemma" command as an alias for "theorem" since "lemma" is gone in Lean4, so maybe we'll have some more notations like the ones you mentioned once mathlib is ported (but commas probably won't make a reappearance).

[Horatiu Cheval]

And about popularity I don't know, I always preferred \lambda x, ... and have x := ... anyway to the other versions in Lean3 :) But I believehave, from is quite frequent in mathlib

[Patrick Massot]

Very clearly all the nice ways to write proofs are meant to go in mathlib. You're not expected to be happy writing non trivial proofs using only core Lean. So indeed there will be lots of macros and consistency will be ensured by using mathlib.