Zulip Chat Archive
Stream: general
Topic: diamond in `complete_linear_order`
Yury G. Kudryashov (Jan 08 2022 at 07:16):
[complete_linear_order α] creates a diamond for [lattice α]: one instance goes through complete_linear_order.to_complete_lattice, another one goes through complete_linear_order.to_linear_order.
Yury G. Kudryashov (Jan 08 2022 at 07:18):
/poll How should we solve it?
Redefine linear_order to have fields inf and sup instead of min and max
Redefine complete_linear_order and conditionally_complete_linear_order so that they no longer extend structures with sup/inf
Johan Commelin (Jan 08 2022 at 07:53):
Would it make sense to redefine linear_order to have fields inf + sup and min + max?
Yaël Dillies (Jan 08 2022 at 07:54):
Sure it does. There's also the Yakov way of doing things which is to make linearity a mixin. And that may be what we'll eventually do.
Eric Wieser (Jan 08 2022 at 11:09):
Do you have an example of the diamond being non-defeq?
Eric Wieser (Jan 08 2022 at 11:11):
If docs#complete_linear_order is an old style structure, can you just use renaming to merge the inf and min fields?
Yury G. Kudryashov (Jan 08 2022 at 15:41):
We already have a mixin for linearity; it's called [is_total α (≤)].
Yury G. Kudryashov (Jan 08 2022 at 15:43):
@Johan Commelin What are the advantages of inf + sup + min + max?
Yury G. Kudryashov (Jan 08 2022 at 15:44):
@Eric Wieser The diamond is non-defeq if you write {α : Type*} [complete_linear_order α].
Eric Wieser (Jan 08 2022 at 15:50):
Eric Wieser (Jan 08 2022 at 15:51):
I've no idea which way around is the better direction for the rename
Eric Wieser (Jan 08 2022 at 15:51):
It probably doesn't matter
Yury G. Kudryashov (Jan 08 2022 at 16:09):
Probably you should do the same with docs#conditionally_complete_linear_order
Eric Wieser (Jan 08 2022 at 19:45):
Feel free to push to that branch, I'm done for the day
Eric Wieser (Jan 12 2022 at 00:00):
Alright, I think I have #11309 building now. Probably it would still be convenient to rename the max field to sup and min to inf, but that's largely cosmetic.
Yury G. Kudryashov (Jan 12 2022 at 00:45):
I left 2 comments.
Eric Wieser (Jan 19 2022 at 18:22):
Do we still want to rename themin and max fields to inf and sup? Or is there no longer any reason to care now that the diamond is gone?
Yury G. Kudryashov (Jan 21 2022 at 05:11):
I would prefer to unify names but now this is a low-priority task for me.
Yury G. Kudryashov (Jan 21 2022 at 05:12):
While the diamond is gone, we have yet another way to create hard-to-notice diamonds.
Yury G. Kudryashov (Jan 21 2022 at 05:12):
(e.g., some version of the PR that fixed this diamond introduced another one)
Last updated: Dec 20 2023 at 11:08 UTC