notation for intervals

Stream: mathlib4

[Floris van Doorn]

I think we should introduce notation for intervals. The Ixx abbreviations are very cryptic for newcomers.
How about this notation?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Int.Interval
import Mathlib.Order.Interval.Finset.Nat


notation "{" a:51 " < " "·" " < " b:51 "}" => Set.Ioo a b
notation "{" a:51 " ≤ " "·" " < " b:51 "}" => Set.Ico a b
notation "{" a:51 " < " "·" " ≤ " b:51 "}" => Set.Ioc a b
notation "{" a:51 " ≤ " "·" " ≤ " b:51 "}" => Set.Icc a b
notation "{" a:51 " < " "·" "}" => Set.Ioi a
notation "{" a:51 " ≤ " "·" "}" => Set.Ici a
notation "{" "·" " < " b:51 "}" => Set.Iio b
notation "{" "·" " ≤ " b:51 "}" => Set.Iic b

-- all the following notations work
#check {(1 : ℝ) ≤ · < 2}
#check {1 < · < 3}
#check {(3 : ℤ) < · ≤ 4}
#check {5 ≤ · ≤ 6}
#check {(1 : ℝ) ≤ · }
#check {· < 3}
#check {(3 : ℤ) < · }
#check { · ≤ (6 : ℝ)}
#check { x : ℝ | x ^ 2 > 2 }
#check { n ∈ {1 < · < 10} | n ≠ 5 }
#check ({1 ≤ · < 2} : Set ℝ)

Todo: make sure that it elaborates as Finset if the expected type is known.
Note: Of course we'll keep Ixx in theorem names about intervals.

[Floris van Doorn]

(thanks to @Kyle Miller for figuring out that this notation works.)

[Eric Wieser]

I'm tempted to say that this notation is slightly too weird, and we should make {x | 0 ≤ x < n} work instead

[Eric Wieser]

(or make . work in all set notation)

[Kyle Miller]

Eric Wieser said:

(or make . work in all set notation)

This would involve collaboration with core, to add the ability to configure which notations cdot expansion can't see through. It would make the rule "cdot expansion just can see through parentheses" more complicated.

[Kyle Miller]

Eric Wieser said:

I'm tempted to say that this notation is slightly too weird, and we should make {x | 0 ≤ x < n} work instead

This is tempting, but it's fairly brittle since I believe we want to make sure these give the Set.Ixx functions (I'm not completely clear on why though).

I do want to see inequality chain support at some point!

[Yury G. Kudryashov]

One downside of having notation with ≤ that outputs Set.Ixx behind the scene is that {0 ≤ · ≤ c} doesn't simplify if we have a lemma about _ ≤ c (e.g., c is min a b or some indexed infimum).

[Yury G. Kudryashov]

BTW, should we use lowercase I instead of uppercase?

[Yury G. Kudryashov]

And if we drop defs, then it will simplify, and we may have issues with confluence.

[Johan Commelin]

There is also https://proofwiki.org/wiki/Definition:Real_Interval/Notation/Wirth
But maybe unbalanced parens are just too evil?

[Tomas Skrivan]

Johan Commelin said:

There is also https://proofwiki.org/wiki/Definition:Real_Interval/Notation/Wirth
But maybe unbalanced parens are just too evil?

