Notation for AntisymmRel

Stream: mathlib4

[Violeta Hernández]

I opened #19554 to define ⋚ as notation for AntisymmRel (· ≤ ·) (a ≤ b ∧ b ≤ a). There was considerable pushback to this, mostly because of the possibility that this symbol could be misread as a "comparability" relation (a ≤ b ∨ b ≤ a). I then brought up an idea from the Xena Discord to use ≗ (read as order-equivalent), but the PR stalled.

[Violeta Hernández]

I think we do in fact need some notation for this, even if it's just a local notation. Otherwise writing API becomes quite painful (and there is in fact API to be written, see #19571). But there seems to be no existing notation in the literature. So, here's a poll to decide what we can do:

[Violeta Hernández]

/poll AntisymmRel (· ≤ ·)
⋚
≗
don't use notation

[Violeta Hernández]

(you can add more choices)

[Kim Morrison]

My point from before is that making up new notation might help on the "painful to write" aspect, but it is actively harmful on the "painful to read" aspect, which is more important.

[Violeta Hernández]

Yeah, my counter to that is that AntisymmRel (· ≤ ·) a b is no less cryptic and no more legible before you read the docs, and after that point any custom notation becomes easier to read.

[Patrick Massot]

I find it a lot less cryptic.

[Jireh Loreaux]

The spelled out version is much easier to read as it tells you that at least it has something to do with antisymmetry, whereas the notation tells you very little, especially because it's nonstandard and it doesn't have any existing counterpart in the library.

[Jireh Loreaux]

On top of that, upon reading it in the source on GitHub, I wouldn't have to go figure out what the name of the declaration is.

[Mario Carneiro]

an alternative slightly-more-documenting notation is a ≤∧≥ b

[Violeta Hernández]

Really like that one

[Violeta Hernández]

I've updated #19554 to use ≤∧≥.

[Violeta Hernández]

At least to me this seems self-documenting enough. As for the declaration name not being clear... I don't see how this is an issue unique to this notation. The name AntisymmRel should still appear in most of the theorem names anyways.

[Violeta Hernández]

I would really like to emphasize that "don't use notation" implies "type out the 19-character sequence AntisymmRel (· ≤ ·) every single time you want to talk about order-equivalent elements in preorders". If we're providing support for Preorder to begin with then I don't think actually talking about them should be so painful.

[Kim Morrison]

Still opposed to notation for this. :-)

[Mario Carneiro]

I think it is also worth clarifying whether this is about local or global notation

[Mario Carneiro]

I'm against a global notation but indifferent about local notation here

[Jireh Loreaux]

As long as we mean local and not scoped, then I suppose it doesn't bother me.

[Jireh Loreaux]

@Violeta Hernández note that in C⋆-algebras, both docs#spectrum and docs#quasispectrum are used all the time, but so far I only ever introduce local notation for them. Admittedly, the first is short, but quasispectrum is close to the length of AntisymmRel (· ≤ ·)

[Violeta Hernández]

I can agree with having only local notation. Ultimately my main use case is PGame and there I can just use the setoid notation instead.

[Jireh Loreaux]

:confused: Then why do you even need local notation? I just looked at #19571 and it's only 100 lines or so that would be affected here.

[Jireh Loreaux]

Compare that to, for example file#Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital, where I use the σₙ local notation for quasispectrum literally 100 times (and that's just one file).

[Jireh Loreaux]

Above
Violeta Hernández said:

I think we do in fact need some notation for this, even if it's just a local notation. Otherwise writing API becomes quite painful

you make it sound like this is especially burdensome, but I think it's simply not.

[Violeta Hernández]

I do think these are slightly different situations. We generally don't have notation for functions, whereas we do often have very concise notation for relations (think =, <, and so on).

[Violeta Hernández]

I also don't think notation would be limited to the 100 lines of my PR. I expect that the AntisymmRel will grow as Mathlib defines more concrete preorders

[Violeta Hernández]

But maybe we'll get there when we get there

[Jireh Loreaux]

I could counter with +, -, /, ⁻¹, • etc to prove your claim wrong. Also note that we don't have notation for docs#Relation.TransGen and friends. It's exactly this situation where we define one relation from another where we often don't have notation.

[Jireh Loreaux]

(docs#NumberField.RingOfintegers is an example of a function with prefix notation, as opposed to infix or postfix)

[Violeta Hernández]

Eh, fine. We can stay notationless for the time being then.

[Violeta Hernández]

I imagine this discussion also implies we shouldn't have any notation for the future incomparability relation IncompRel either

[Violeta Hernández]

I have an alternate proposal

[Violeta Hernández]

Do we really need AntisymmRel for arbitrary relations?

[Violeta Hernández]

Being able to just write AntisymmRel a b would be a pretty major improvement over AntisymmRel (· ≤ ·) a b

[Jireh Loreaux]

Yes, I will for sure. In C⋆-algebras there are multiple orderings which come up a lot. There's the usual a ≤ b if b - a = star x * x for some x, but there's also Cuntz subequivalence and (what is related) Murray-von Neumann equivalence of projections. Both of these are built from certain preorders via AntisymmRel.

[Jireh Loreaux]

These generic operations on relations should all take the specific relation as an argument. (e.g., imagine if Relation.TransGen only acted on ≤, then you wouldn't even be able to state docs#lt_iff_transGen_covBy).

[Jireh Loreaux]

Violeta Hernández said:

I also don't think notation would be limited to the 100 lines of my PR. I expect that the AntisymmRel will grow as Mathlib defines more concrete preorders

Violeta, I suggest we revisit this topic if and when this situation comes to pass. As for the current PR, it really doesn't seem burdensome. If you write 500 lines of necessary AntisymmRel API, then introduce some local notation. After you write 1000, consider some scoped notation. These aren't hard and fast limits, just some guidelines I would use to consider when some notation might be helpful, especially when it seems there isn't an existing consensus that the notation is favorable.

[Mario Carneiro]

I think this is also an instance of a general pattern: Don't prematurely generalize. Wait until you actually need it, because if you try to do it in advance there is even odds that the anticipated use will never happen, and even if it does there are good chances that you will end up needing a different generalization than you prepared. The use cases have to be in the present or very near future, such that you have not just an idea but actual code in the pipeline that benefits from it, enough to counterbalance the cost of changes and additional complexity for readers and library users.

[Mario Carneiro]

Also, remember that library code is not optimized for you the writer, it is optimized for future users of the library (including you tomorrow). That's why readability is much more important than writability. When doing the cost benefit analysis of things like this you have to take care to not let the writer's bias come out too much and put yourself in the reader's shoes.