no_top_order is not an order without a top

Stream: general

[Rémy Degenne]

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]

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]

But also I don't think this is too important.

[Mario Carneiro]

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]

for example, "dense linear order without endpoints" is a common term for orders like Q

[Yaël Dillies]

I disagree, Mario. I use it everywhere and mostly not in linear orders.

[Mario Carneiro]

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]

@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]

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]

I don't think "has no maximal element" is a correct gloss either in the preorder setting

[Rémy Degenne]

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]

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]

add a sentence stating that in a linear order, this is the same as not being order_top, but not in general?

[Mario Carneiro]

There should be a lemma saying that

[Mario Carneiro]

there is docs#not_is_top but it's not a biconditional

[Yaël Dillies]

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]

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]

@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]

Have a look at Yury's description of #9493

[Yaël Dillies]

I perfectly agree with you, hence me not understanding what Yury meant.

[Mario Carneiro]

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]

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]

So Yury meant "to orders which have a bot not declared through order_bot"?

[Mario Carneiro]

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]

A similar thing is done with the nontriviality tactic

[Mario Carneiro]

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]

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]

Sure, the lemma that requires this should point out that the hypothesis is necessary

[Yaël Dillies]

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$ in mind (I think?).

[Mario Carneiro]

is_bot is a very basic definition

[Mario Carneiro]

it says that an element is minimum

[Yaël Dillies]

But the docstring doesn't reflect that.

[Yaël Dillies]

Mario Carneiro said:

it says that an element is minimum

No it doesn't :stuck_out_tongue:

[Mario Carneiro]

??

[Mario Carneiro]

It says that it is less or equal to everything

[Yaël Dillies]

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]

that is, a global minimum element

[Yaël Dillies]

... which is not what being minimal is.

[Mario Carneiro]

I said minimum not minimal

[Yaël Dillies]

Arf, got me

[Mario Carneiro]

I think minimal and maximal are defined as well

[Yaël Dillies]

We have docs#is_min_on, but it's minimum, and with a set and an indexing type on top

[Mario Carneiro]

also docs#is_least

[Yaël Dillies]

That's minimum, not minimal

[Yaël Dillies]

I have #11268 for minimal elements.

[Mario Carneiro]

I'm surprised it managed to evade mathlibification for so long

[Mario Carneiro]

there is a weird version of minimality appearing in docs#zorn.exists_maximal_of_chains_bounded

[Yaël Dillies]

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]

Yeah, Zorn uses minimality without having special predicates.

[Mario Carneiro]

In fact, you might want to consider whether that definition is better than yours for the preorder case

[Yaël Dillies]

It sure is

[Mario Carneiro]

that is, x is maximal if \forall y, x <= y -> y <= x instead of \forall y, x <= y -> x = y

[Yaël Dillies]

Another way people stated minimality is as in docs#eq_bot_of_minimal

[Yaël Dillies]

You're right, Mario, this definition is great.

[Reid Barton]

On another note, I'm very skeptical of the Sometimes called cofinal. part of the docstring

[Yury G. Kudryashov]

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]

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.