Nested binders without annotations

Stream: mathlib4

[Yaël Dillies]

I just hit a (Lean 4? Std?) regression in the way nested binders are handled. All examples work in Lean3.

def myPred  : ℕ → Prop := sorry

example : ∃ a (h : myPred a), True := sorry -- expected ',' or binderPred
example : ∃ (a) (h : myPred a), True := sorry -- expected ',' or binderPred
example : ∃ a, ∃ h : myPred a, True := sorry -- works
example : ∃ (a : _) (h : myPred a), True := sorry -- works

[Yaël Dillies]

(I'm happy for this thread to be moved to #lean4 if this is a Lean 4 issue. I must say it's hard to know which library does what precisely these days)

[Kyle Miller]

Here's a tip for how to figure out who might be responsible for what notation: right click a salient part of the notation and do "Go to Declaration" in VS Code. For the working multiple-binders exists notation, that leads to this line of Init.NotationExtra, so it turns out to be Lean 4.

That syntax definition says that what comes after ∃ is an explicitBinders, and going to definition we can see this:

syntax unbracketedExplicitBinders := (ppSpace binderIdent)+ (" : " term)?
syntax bracketedExplicitBinders   := "(" withoutPosition((binderIdent ppSpace)+ ": " term) ")"
syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unbracketedExplicitBinders

Simplified,

syntax unbracketedExplicitBinders := binderIdent+ (" : " term)?
syntax bracketedExplicitBinders   := "(" binderIdent+ ": " term ")"
syntax explicitBinders            := bracketedExplicitBinders+ <|> unbracketedExplicitBinders

So, it doesn't allow mixing bracketed binders and unbracketed binders. And furthermore, it doesn't allow ∃ (a) (h : myPred a), True, which might have been a convenient shorthand for ∃ (a : _) (h : myPred a), True.

Mixing bracketed and unbracketed binders is probably not allowed because there is a parsing issue: when you're parsing ∃ a b c : X, True you don't know if you should only have unbracketed binders until you get to the :. However, fun notation allows mixed binders, so it's not impossible.

[Yaël Dillies]

Good point. I actually tried ∃ (a) (h : myPred a), True but decided it wasn't relevant.

[Kyle Miller]

We can Go To Declaration on fun too to see how it's syntax works. Here are the relevant definitions, simplified and using syntax notation.

syntax funBinder := funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> term:max
syntax basicFun := funBinder+ (":" term)? " =>" term
syntax «fun» := "fun" (basicFun <|> matchAlts)

So, the way it works is that it parses a sequence of binders (or terms!) and then optionally a : type. It's then up to the fun elaborator to mak sure that if : type is present then the only things preceding it are identifiers.

[Kyle Miller]

(I've been thinking of these things anyway because I've been wanting to make the binders that appear in notations defined by mathlib's notation3 command to be more flexible. It'd be nice to use this fun setup there I think, along with our extended binders.)

[Yaël Dillies]

It's annoying that this syntax is defined in core Lean. It seems that the bar for PRs there got much higher recently :half_frown:

[Kyle Miller]

Exists could be more flexible with

syntax bracketedExplicitBinders   := "(" binderIdent+ ": " term ")"
syntax explicitBinders := (bracketedExplicitBinders <|> binderIdent)+ (":" term)?

[Kyle Miller]

I just thought to compare it with forall, and this turns out to be essentially its binder syntax:

syntax «forall» := "∀" (binderIdent <|> bracketedBinder)+ (":" term)? ", " term

though bracketedBinder supports other types of binders too.

[Kyle Miller]

For a Lean PR, we'd need an RFC, and there are a number of points we need to cover link

For impact to code, explicitBinders only used for a few notations in Lean 4, it's never mentioned by name in Std4 (though it likely needs patching), and Mathlib uses it once for ∃!. Std4 mentions that it'd be nice to upstream letting bracketedExplicitBinders have an optional type, though that would impact (x : X) × Y x sigma notation (you don't want (X) × Y to mean (X : _) × Y!).

[Kyle Miller]

(I'll just mention that we can let mathlib have our own exists notation entirely since we can set a high-priority parse. I'd rather not go down this route for mathlib, but at least it's something you could have in your own projects.)

[Kevin Buzzard]

Yaël Dillies said:

It's annoying that this syntax is defined in core Lean. It seems that the bar for PRs there got much higher recently :half_frown:

My understanding from Leo was that Lean 4 was designed with so much flexibility in mind that if you don't like something then you can change it without having to make PRs to core Lean. Would that principle apply here? (oh maybe that's what Kyle is saying above?)

[Yaël Dillies]

He did say that, but he also said that he wished for fragmentation not to happen (at least between Core and Std, don't know how much that applies to mathlib).

[Kyle Miller]

Yeah, I'm saying it's flexible enough that we can override it in mathlib, but I think for Exists it would be much better if it were just made to be more consistent with other notations (like forall and fun).

If we're careful about making our new notations be extensions of pre-existing notations, then it's not so bad, but if you're not careful you can end up with libraries with mutually unintelligible dialects of Lean.

Syntax extension is fun but it's dangerous for large projects. Luckily mathlib is for mathematicians, who are used to needing to learn new notations (and maybe enjoy it?). Software engineers tend to be much more wary of these sorts of features.

[Kyle Miller]

I'm very thankful for "Go to Declaration" for custom (and core!) syntax, which makes dealing with this feature (and learning Lean 4) so much more manageable.

[Yaël Dillies]

Kyle, I assume you already know ⨆ i j, f i j currently doesn't parse?

[Kyle Miller]

@Yaël Dillies Turns out this is all that's needed to get Exists work with your test cases and also with destructuring.

import Lean

namespace MyExists
open Lean Parser

syntax (name := myExists) (priority := high)
  "∃" (ppSpace term:max)+ Term.optType ", " term : term

macro_rules
  | `(∃ $[$bs]* $[: $ty?]?, $e) => show MacroM Term from
    bs.foldrM (init := e) (fun b e => `(Exists fun $b $[: $ty?]? => $e))

end MyExists

def myPred : Nat → Prop := sorry

example : ∃ a (h : myPred a), True := sorry
example : ∃ (a) (h : myPred a), True := sorry
example : ∃ a, ∃ h : myPred a, True := sorry
example : ∃ (a : _) (h : myPred a), True := sorry
example : ∃ x y : Nat, x = y := sorry
example : ∃ ((x, y) : Nat × Nat), x + 1 = y := sorry

example : ∃ x (y : Nat) : Int, x = y := sorry -- unexpected type ascription

[Kyle Miller]

(Yeah, I think I knew about ⨆ i j, f i j. You should be able to write ⨆ (i) (j), f i j as a workaround.)

[Mario Carneiro]

I can confirm that it is incredibly annoying that the syntax of fun, forall and exists is not consistent. This made mathport have some very annoying code to convert between them

[Kevin Buzzard]

So this is a core lean issue?

[Mario Carneiro]

yes, this is inconsistency of the lean grammar