WithTop is a SuccOrder

Stream: mathlib4

[Yury G. Kudryashov]

Currently, we have 2 instances that turn WithTop into a SuccOrder, depending on whether the original type has a maximal element or not. What do you think about unifying them into

def WithTop.succ : WithTop α → WithTop α
  | (a : α) => if succ a = a then \top else some (succ a)
  | \top => \top

[Yury G. Kudryashov]

@Yaël Dillies :up:

[Yury G. Kudryashov]

I didn't test that it works for any [PartialOrder α] [SuccOrder α] [DecidableEq α] yet.

[Yury G. Kudryashov]

Another option is to test for IsMax a assuming ∀ a, Decidable (IsMax a). On the one hand, this way we can have efficient Decidable instances for this predicate. On the other hand, a generic instance assuming [DecidableEq α] [OrderTop α] would conflict with, e.g., type-specific instance for WithTop _.

[Junyan Xu]

My PR #9480 depends on the defeq succ (some a) = some (succ a) which isn't preserved by your proposed unification ...

[Yaël Dillies]

That looks fine to me, but I guess you'll have to fix Junyan's application

[Eric Rodriguez]

How crucial is the defeq?

[Yury G. Kudryashov]

I can add a def that works in all cases, then use .copy (adding if it's not here yet) to provide necessary defeq in the existing cases.

[Junyan Xu]

In the meantime, the unification of the two instances has been implemented by @Daniel Weber #15881. I'm now reviving my PR #9480 and found that the defeq has been broken. What I plan to do is to restore the removed NoMax/MinOrder instances as defs and use the NoMaxOrder instance in my PR. Hopefully there's no objection. I think I'll go ahead to implement Yury's suggestion above.

[Yaël Dillies]

Eric Rodriguez said:

How crucial is the defeq?

@Junyan Xu, would you mind answering the above?

[Junyan Xu]

Oh wait, I think I misdiagnosed the breakage in #9480, and my solution in #15881 isn't optimal. I think we can unify the instances while keeping favorable defeq, by replacing [DecidableEq] by [Decidable (a = succ a)] and provide an instances for the latter in the case of NoMaxOrder (that is always false). But deriving data-carrying instance like Decidable from Prop instance is probably not good practice, as it may conflict with existing DecidableEq instance. So maybe I'll just locally add a [Decidable (a = succ a)] instance in my PR.

The situation is basically this: you have a sequence of vector subspaces $\mathbb{R}^0\subset\mathbb{R}^1\subset\mathbb{R}^2\subset\dots$ indexed by ℕ of the countably infinite-dimensional space $\mathbb{R}^\infty$, and you want to add a top element as the index of their union, which is the whole space ⊤. After you do this you still want the successor of $\mathbb{R}^1$ reduce to $\mathbb{R}^2$ rather than some if-then-else expression. (If you do a rewrite it might break the algebraic/topological instances on these subspaces.) Of course for ℕ the reduction does work, but not in my setting where the SuccOrder is from an ordinal and doesn't have computable DecidableEq.

[Junyan Xu]

Actually linearOrder_toType for Ordinal.toType contains a noncomputable DecidableEq instance, so I'll need more maneuver to get the correct SuccOrder instance on WithTop o.toType.

[Violeta Hernández]

Why are you using o.toType?

[Violeta Hernández]

As the docstring explains, you should only be using this over Iio o when you absolutely need something in Type u

[Violeta Hernández]

I'd also like to mention an idea I previously had to generalize succ and pred to arbitrary orders and to instead have SuccOrder as a Prop-valued typeclass constraining these functions. I'm still not sure if this is a good idea, and in particular, I'd like to know whether the def-eqs provided by succ and pred are important in practice.

[Junyan Xu]

I have been able to make #9480 compile by just adding two lines in SuccPred/Basic and one line local instance (i : ι) : Decidable (succ i = i) := .isFalse (lt_succ i).ne' in the main file, so I'll probably abandon #15881. As I explained the defeq of the succ field is very convenient.

Violeta Hernández said:

As the docstring explains, you should only be using this over Iio o when you absolutely need something in Type u

I checked and there are multiple places that break with the universe bump: first if you define ι := Iio (Module.rank F E).ord instead of (Module.rank F E).ord.toType then #ι = Module.rank F E doesn't compile and you'd need to use Cardinal.lift. Second, there's two families of types Factor and Emb (both in the universe of E) such that $\mathrm{Emb}(o)\simeq\prod_{i < o}\mathrm{Factor}(i)$, and if o is in a higher universe then the cardinal equality would require a Cardinal.lift. In summary, making the change would unnecessarily complicate the code.

[Violeta Hernández]

Hm, that's unfortunate, but I guess o.toType might be the solution.