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