segments in a vector space notation

Stream: general

[Kim Morrison]

Mathlib.Analysis.Convex.Segment introduces notation:

@[inherit_doc] scoped[Convex] notation (priority := high) "[" x "-[" 𝕜 "]" y "]" => segment 𝕜 x y

Can I propose that we don't ever add notations that interfere with List notation, and in particular that someone replaces this notation with something else (or removes it: I think this would be much clearer with no notation)?

[Kim Morrison]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Help.20with.20.60nightly-testing.60/near/426041257 for an example of the resulting pain. :-)

[Yaël Dillies]

Scott Morrison said:

The notation here seems insane. Is it really [X -[k] Y]?

Uh, yeah, that's an affine segment

[Yaël Dillies]

What's so bad with that notation?

[Yaël Dillies]

I introduced that notation precisely because it was the closest to segment notation that didn't interfere with list notation. Did that change recently?

[Johan Commelin]

@Scott Morrison Does this mean that notation for linear maps is also bad? Because that attaches [R] to an arrow, to indicate that the map is R-linear.

[Eric Wieser]

I don't feel as strongly about it as it sounds like Scott does, but it's weird that we have a notation for it but not Icc

[Eric Wieser]

(presumably we rejected any ideas for such a notation using the same reasoning behind Scott's distaste of the affine segment notation)

[Yaël Dillies]

We do have a notation for Icc actually. It's [x, y] for Icc x y. But it's local/localised I believe.

[Notification Bot]

5 messages were moved here from #general > Help with nightly-testing by Yaël Dillies.

[Johan Commelin]

Potential notation for Ixx that semi-conflicts with list notation: https://proofwiki.org/wiki/Definition:Real_Interval/Notation/Wirth

• (a .. b) := Ioo a b
• (a .. b] := Ioc a b
• [a .. b) := Ico a b
• [a .. b] := Icc a b

And the unbounded versions can easily be added by using $\infty$ (as notation, not the term) for one of a or b.

[Johan Commelin]

Maybe this can also be adapted for segments?

[Johan Commelin]

But if I understand @Scott Morrison then anything involving [] is off limits. It would be good to know a general guideline.

[Yaël Dillies]

Something like this?

• [a ..[𝕜] b] := segment 𝕜 a b
• (a ..[𝕜] b) := openSegment 𝕜 a b

[Eric Wieser]

I think (a .. b] is likely off limits too because of IDEs using dumb bracket matching

[Eric Wieser]

Unless we ask people to always write (a .. /-)[-/ b]

[Kim Morrison]

I mean, I don't want to insist it is not allowed. Maybe the recent failure on nightly-testing (that required adding a type ascription) was actually unrelated to the notation?

[Kim Morrison]

I don't really understand how [X -[k] Y] is meant to be an improvement over segment k X Y. To me, it feels strictly worse. (Not immediately obvious what it means, doesn't show me the key word, and potentially has weird interactions with List.)

[Patrick Massot]

To be honest the really crazy part is reserving [ and ] for lists in a proof assistant. It should be a scoped notations that needs to be opened when programming or proving stuff about lists.

[Eric Wieser]

Is it even reserved? My impression was that there wasn't actually a clash with list in the first place, only potential for one

[Kevin Buzzard]

Patrick said the thing I wrote, thought about, and deleted, but I do believe it. My only concern about removing list notation is that I'm then not entirely sure whether I'll be able to rw anything. But lists do not come up in most of the mathematics I do, other than secretly powering things like finite sets behind the scenes.

[Eric Wieser]

Scott Morrison said:

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Help.20with.20.60nightly-testing.60/near/426041257 for an example of the resulting pain. :-)

I looked at this, and the pain is nothing to do with the notation. So I don't think there are any technical issues with the notation sharing []s with List; the issues exists only in the minds of the humans who mentally reserve [] for lists / non-lists.

[Kim Morrison]

Scott Morrison said:

I don't really understand how [X -[k] Y] is meant to be an improvement over segment k X Y. To me, it feels strictly worse. (Not immediately obvious what it means, doesn't show me the key word, and potentially has weird interactions with List.)

Leaving aside the "potential weird interactions with List" point, as I agree that's incorrect, how do others feel about my remaining claim that [X -[k] Y] is strictly worse than segment k X Y?