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 a no_bot_order, so is_bot is most definitely not allowing to treat order_bot and no_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 R\R 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 a no_bot_order, so is_bot is most definitely not allowing to treat order_bot and no_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