I would love to have this. I did some experiments some time ago but it completely broke syntax highlighting in Emacs :(

[Yaël Dillies]

I recently added similar notation for (Finset.Ixx ..).filter _ and it has greatly improved the readability, so I'm all in favour of it!

[Violeta Hernández]

I like this idea. I'd prefer something more traditional like (x, y), [x, y), (-∞, x), etc. but I completely understand that would bring tons of ambiguity and syntax highlighting issues.

[Martin Dvořák]

Well [x, y) is heresy.

[Violeta Hernández]

It's what I've been using my whole life!

[Violeta Hernández]

I'll reluctantly accept French notation )x, y) too.

[Violeta Hernández]

But yeah, that's subject to the same problems.

[Yaël Dillies]

Violeta Hernández said:

I'll reluctantly accept French notation )x, y) too.

I'm not sure where you got that from. In France, your [x, y) is written [x, y[

[Violeta Hernández]

oh yeah that

[Violeta Hernández]

guess I just inadvertently came up with inverse French notation :stuck_out_tongue:

[Vincent Beffara]

Would ［a, b］ work? (with "fullwidth brackets" that are separate unicode characters). It would not be the only place where we get similar looking characters meaning different things. (Although if the aim is to be more beginner-friendly it might not work and be more misleading than anything else.)

[Vincent Beffara]

Actually, ⟦ ⟧ is used already for quotients but it has the right mathematical meaning in informal texts, it might be an option to say ⟦a, b⟧.

[Patrick Massot]

The only notations that make sense here are the French ones. The idea of having $(a, b)$ mean both the pair and the interval is really one of the worst mathematical notation clash ever invented.

[Joachim Breitner]

You must be joking. It can’t be worse than the malice behind the introduction of the Legendre symbol.

[Edward van de Meent]

the french notation doesn't make sense either, non-matching brackets are evil too.

[Kevin Buzzard]

non-matching brackets have only become evil with the advent of computers. I'm not entirely sure that Bourbaki were too worried about messing up syntax highlighting in emacs. I have always loathed the Legendre symbol notation and I've lectured it many times -- it's clearly a fraction in a bracket!

[Moritz Firsching]

some people use (a, b) to denote the greatest common divisor

[Joachim Breitner]

This syntax is itself a great divisor, it seems! Very divisive.

[Ruben Van de Velde]

Clearly notation was a mistake and we should go back to writing everything out in Latin

[Joachim Breitner]

Like in Rocq? (Clear you must be referring to the character set Latin-1)

[Patrick Massot]

Edward, the issue is that we want notation for a mathematical reality were both ends do not match. This has nothing to do with notation. The interval $\left[a, b\right[$ contains $a$ but does not contain $b$, there is nothing you can do about that.

[Patrick Massot]

And the inverted bracket very nicely convey the corresponding geometric idea. Of course $\left(a, b\right($ would also work for this, but the clash with pairs remains.

[Filippo A. E. Nuccio]

Martin Dvořák said:

Well [x, y) is heresy.

Why?

[Filippo A. E. Nuccio]

All in all, I find that Ixx is perhaps a bit hard to newcomers (although it is pretty well documented, and after a moment thought very much understandable), but creates no clash, no typographical conflict and no meta-mathematical debate. I would honestly opt to keep it as it is...

[Antoine Chambert-Loir]

Kevin Buzzard said:

non-matching brackets have only become evil with the advent of computers. I'm not entirely sure that Bourbaki were too worried about messing up syntax highlighting in emacs.

Note that Bourbaki uses bizarre bracket symbols for intervals.
image.png

Note also the special notation for illimited intervals on the left or on the right
image.png

[Violeta Hernández]

Filippo A. E. Nuccio said:

All in all, I find that Ixx is perhaps a bit hard to newcomers (although it is pretty well documented, and after a moment thought very much understandable), but creates no clash, no typographical conflict and no meta-mathematical debate. I would honestly opt to keep it as it is...

Yeah, I think this might be one of those cases where "there's five different solutions with differing benefits and tradeoffs, so we don't try and solve it at all"

[Violeta Hernández]

Something I like about Ixx is how compact the notation is. Three letters and you can immediately tell what kind of interval you're talking about, compared to the new suggested notation which takes a bit more time to parse, and isn't so obviously exhaustive.

[Eric Wieser]

If we're worried about confusion for newcomers with the status quo, I think we can get an easy win by putting $[a, b)$ or $[a, b[$ or $a ≤ · < b$ in the docstring of docs#Set.Ico.

[Filippo A. E. Nuccio]

#17523

[Sebastian Ullrich]

There was also lean#1962

[Kyle Miller]

Floris pointed out this thread from #general > New range syntax in lean 4.22 @ 💬

I like Floris's original proposal, to use {5 ≤ · ≤ 6} with the dot. If it's part of the notation, it's unambiguous. There's ambiguity with ({· ≤ 6}), but using (priority := high) on the notation seems to solve it. (This isn't just a hypothetical issue. It would affect intervals appearing anywhere inside parentheses.)

In that thread, @Arthur Paulino suggested {1 < ⋯} as an alternative. I like this too — cdots are a nice idea, and it looks more like common practice math notation. The single · looks more like Lean, for better or for worse.

[Kim Morrison]

I much prefer ⋯, using the pure lambda dot would drive me insane. It might be unambiguous to the Lean parser, but not mine.

[Floris van Doorn]

I'm also very happy with using ⋯.

[Floris van Doorn]

/poll What notation should we use for intervals in Mathlib?
{5 ≤ · < 6}
{5 ≤ ⋯ < 6}
No notation
I want notation, but not these suggestions

[Floris van Doorn]

Feel free to add other options!
(If you want that (a, b) or [a, b] should be interpreted as intervals, a MWE showing that it doesn't clash badly with pairs or list should be given.)

[Arthur Paulino]

Kyle Miller said:

In that thread, Arthur Paulino suggested {1 < ⋯} as an alternative. I like this too — cdots are a nice idea, and it looks more like common practice math notation. The single · looks more like Lean, for better or for worse.

To clarify, I was iterating on François' idea:
François G. Dorais said:

It would be nice to have … (U+2026) as an alternative.

Though I wouldn't say that · looks more like Lean. I think both look like Lean just the same because both make good use of unicode that Lean ergonomically supports. It's just that we're more accustomed with · because it's part of already existing syntax.

[Kim Morrison]

I want to keep pushing against ·:

• it's potential confusing to the Lean parser, disambiguating with the pure lambda notation
• it's potential confusing to the human parsers, ditto
• it's further from paper notation than ⋯

[Eric Wieser]

Regarding parser confusion, the rule could change from "· is associated with the next set of () parentheses" to "· is associated with the next set of () or {} delimiters"

[Eric Wieser]

(Note that this is already confusing in the face of notation like C(X, Y), where · doesn't behave as the ()s would imply)

[Kim Morrison]

But, but, but, that's the possibility of doing something where the · is confusing, rather than insisting that people use it in a confusing way!

[Eric Wieser]

Right, I parenthesized that because it's not that relevant an argument

[Yaël Dillies]

Eric Wieser said:

the rule could change from "· is associated with the next set of () parentheses" to "· is associated with the next set of () or {} delimiters"

Then we would lose ({ foo with bar := · })

[Eric Wieser]

fun bar => { foo with bar } isn't a terrible replacement

[Eric Wieser]

But yes, this would be a breaking change - we already knew that, because ({· < 6}) is already something else.

[Violeta Hernández]

Whatever happened to keeping Ixx? Is that completely out of the table?

[Kyle Miller]

My interpretation of any notation proposal would be that the Ixx definitions would stay.

There at least a few potential implementations of the proposal however:

1. It could be a notation only for Set.
2. Both Set and Finset could have scoped notations for it.
3. The interval syntaxes could have an elaborator that tries to select whether it's a Set or a Finset depending on the expected type, defaulting to Set.
4. There could be Ixx classes with a Set default instance. The notation targets these classes. Mathlib is refactored to be in terms of these Ixx classes.

[Alex Meiburg]

I generally like ⋯ in the notation, but it's something that for me is so associated to "hidden proof terms" that if I saw it in an info view I would instinctively parse it as "there's some other expression here that's not being shown". I think the low ellipsis … would be better then, it also looks much more reminiscent of the a .. b range syntax that is in several languages (e.g. Haskell), and also the v4.22 range syntax.

[Floris van Doorn]

I think there is overwhelming support to change the interval notation to {5 ≤ ⋯ < 6}
If someone that thinks we should use … instead wants to make a poll to decide between ⋯/…, please go ahead. I personally prefer to use middle dots between relation symbols.

[Johan Commelin]

/poll cdots vs ldots

• cdots
• ldots
• wut? I don't care

[Violeta Hernández]

Floris van Doorn said:

I think there is overwhelming support to change the interval notation to {5 ≤ ⋯ < 6}

Has this been discussed elsewhere? I still feel completely blindsided by this. I think the Ixx system was very elegant and avoided precisely this kind of bikeshedding.

What will happen with theorem names? Will we keep using Ixx in them, or are we going to mass rename them into something else (presumably much longer)?

[Jovan Gerbscheid]

The Ixx theorem names are staying the same.

[Ruben Van de Velde]

I don't mind Ixx, but if we do change, I like {5 ≤ ⋯ < 6}

[Aaron Liu]

I don't like {5 ≤ ⋯ < 6} because that's {5 \le \... < 6} which is 16 chars to type (mostly special characters) while Set.Ico 5 6 is only 11 (mostly letters) and Ico 5 6 is only 7 (mostly letters)

[Ruben Van de Velde]

How about if we add a keyboard shortcut \Ico?

[Aaron Liu]

if you can get it to put my cursor in the right spots then I'd be more supportive

[Robin Arnez]

You can always "Ico": "{$CURSOR ≤ ⋯ < }" but I don't think you can get it to also put you into the second spot without manually moving your cursor there.

[Robin Arnez]

alternatively, you could have "Ico": "≤ ⋯ <", so you only need to type {a \Ico b} but idk

[Damiano Testa]

VSCode does give you the option of placing several "default" positions for the cursor and you move between them with Tab.

[Damiano Testa]

So you could have "Ico": "{$0 ≤ ⋯ < $1}$2" (or something similar) and you could go through them.

[Robin Arnez]

Yeah I suppose we'd need support for that in the VS code extension though

[Damiano Testa]

Editing the vscode settings already has support for this.

[Robin Arnez]

I mean, if you add "Ico": "{$CURSOR ≤ ⋯ < $CURSOR}$CURSOR", you get { ≤ ⋯ < $CURSOR}$CURSOR currently

[Damiano Testa]

Having just added

    "ICO template": {
        "scope": "lean4",
        "prefix": "Ico",
        "body": [
            "{$1 ≤ ⋯ < $2}$3",
        ],
        "description": "Print a template for an interval"
    }

to my snippets file, I typed

Ico[Tab]a[Tab]b[Tab]c

and I obtained

{a ≤ ⋯ < b}c

[Damiano Testa]

So, I agree that it would be good if the extension did this automatically, but you can achieve the same effect without support from the extension.

[Julian Berman]

(deleted, that was an old draft message...)