Zulip Chat Archive
Stream: general
Topic: no_top_order is not an order without a top
Rémy Degenne (Jan 09 2022 at 11:54):
I just got very confused by the no_top_order
and no_bot_order
classes, which are not what I thought they were by reading the name and the docstrings. Let's look at no_top_order
and order_top
, which are defined as
/-- Order without a maximal element. Sometimes called cofinal. -/
class no_top_order (α : Type u) [has_lt α] : Prop :=
(no_top : ∀ a : α, ∃ a', a < a')
/-- An order is an `order_top` if it has a greatest element. -/
class order_top (α : Type u) [has_le α] extends has_top α :=
(le_top : ∀ a : α, a ≤ ⊤)
(docs#no_top_order and docs#order_top)
no_top_order
is actually stronger than not having a ⊤
element verifying le_top
. Consider a type with three elements a,b,c
such that a < b
and a < c
(and no other order relations). Then there is no ⊤
because b
and c
are not comparable, but this is not a no_top_order
either, because b
and c
don't verify the no_top
condition. no_top_order
also excludes "local" tops.
That issue disappears for linear orders, for which you either have order_top
or no_top_order
. The whole issue is really that unless the order is linear, you don't have docs#le_of_not_lt .
In the same way, the predicate docs#is_top is not in general the opposite of what you get from docs#no_top_order.no_top . Nonetheless, the docstring of is_top
states "This predicate is useful, e.g., to make some statements and proofs work in both cases [order_top α] and [no_top_order α]". This makes me think that the author of those lines probably had linear orders in mind.
In conclusion: should we give another name to no_top_order
to better reflect that it is stronger than not being an order_top
? At least the docstrings need to be modified.
Yaël Dillies (Jan 09 2022 at 12:07):
Yeah this is indeed confusing to people who discover the order library. We could rename them to no_max_order
/no_min_order
.
Yaël Dillies (Jan 09 2022 at 12:07):
But also I don't think this is too important.
Mario Carneiro (Jan 09 2022 at 12:07):
That's the intended behavior. The name is unfortunate but I think standard (modulo some adaptation to our terminology for top elements), since the main interest in this predicate is in total orders
Mario Carneiro (Jan 09 2022 at 12:08):
for example, "dense linear order without endpoints" is a common term for orders like Q
Yaël Dillies (Jan 09 2022 at 12:09):
I disagree, Mario. I use it everywhere and mostly not in linear orders.
Mario Carneiro (Jan 09 2022 at 12:09):
and the terminology emphasizes what the order does not have even though it is a positive statement (every element has a greater element)
Mario Carneiro (Jan 09 2022 at 12:10):
@Yaël Dillies Er, I mean the birthplace of the concept is in the linear setting. It generalizes, as many things do, to beyond where the conventional terminology makes a lot of sense
Rémy Degenne (Jan 09 2022 at 12:14):
Yaël Dillies said:
But also I don't think this is too important.
No it's not very important, indeed. It's still confusing. I am perfectly ok with leaving the name as it is if the notion is only useful for linear orders. But I'll PR some changes to the docstrings in that file to point out that the name reflects what happens in the linear order case.
Mario Carneiro (Jan 09 2022 at 12:15):
I don't think "has no maximal element" is a correct gloss either in the preorder setting
Rémy Degenne (Jan 09 2022 at 12:15):
And indeed the code I was originally writing was about a linear order. i only got surprised by that subtlety once I tried removing hypotheses from my lemmas as much as possible.
Mario Carneiro (Jan 09 2022 at 12:18):
The comment on no_top_order
already says "Order without a maximal element." so I'm not sure what you want to change
Rémy Degenne (Jan 09 2022 at 12:20):
add a sentence stating that in a linear order, this is the same as not being order_top
, but not in general?
Mario Carneiro (Jan 09 2022 at 12:20):
There should be a lemma saying that
Mario Carneiro (Jan 09 2022 at 12:22):
there is docs#not_is_top but it's not a biconditional
Yaël Dillies (Jan 09 2022 at 13:02):
Okay, here's something that's really confusing: @Yury G. Kudryashov's docstring for docs#is_bot, docs#is_top. is_bot
never applies in a no_bot_order
, so is_bot
is most definitely not allowing to treat order_bot
and no_bot_order
simultaneously.
Yaël Dillies (Jan 09 2022 at 13:04):
Yury, did you mean "to orders which have a bot not declared through order_bot
", "to preorders which might have several bots", or did you mean to define is_min
instead? In the latter case, I suspect your lemmas in #9396 generalize.
Mario Carneiro (Jan 09 2022 at 13:06):
@Yaël Dillies said:
is_bot
never applies in ano_bot_order
, sois_bot
is most definitely not allowing to treatorder_bot
andno_bot_order
simultaneously.
What do you mean? They are supposed to be mutually exclusive. The claim that connects them is that order_bot
holds iff there exists a
such that is_bot a
, and no_bot_order
holds iff there does not exist a
such that is_bot a
(under certain additional hypotheses)
Yaël Dillies (Jan 09 2022 at 13:07):
Have a look at Yury's description of #9493
Yaël Dillies (Jan 09 2022 at 13:07):
I perfectly agree with you, hence me not understanding what Yury meant.
Mario Carneiro (Jan 09 2022 at 13:09):
I think he meant what I said. There are complications with directly using a disjunction of order_bot
and no_bot_order
because these are typeclasses, not props, and order_bot
also comes with a designated bottom element which is difficult to work with here. With is_bot
, you can do the case disjunction cleanly using by_cases h : \exists a, is_bot a
Mario Carneiro (Jan 09 2022 at 13:10):
To make that work, you need lemmas that say that you can construct an order_bot
given is_bot a
, and a no_top_order
given \neg \exists a, is_bot a
Yaël Dillies (Jan 09 2022 at 13:11):
So Yury meant "to orders which have a bot not declared through order_bot
"?
Mario Carneiro (Jan 09 2022 at 13:12):
Yeah, if you don't have a bot at all, and you want to reason with order_bot
and no_bot_order
anyway you have to do something like that
Mario Carneiro (Jan 09 2022 at 13:12):
A similar thing is done with the nontriviality
tactic
Mario Carneiro (Jan 09 2022 at 13:13):
you don't know that it is either trivial or nontrivial but you can do a case disjunction and get a typeclass in each case
Yaël Dillies (Jan 09 2022 at 13:13):
What's confusing is that the "certain additional hypotheses" comprises being linear, which to my eyes (and Rémy's) is quite a strong condition which we shouldn't just sweep under the rug.
Mario Carneiro (Jan 09 2022 at 13:13):
Sure, the lemma that requires this should point out that the hypothesis is necessary
Yaël Dillies (Jan 09 2022 at 13:14):
The docstrings for docs#is_bot and docs#is_top are confusing because they are in the most basic order theory file but were written with in mind (I think?).
Mario Carneiro (Jan 09 2022 at 13:14):
is_bot
is a very basic definition
Mario Carneiro (Jan 09 2022 at 13:14):
it says that an element is minimum
Yaël Dillies (Jan 09 2022 at 13:15):
But the docstring doesn't reflect that.
Yaël Dillies (Jan 09 2022 at 13:15):
Mario Carneiro said:
it says that an element is minimum
No it doesn't :stuck_out_tongue:
Mario Carneiro (Jan 09 2022 at 13:15):
??
Mario Carneiro (Jan 09 2022 at 13:15):
It says that it is less or equal to everything
Yaël Dillies (Jan 09 2022 at 13:15):
Anyway, I need is_min
and is_max
now, so I'll define them next to is_bot
and is_top
and clarify the docstrings.
Mario Carneiro (Jan 09 2022 at 13:16):
that is, a global minimum element
Yaël Dillies (Jan 09 2022 at 13:16):
... which is not what being minimal is.
Mario Carneiro (Jan 09 2022 at 13:16):
I said minimum not minimal
Yaël Dillies (Jan 09 2022 at 13:16):
Arf, got me
Mario Carneiro (Jan 09 2022 at 13:16):
I think minimal and maximal are defined as well
Yaël Dillies (Jan 09 2022 at 13:17):
We have docs#is_min_on, but it's minimum, and with a set and an indexing type on top
Mario Carneiro (Jan 09 2022 at 13:18):
also docs#is_least
Yaël Dillies (Jan 09 2022 at 13:18):
That's minimum, not minimal
Yaël Dillies (Jan 09 2022 at 13:18):
I have #11268 for minimal elements.
Mario Carneiro (Jan 09 2022 at 13:20):
I'm surprised it managed to evade mathlibification for so long
Mario Carneiro (Jan 09 2022 at 13:21):
there is a weird version of minimality appearing in docs#zorn.exists_maximal_of_chains_bounded
Yaël Dillies (Jan 09 2022 at 13:21):
Agreed! And I wouldn't be surprised if it's actually already in some dark corner file of the library. What I'm sure of is that it is not where it should be, aka order.basic
.
Yaël Dillies (Jan 09 2022 at 13:21):
Yeah, Zorn uses minimality without having special predicates.
Mario Carneiro (Jan 09 2022 at 13:22):
In fact, you might want to consider whether that definition is better than yours for the preorder case
Yaël Dillies (Jan 09 2022 at 13:22):
It sure is
Mario Carneiro (Jan 09 2022 at 13:23):
that is, x is maximal if \forall y, x <= y -> y <= x
instead of \forall y, x <= y -> x = y
Yaël Dillies (Jan 09 2022 at 13:31):
Another way people stated minimality is as in docs#eq_bot_of_minimal
Yaël Dillies (Jan 09 2022 at 13:57):
You're right, Mario, this definition is great.
Reid Barton (Jan 09 2022 at 14:31):
On another note, I'm very skeptical of the Sometimes called cofinal.
part of the docstring
Yury G. Kudryashov (Jan 09 2022 at 14:32):
Yaël Dillies said:
Okay, here's something that's really confusing: Yury G. Kudryashov's docstring for docs#is_bot, docs#is_top.
is_bot
never applies in ano_bot_order
, sois_bot
is most definitely not allowing to treatorder_bot
andno_bot_order
simultaneously.
I meant something like docs#exists_countable_dense_bot_top . It states something about bot
/top
but works both for types with bot
/top
, and for types without bot
/top
. Feel free to improve the docstring.
Yaël Dillies (Jan 10 2022 at 18:22):
I'm renaming the instances and trying to make the docstrings more understandable in #11357. The docstrings do not make as much sense as they could because we're missing is_min
/is_max
and the real no_bot_order
/no_top_order
.
Last updated: Dec 20 2023 at 11:08 UTC