leanprover-community
"∀ x < n" binders
In lean 3, you can use (x y z OP e) as a binder whenever OP is a binary operation, and it abbreviates the binder sequence (x y z : _) (H : x OP e) (H : y OP e) (H : z OP e).
example : ∀ x < 5, x < 5 := λ x H, H
Lean 4 doesn't have a general mechanism for infix notations, so these have to be added individually for every combination of binding notation and operator (i.e. ∀ x < e, p x and ∃ x < e, p x and ∃ x ∈ S, p x all need to be defined separately). It is unclear what we even want to do here for translation purposes besides simple expansion.
Some potential overlap with the "bigop" example from our macro paper https://github.com/leanprover/lean4/blob/2b451a3fed237f72da7e20f6b7062cf118114880/tests/lean/run/bigop.lean#L43-L50
Would it be possible for "binder group" to be a syntax class? Right now I think there are 3 or 4 different binder-like syntax classes in lean 4, which isn't great, and they all have more limitations than the "binders" syntax class of lean 3. I think the "index" class as in your paper needs to be defined in lean 4 core and needs to be used in forall and exists to be really useful; a user-defined index class is only helpful for new syntax added by the user.
Should they really be binders again? I thought most people agreed that in Lean 3 neither the generic desugaring nor the fact that you could use them anywhere a binder is expected was exactly optimal.
Ideally there should be some generic desugaring, a way to add new binder behavior for newly introduced binder syntax, and a way to do "double dispatch" for especially unusual combinations of binder and leader. I don't think that binder collections as a generic mechanism working anywhere binders do is a bad thing, but the generic desugaring of multiple binders is unfortunate for some binders, like exists unique, where iterating the combinator/lambda doesn't work.
To be clear, in this post I'm not necessarily advocating for binder collections as implemented in lean 3, but there are many hundreds of uses of this idiom in mathlib and even an exception in the style guide just so that people can write ∀ x > n, p x instead of ∀ x, n < x -> p x, so this is clearly a desired feature and while desugaring it during translation is an option, it's not a good one.
By the way, that is an example where in an ideal system there would be a custom binder: (x y z > e) should expand to (x y z) (_ : e < x) (_ : e < y) (_ : e < z), generically anywhere a binder can be used. That would be a rule overriding the usual binder collection behavior for other binops. Each leader then decides what to do with this binder sequence to turn it into an expression, with the generic/default behavior being to iterate foo fun $bi => for each binder bi.
Sure, I don't think anyone wants to live without QUANT x OP e, ..., so we should not lose that during translation. But I would not have implemented that specific pattern via a binder category. How many more complex (and convincing) uses of this feature are there in mathlib?
For example, these look pretty weird to me. But that might just be lack of familiarity on my side.
src/set_theory/cardinal.lean
710: suffices : ∀ (n : ℕ) (m < n), F m ≠ F n,
1205:lemma powerlt_le {c₁ c₂ c₃ : cardinal} : c₁ ^< c₂ ≤ c₃ ↔ ∀(c₄ < c₂), c₁ ^ c₄ ≤ c₃ :=
Well, we use what we have. It's somewhat limited, but useful when it can be used. There are lots of things about the lean 3 binder collection syntax I would like to change, for example you can't put a type ascription on the variables, but the general mechanism that is missing that prevents the whole feature from being implemented in mathlib is that binders are not an extensible syntax category.
By the way, I forget if I mentioned to you but when I mention multiple binder syntaxes I'm talking about the differences between the binders that are valid in forall, exists, and lambda, which seem entirely unnecessary. For example \forall x (y : Nat), True works but \exists x (y : Nat), True doesn't.
My point is that, if there is consensus this kind of binder is its own special thing and should not be mixed with other binders, then it should not be a member of a general binder category but used directly by each operator that wants to support it, i.e. something like binders <|> opBinder. Thus my question about how many other uses of this feature there are, and whether continuing to support them makes sense. If there are only a handful and no-one insists on keeping them, wouldn't it be easier to erase them before porting?
For example
\forall x (y : Nat), Trueworks but\exists x (y : Nat), Truedoesn't.
I agree this distinction doesn't make much sense, and it likely wasn't deliberate. On the other hand, I'm pretty sure it was deliberate that e.g. implicit binders cannot be used with exists, since it just doesn't make any sense. So we should refine this part of the grammar, but I don't see us using the exact same binder parser in each case.
Perhaps as a more general design criterion that Leo and I never explicitly talked about, but I think we agree on: the more extensive and extensible your grammar is, the more care should be taken in designing each grammar rule. It will be confusing enough to keep track of the many syntax variations people will introduce, so let's not make newcomers' lives even harder by providing confusing syntax combinations that don't even make sense semantically.
I agree this distinction doesn't make much sense, and it likely wasn't deliberate. On the other hand, I'm pretty sure it was deliberate that e.g. implicit binders cannot be used with exists, since it just doesn't make any sense. So we should refine this part of the grammar, but I don't see us using the exact same binder parser in each case.
I don't think this should be enforced at the parser level. That just makes everything meaninglessly more complicated. Just either error or filter out bad binder kinds during elab.
Perhaps as a more general design criterion that Leo and I never explicitly talked about, but I think we agree on: the more extensive and extensible your grammar is, the more care should be taken in designing each grammar rule. It will be confusing enough to keep track of the many syntax variations people will introduce, so let's not make newcomers' lives even harder by providing confusing syntax combinations that don't even make sense semantically.
It's not clear to me whether or not my position is compatible with this design criterion, but I value simplicity of the grammar, both literally in terms of the number of grammatical constructs, and in the user's impression of the grammar, where fewer constructs means more regularity - if a thing works in one place then it also works in all similar places. I would put implicit binders for exists in that category - just because they aren't particularly useful doesn't mean they should be a parse error, and making them such means documentation and such have to be more complicated to outline the holes that have been cut into the grammar.
My point is that, if there is consensus this kind of binder is its own special thing and should not be mixed with other binders, then it should not be a member of a general binder category but used directly by each operator that wants to support it, i.e. something like binders <|> opBinder.
I'm not sure what is what in your example. I agree that some contexts want to be able to support more kinds of binders than the usual, for example fun might accept either binder or term where binder is an extensible syntax category for binder groups. But I don't see how you imagine it would be possible to retrofit opBinder into all the locations binders are accepted, if this is done outside the core, without overriding literally every command in lean.
Thus my question about how many other uses of this feature there are, and whether continuing to support them makes sense. If there are only a handful and no-one insists on keeping them, wouldn't it be easier to erase them before porting?
I'm looking forward here, not at the port itself. It's certainly possible to erase them during porting, and indeed I'm doing this at the moment, but in the far future when mathlib is all in lean 4, I don't want to have to settle for a worse syntax than what lean 3 offers. That doesn't mean copying what lean 3 is doing, but it does mean doing something approximately equivalent. There are plenty of current uses of this idiom (your list is far from complete, although I don't think you were going for that) that indicate that something approximately like the feature is desirable.
I don't think this should be enforced at the parser level. That just makes everything meaninglessly more complicated. Just either error or filter out bad binder kinds during elab.
Well, I don't necessarily disagree. But not something for me to decide either, I didn't even write those parts of the grammar :) .
But I don't see how you imagine it would be possible to retrofit
opBinderinto all the locations binders are accepted, if this is done outside the core, without overriding literally every command in lean.
Same discussion as above I suppose, but surely we don't need support for this kind of binder in "literally every command" of core, but, like, two (four with Sigma/PSigma)? Since opBinder should not overlap with any core binder syntax, redeclaring core syntax with it should just work.
There are plenty of current uses of this idiom (your list is far from complete, although I don't think you were going for that) that indicate that something approximately like the feature is desirable.
Let me rephrase my question: how many uses of this idiom that are not of the form QUANT x OP e that we all agree on are there in mathlib, ? With the query ∀[^,]*< I found the above and ∀ (i<n) (j<n) and I can't say I'm convinced... that's not even shorter than two quantifiers.
Same discussion as above I suppose, but surely we don't need support for this kind of binder in "literally every command" of core, but, like, two (four with Sigma/PSigma)? Since opBinder should not overlap with any core binder syntax, redeclaring core syntax with it should just work.
I mean, if you want to use this in binders for def, you will have to override the def command; if you want it in instance you will need to override that too, and so on. It's a game of whackamole with all possible occurrences of the production in the grammar - almost all commands transitively depend on the binder production except for trivial commands like namespace.
Let me rephrase my question: how many uses of this idiom that are not of the form
QUANT x OP ethat we all agree on are there in mathlib, ? With the query∀[^,]*<I found the above and∀ (i<n) (j<n)and I can't say I'm convinced... that's not even shorter than two quantifiers.
Other common binops used in that position include <=, > and \in. I will be able to answer this question more definitively soon, when mathport gets to the point that we can run it on all of mathlib with a minimum of errors, and then it will be possible to instrument the parser to just see how commonly the Binder.collection variant is used.
But I don't really want to be in the business of arbitrating whether this is a good syntax. It seems reasonable to a mathematician and that's reason enough for me; personally I would go with far less fancy syntax but my current goal is to respect the choices of mathlib users, not impose my own design sense on everyone else.