Comparison in preorders

Stream: maths

[Violeta Hernández]

So right now, a lot of my PRs are blocked due to design decisions that need to be made. Basically, I wanted to make an analog to docs#cmp for preorders, to be used to golf many results on games. In a preorder, any two elements compare as either <, or >, or are equivalent up to antisymmetry (x ≤ y and y ≤ x), or are incomparable. I wanted to express these last two as antisymm_rel (≤) x y and incomp_rel (≤) x y, the latter being a new predicate defined as incomp_rel r x y := ¬ r x y ∧ ¬ r y x.

I was told that having incomp_rel on its own wouldn't make much sense, as we could write incomp_rel (≤) x y as antisymm_rel (≤)ᶜ x y (after a refactor moving the docs#pi.has_compl instance earlier in the import chain). I don't like this, since thinking about incomparable elements as "equivalent up to antisymmetry by the not less equal relation" is really awkward even if it makes mathematical sense. @Yaël Dillies suggested that we could specialize antisymm_rel to ≤ and rename it to order.indistinguishable, and have incomp_rel as order.incomparable. After all, we currently only use antisymm_rel on the ≤ relation coming from a preorder. This was then opposed by @Bhavik Mehta who mentioned we might need the relation in further generality later down the line.

In short, there's three possibilities:

• make a new incomp_rel together with antisymm_rel.
• use antisymm_rel (≤)ᶜ to spell out incomparability.
• specialize antisymm_rel to ≤, rename to order.indistinguishable, make order.incomparable to match.

Not sure if a vote would be best here, but I'd like at least some further discussion.

[Violeta Hernández]

Incomparability is a really basic predicate on preorders and it's very relevant when discussing antichains, so I'd prefer if we had a specialized spelling for it. I also think there's little point in having antisymm_rel for general relations, since it's only relevant on preorders, and I doubt we have many important preorders that aren't part of a preorder instance.

[Violeta Hernández]

And regarding indistinguishability, would order.indistinguishablecoincide with docs#topology.inseparable in the order topology? That would be a nice result to have.

[Bhavik Mehta]

To be clear, my opposition to the proposal was because it specialises docs#antisymm_rel away from a general relation and insists on a preorder which is strictly less general with no benefit that I'm aware of. As a very basic example of where this construction shows up outside of preorders - it's one of the ways of constructing a graph from directed graph "by forgetting direction". I'm more than happy to rename, but I don't think the specialisation is a good idea

[Violeta Hernández]

Ah, you're right about that

[Violeta Hernández]

There goes approach 3 then

[Violeta Hernández]

Then my support goes to approach 1

[Violeta Hernández]

We could define incomp_rel in terms of antisymm_rel and port the appropriate API over via def-eqs

[Violeta Hernández]

That way we get the benefits of a clear way of writing incomparability while still minimizing API duplication

[Violeta Hernández]

Bhavik Mehta said:

As a very basic example of where this construction shows up outside of preorders - it's one of the ways of constructing a graph from directed graph "by forgetting direction".

Wait, this is actually wrong. The antisymmetrization of a directed graph gives you an undirected graph where edges that exist in one direction but not the other get removed. Which is not quite the usual construction of an undirected graph from a directed one.

[Violeta Hernández]

Still, I do agree with your argument. We don't really benefit by specialization.

[Violeta Hernández]

I wonder if we could maybe have notation to at least make the ≤ case easier to write down. We could use x ⋚ y for antisymm_rel (≤) x y, but unfortunately Unicode doesn't seem to have a symbol for the negation.

[Violeta Hernández]

We could maybe borrow ∥ from game theory, and put it in a locale so that the geometers don't get mad at us

[Bhavik Mehta]

Violeta Hernández said:

Bhavik Mehta said:

As a very basic example of where this construction shows up outside of preorders - it's one of the ways of constructing a graph from directed graph "by forgetting direction".

Wait, this is actually wrong. The antisymmetrization of a directed graph gives you an undirected graph where edges that exist in one direction but not the other get removed. Which is not quite the usual construction of an undirected graph from a directed one.

Oops, you're right! But I think it's still a reasonably standard construction :)

[Junyan Xu]

Some constructions certainly needs to be specialized to preorders. When it's not a preorder, docs#antisymm_rel.setoid isn't a setoid. To get the strong connected components (a standard construction), you take the transitive closure (actually, docs#relation.refl_trans_gen) so it becomes a preorder, and then take the antisymm_rel.

[Bhavik Mehta]

Junyan Xu said:

Some constructions certainly needs to be specialized to preorders. When it's not a preorder, docs#antisymm_rel.setoid isn't a setoid. To get the strong connected components (a standard construction), you take the transitive closure (actually, docs#relation.refl_trans_gen) so it becomes a preorder, and then take the antisymm_rel.

Agreed, but I don't think this means that antisymm_rel itself needs to be specialized

[Violeta Hernández]

All that I'm missing is a verdict on incomp_rel. I opened #15602, which obsoletes the problem of ᶜ not always being available. But I still think that antisymm_rel (≤)ᶜ is a really weird spelling for incomparability, particularly if we work under the mental model where antisymm_rel is almost always meant to be used on preorders.

[Violeta Hernández]

Well, I'll open the incomp_rel PR again and we can discuss it there

[Violeta Hernández]

I'm just now realizing

[Violeta Hernández]

If I were to introduce notation for incomp_rel (≤), then it would be natural to just use incomp to name lemmas using this, instead of incomp_rel

[Violeta Hernández]

Or maybe incomp_le

[Violeta Hernández]

But what about antisymm_rel (≤)? Using antisymm or antisymm_le would both be misleading

[Violeta Hernández]

Maybe we should rename antisymm_rel into indist_rel so that we can just use indistin theorem names?

[Violeta Hernández]

An alternative would be to use equiv as in docs#pgame.equiv, but I'd rather not since that word is quite overloaded