Set intervals names

Stream: maths

[Yaël Dillies]

What do people think of renaming docs#set.interval and docs#set.interval_oc to set.uIcc and set.uIco, with the u standing for "unordered"? This would:

• fix the unanimously bad name interval_oc
• make set.interval look closer to docs#set.Icc than it currently is
• shorten the names
• match the naming convention I introduced (a while back!) with docs#set.cIcc
• make clear that we don't have the Ioc and Ioo versions (which would then be called uIoc, uIoo
• avoid confusion with docs#interval

[Yaël Dillies]

The one downside I see so far is that uIcc is a more obscure name than interval, but

• interval could (and indeed does) refer to many similar concepts
• the Ixx naming convention is already well-implemented.

[Yaël Dillies]

This is relevant to the mathlib4 port: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20clarification/near/315915143 and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60interval_oc.60.20naming.20scheme

[Kevin Buzzard]

What's wrong with just set.Icc etc?

[Reid Barton]

set.interval isn't set.Icc

[Ruben Van de Velde]

It's [min a b, max a b], yes?

[Kevin Buzzard]

Why?

[Kevin Buzzard]

Maybe that's the wrong question. Maybe the question is why what we have is called an interval at all? Is this standard terminology?

[Kevin Buzzard]

I think Yael's convention sounds great, an incomprehensible name for an incomprehensible construction sounds perfect.

[Kevin Buzzard]

I'd also vote for changing the docstring of set.interval_oc to something which actually describes the object being defined

[Reid Barton]

I think "incomprehensible" is a bit too far but in general I agree it looks like a good change.

[Kevin Buzzard]

So you're happy that {2} and {1,2,3} are in the interval between {1,2} and {2,3}, given the description "interval a b is the set of elements lying between a and b, with a and b included"?

[Kevin Buzzard]

Surely "the set of elements lying between a and b" is {x : a<=x<=b}?

[Reid Barton]

I mean this is just too much generality gone awry

[Reid Barton]

It's clearly a sensible construction in the case of, say, the real numbers

[Kevin Buzzard]

Anyway, to answer the question I am definitely for the change :-)

[Kevin Buzzard]

Oh I see, the point is that it allows us to talk about the interval from 10 to 1. It could still have been the union of [a,b] and [b,a] but whatever.

[Kevin Buzzard]

For linear orders these agree and you can argue that everything else is a junk value

[Yaël Dillies]

Reid Barton said:

I mean this is just too much generality gone awry

Well in fact I very recently generalised set.interval to lattices because I need this generality for a combinatorial inequality :sweat_smile: but it has nothing to do with the current discussion.

[Pedro Sánchez Terraf]

Kevin Buzzard said:

So you're happy that {2} and {1,2,3} are in the interval between {1,2} and {2,3}, given the description "interval a b is the set of elements lying between a and b, with a and b included"?

Even from the (order) lattice-theoretic point of view I share this concern. The name interval for this construct is misleading. It is more like a “hull” (actually being the sublattice generated by those two elements).

[Yaël Dillies]

The world \ {me} only cares about the linear order case, so this is a deliberate lie from the docstring.

[Yaël Dillies]

#18104 (it will probably be a while before it builds)

[David Loeffler]

The build is broken for #18104 (looks like a search-and-replace over the library caught something it shouldn't).

[David Loeffler]

Incidentally, this change will break basically any pre-existing code that uses definite integrals (e.g. my Riemann zeta function project), all for a purely aesthetic gain. Whatever happened to "if it ain't broke don't fix it"?

[Yaël Dillies]

My thought is that it shouldn't break so much because we have notation for it. Are you really not using the [a, b] notation?

[Johan Commelin]

You are also change a bunch of lemma names, right?

[Yaël Dillies]

Yes, that is unavoidable if we want to keep consistency :sad:

[Johan Commelin]

Sure, but it means that using the notation isn't going to avoid breakage.

[Johan Commelin]

I'm really looking forward to using alias + deprecated for these kind of situations, once we've moved to Lean 4.

[Yaël Dillies]

Most of the existing code around interval integrals only uses the notation, thankfully.

[Yaël Dillies]

But yeah whatever is not in mathlib is hardly ever considered when mathlib moves on, which is why if you want to reduce your maintenance burden you should PR your code to mathlib.

[David Loeffler]

There was a thread recently about differences between mathlib and one of its rivals (Coq?), in which some people tried to argue against the claim that mathlib had a casual approach to backward-compatibility issues. I think this thread here demonstrates that casual attitude rather neatly.

[Alex J. Best]

I'm not sure how one would argue mathlib respects backwards compatibility! It definitely doesn't of course, most people here seem to consider the fact we readily revise previous work that isn't sufficient for some reason as a good thing. Maybe they tried to argue it doesn't matter for some reason (all dependents fix a version)?
There are definitely a lot more things we can do to at least help people switch mathlib versions more easily (https://mathlib-changelog.org/ is a good start), but currently adjusting mathlib induced breakage is still quite manual process.

[Eric Wieser]

David Loeffler said:

some people tried to argue against the claim that mathlib had a casual approach to backward-compatibility issues.

From my perspective, it's not that our approach is casual; it's that as a community, we have made a deliberate choice that backwards compatibility (in a software sense) is a non-goal.

I think we still try to remain mathematically backwards-compatible; a mathematical idea usually doesn't disappear from mathlib entirely.

[Yaël Dillies]

In particular, name changes are not backward-compatible, but in a trivial way. Once you've replaced the modified names, you're guaranteed that your work will still compile.

[Eric Wieser]

Well, unless the statement changes too. Your comments amounts to "changes are incompatible in name only, except when they're not"

[Yaël Dillies]

What I mean is that there's no work trying to fit new definitions.

[Eric Wieser]

Yaël Dillies said:

What do people think of renaming docs#set.interval and docs#set.interval_oc to set.uIcc and set.uIco, with the u standing for "unordered"?

This thread took multiple tangents above, and I think to some extent the question of naming got lost. #18104, which performs this rename, is now passing CI. Were people generally happy with the new names?

[David Loeffler]

If there has to be a new name, then this seems a good choice.

[Eric Wieser]

Pinging the people who approved/contributed the old names @Sebastien Gouezel and @Yury G. Kudryashov (interval in #1949), @Patrick Massot (interval_oc in #7864); are you happy with these new names?

[Sebastien Gouezel]

Yes, I think the new names are better.

[Patrick Massot]

Yes, I already wrote somewhere that I'm ok with the renaming.

[Eric Wieser]