WithBot (WithTop α)

Stream: general

[Violeta Hernández]

There are two possible ways to endow a type with both a top and a bottom element: WithBot (WithTop α), and WithTop (WithBot α). I'd like to create a common definition WithBotTop α subsuming both of them. But I'm running into some quite large annoyances.

My initial idea was to define this as an abbrev. This entirely breaks to_dual, unfortunately. We can set the dual of WithBotTop α to be itself, but then the inferred ≤ instance from WithBot will not be def-eq to its dual, and shenanigans ensue.

If we choose to hide the definition behind a def, we run into the problem that the existing API on WithBot and WithTop is unusable. We'd have to re-prove these theorems from scratch. Which admittedly shouldn't be so hard, since we can use the def-eq with WithBot (WithTop α) to prove theorems, but then hide it from the public API.

What's the correct course of action here?

[Violeta Hernández]

cc @Ayhon @Joël Riou

[Violeta Hernández]

The open PR #33876 takes a third approach, defining both WithBotTop α = WithBot (WithTop α) and WithTopBot α = WithTop (WithBot α). This does make to_dual functional, but to me it seems like needless duplication; these two types should morally be the same.

[Violeta Hernández]

Actually, here's an idea. Perhaps we could define the order isomorphisms WithBotTop α ≃o WithBot (WithTop α) and WithBotTop α ≃o WithTop (WithBot α), and use them to transfer API in a to_dual-friendly manner?

[Martin Dvořák]

Great initiative!

I did something similar https://github.com/madvorak/duality/blob/main/Duality/ExtendedFields.lean but it is far from being sufficiently general for Mathlib.

[Ayhon]

Would it be possible to change to_dual instead?

[Joël Riou]

Violeta Hernández said:

The open PR #33876 takes a third approach, defining both WithBotTop α = WithBot (WithTop α) and WithTopBot α = WithTop (WithBot α). This does make to_dual functional, but to me it seems like needless duplication; these two types should morally be the same.

Not exactly. My intend was only to introduce WithBotTop because EReal was defined in this way.

[Wrenna Robson]

An idle observation that may well not be helpful: one could imagine, instead of WithBot and WithTop, operators on α that add the bot or top if they are not already present.

[Violeta Hernández]

Sure, but I'm not sure if we want that? We have legitimate uses for adding bottom/top elements to types that already have them, see e.g. docs#Polynomial.degree.

[Kevin Buzzard]

Differentiability on manifolds takes a parameter in WithTop ENat :-) (infinity means infinitely-differentiable, top means analytic (i.e. has a power series, which is a stronger condition for real-valued functions).

[Niels Voss]

I guess adding top and bottom elements if they don't already exist could make sense from the perspective of it being kind of like an order-theoretic closure (not sure what that would be called), but WithTop would probably be useful more often

[Eric Wieser]

Violeta Hernández said:

these two types should morally be the same.

Don't they disagree on the value of bot + top?

[Wrenna Robson]

Violeta Hernández said:

Sure, but I'm not sure if we want that? We have legitimate uses for adding bottom/top elements to types that already have them, see e.g. docs#Polynomial.degree.

Yeah I think it has mostly only disadvantages in general.

[Wrenna Robson]

Niels Voss said:

I guess adding top and bottom elements if they don't already exist could make sense from the perspective of it being kind of like an order-theoretic closure (not sure what that would be called), but WithTop would probably be useful more often

Yes that's what I meant really - sometimes WithTop is the top-closure but sometimes it isn't.

[Violeta Hernández]

Eric Wieser said:

Violeta Hernández said:

these two types should morally be the same.

Don't they disagree on the value of bot + top?

Oh, yikes...

[Violeta Hernández]

Does this mean we want both aliases to be available? Or do we just choose one and go with it?

[Joël Riou]

For EReal, the ship has sailed.

[Kevin Buzzard]

IIRC I was responsible for EReal and there was some discussion of this issue at the time but I don't remember any compelling arguments for being careful about which order to choose.

[Aaron Liu]

we want ENNReal.log (x * y) = ENNReal.log x + ENNReal.log y to be unconditional

[Aaron Liu]

so since 0 * ⊤ = 0 therefore ⊥ + ⊤ = ⊥

[Kevin Buzzard]

And I think 0 * ⊤ = 0 is motivated by measure theory (i.e. there really is a good reason for this choice, analysts want the integral of a function which is mostly 0 but takes the value infinity on a set with zero measure to be zero and not infinity) so this looks like a good argument for ⊥ + ⊤ = ⊥.

[Martin Dvořák]

I agree that ⊥ + ⊤ = ⊥ = ⊤ + ⊥ is the morally correct option.

[Sébastien Gouëzel]

In fact the initial definition of EReal gave bot + top = top, and for precisely the reason given above I have refactored it some time ago (changing from WithTop (WithBot R)) to WithBot (WithTop R)).

[Kevin Buzzard]

I can quite believe that in my original work I made a random choice; it was only this $0\times\infty=0$ observation coming from measure theory which made me understand that sometimes there was a good answer to these junk-looking questions.

[Eric Wieser]

Aaron Liu said:

we want ENNReal.log (x * y) = ENNReal.log x + ENNReal.log y to be unconditional

Couldn't we also argue that we want -(a + b) = -a + -b to be unconditional?

[Eric Wieser]

(which would be satisfied by ⊥ + ⊤ = 0)

[Kevin Buzzard]

I think that the conclusion is an absurd choice but it's a reasonable observation. Perhaps the difference is that (a) measure theory is giving us good conventions for ENNReal and log is a natural bijection between ENNReal and EReal but (b) Neg, whilst being a bijection from EReal to itself, is not the natural one (the natural one is id).