weaker SuccOrder/PredOrder

Stream: mathlib4

[Floris van Doorn]

Yaël Dillies said:

It is, yes (at least so long as you don't care about infinite dangling bits). But from your description it's not very clear how exactly you want to manipulate rooted trees

I don't think this is true at all. The axiom le_of_pred_lt states that every node that is the predecessor of another node has a unique successor, so there cannot be any branches in your tree.

I think the SuccOrder/PredOrder classes are too strong. I would like to have classes where the final axiom is removed. This is also useful in the Carleson project, where we are working with a finite rooted trees as an order: https://github.com/fpvandoorn/carleson/blob/master/Carleson/GridStructure.lean#L180-L191

[Yaël Dillies]

Floris van Doorn said:

I don't think this is true at all. The axiom le_of_pred_lt states that every node that is the predecessor of another node has a unique successor, so there cannot be any branches in your tree.

Sorry yeah. I automatically switched off that requirement in my head. What I had in mind was an order α with an endomorphism pred : α → α such that pred a ⩿ a and ¬ IsMin a → pred a ⋖ a

[Daniel Weber]

Well, other then using a wrong definition of trees, I finished formalizing the proof. Hopefully it wouldn't be too hard to fix my definition.

[Daniel Weber]

Floris van Doorn said:

Yaël Dillies said:

It is, yes (at least so long as you don't care about infinite dangling bits). But from your description it's not very clear how exactly you want to manipulate rooted trees

I don't think this is true at all. The axiom le_of_pred_lt states that every node that is the predecessor of another node has a unique successor, so there cannot be any branches in your tree.

I think the SuccOrder/PredOrder classes are too strong. I would like to have classes where the final axiom is removed. This is also useful in the Carleson project, where we are working with a finite rooted trees as an order: https://github.com/fpvandoorn/carleson/blob/master/Carleson/GridStructure.lean#L180-L191

What would be a good to resolve that in Mathlib? I think definingWeakPredOrder and WeakSuccOrder without it (and making PredOrder/SuccOrder extend it) could work well enough, although it will require some work to figure out how to handle the existing lemmas

[Floris van Doorn]

Yeah, adding WeakPredOrder and WeakSuccOrder would be good. Although my preference would be that those actually become the default classes, and that the current classes become StrongPredOrder/StrongSuccOrder or something. The weaker ones feel a lot more natural. E.g. if X is a WeakSuccOrder then WithTop X is one too - this doesn't hold for the current SuccOrder.
Also, types that are both WeakPredOrder + WeakSuccOrder are also both StrongPredOrder and StrongSuccOrder.

[Daniel Weber]

Couldn't that cause a problem with dependencies, or are renames generally ok in Mathlib?

[Kim Morrison]

Use @[deprecated (since := "2024-08-16")] alias X := Y to indicate the replacements, and you're good to go!

[Daniel Weber]

We want to keep the old name, but change its meaning, so an alias couldn't work. I think this is the same problem as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Deprecation.20.26.20recycling.20lemma.20names

[Kim Morrison]

Careful explanation in the PR description, so that someone tripped up by the change can at least jump to source, git blame, and then read the explanation.

[Kim Morrison]

But yes, Mathlib is generally pretty bold about this. We're trying to reform. :-)

[Yaël Dillies]

Floris van Doorn said:

if X is a WeakSuccOrder then WithTop X is one too - this doesn't hold for the current SuccOrder.

We do have docs#WithTop.succOrderOfNoMaxOrder though, but yes, point taken

[Yaël Dillies]

I think your refactor is plenty reasonable since your proposed weaker typeclass is in fact equivalent to my current one in the case of a linear order, which is really all I cared about when I originally introduced it

[Daniel Weber]

I'll work on it, then

[Daniel Weber]

I'm working on it on #15881, but I'm having some trouble in file#Mathlib/Order/SuccPred/Limit. In particular, are docs#Order.isSuccLimitRecOn_succ', docs#SuccOrder.limitRecOn_succ and docs#PredOrder.limitRecOn_pred true for weak succ/pred orders?

[Yaël Dillies]

No, can't be, since now every element can be the successor of several ones, so you can't ensure you know how the data was created

[Daniel Weber]

I see, thanks, I moved those results (and what depends on them) to a section which assumes a strong order

[Yaël Dillies]

My preference would for those lemmas to assume LinearOrder

[Daniel Weber]

Is there a benefit to that over assuming StrongSuccOrder and having an instance LinearOrder + SuccOrder -> StrongSuccOrder?

[Yaël Dillies]

Yes, your suggestion loops with the StrongSuccOrder → SuccOrder instance

[Daniel Weber]

Oh, so that can't be added as an instance?

[Yaël Dillies]

Well, Lean 4 claims to have cured cancer allowed looping instances, but in practice the algorithm seems to fail to notice it is looping in some cases :shrug:

[Yaël Dillies]

+I don't have any non-silly example of a strong non-linear succ order. Here is a silly example: ℕ ⊕ ℕ

[David Wärn]

fwiw, mathlib has rooted trees in the form of docs#Quiver.Arborescence

[Violeta Hernández]

So, what exactly do PredOrder and StrongPredOrder represent when not used with linear orders?

[Violeta Hernández]

Would it be accurate to say they both represent trees? Where pred x gives you the root of the branch containing x

[Violeta Hernández]

Then the difference between both is that PredOrder can have more than one leaf per branch, while StrongPredOrder cannot

[Violeta Hernández]

I think that's all worth writing in some docstring.

[Violeta Hernández]

Also, the fact that PartialOrder + SuccOrder gains almost no generality over LinearOrder + SuccOrder seems like something important to note.

[Violeta Hernández]

Another way to think about it is that in a SuccOrder, succ ais the unique least element greater than a. A StrongSuccOrder guarantees that a is also the unique greatest element lesser than succ a (save for the IsMax a case)

[Violeta Hernández]

Hey, wait a second. Do we even need StrongSuccOrder?

[Violeta Hernández]

I agree with Yaël that all the examples of it that aren't linear orders are silly. I think it's little but a source of confusion that successor orders on partial orders exist at all.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Why not simply use LinearOrder + SuccOrder?

[Notification Bot]

33 messages were moved here from #Is there code for X? > rooted trees by Floris van Doorn.

[Floris van Doorn]

I would also be happy to get rid of the strong versions (i.e. just remove the last axiom from the current SuccOrder/PredOrder).

Unless I made a mistake, this is I believe this is a full characterization of strong succ-orders:
X Is a strong succ-order iff X is (order-)isomorphic to (i : ι) × α i lexicographically ordered, where

• ι is any partial order
• α i is isomorphic to ℤ, ℕ, ℕᵒᵈ or Fin n (n ≥ 1)
• if α i has a maximal element, then i is a maximal element

This also shows how similar strong succ-orders and strong pred-orders are: strong pred-orders are the same, except that in the last bullet point "maximal" is replaced by "minimal".

I think that because of this characterization, it is unlikely we will find interesting nonlinear strong succ-orders.

[Daniel Weber]

I see there's a consensus, so I'll do that

[Yaël Dillies]

Yes, I agree with this characterisation

[Daniel Weber]

#15881 passes CI now

[Violeta Hernández]

Floris van Doorn said:

This also shows how similar strong succ-orders and strong pred-orders are: strong pred-orders are the same, except that in the last bullet point "maximal" is replaced by "minimal".

Just to note, this doesn't mean they're the same! A good example is Ordinal, which is a succ order but not a pred order (since ω has no predecessor but is not minimal)

[Violeta Hernández]

Is any IsSuccArchimedean + LinearOrder also IsPredArchimedean though?

[Daniel Weber]

In terms of this characterization, a linear strong succ-order being achimedean means that ι is a singleton, doesn't it?

[Violeta Hernández]

I think so, and all of ℤ, ℕ, ℕᵒᵈ and Fin n are both succ and pred archimedean

[Floris van Doorn]

Violeta Hernández said:

Is any IsSuccArchimedean + LinearOrder also IsPredArchimedean though?

I believe that currently IsSuccArchimedeanand IsPredArchimedean are always equivalent, not just for linear orders.
In terms of the characterization, they both hold iff ι holds the trivial order.

[Daniel Weber]

Only if both a SuccOrder and PredOrder exists, no? Your characterization doesn't hold for non-linear orders

[Floris van Doorn]

Where does my characterization fail for non-linear orders?

[Daniel Weber]

I meant a non-linear weak order

[Floris van Doorn]

Yes, I mean that strong succ-order + IsSuccArchimedean is equivalent to strong pred-order + IsPredArchimedean.

[Violeta Hernández]

So, ehm. I was thinking about weakening these even further.

[Violeta Hernández]

Specifically, I wanted to generalize docs#Ordinal.pred to any succ-order. This isn't a true predecessor, since it satisfies e.g. pred ω = ω even though ω isn't minimal.

[Violeta Hernández]

But talking about this on #16463, I realized that we might actually be able to generalize things further.

[Violeta Hernández]

For any preorder, you can define a function pred (or dually succ) satisfying the following axioms

class WeakPredOrder (α : Type*) [Preorder α] where
  pred : α → α
  pred_wcovBy : ∀ a, pred a ⩿ a
  pred_of_covBy {a b} : a ⋖ b → pred b ⋖ b

This function is not in general unique - in general, pred a is just some random element covered by a if it exists. It should be unique for linear orders, though. Our current SuccOrder / PredOrder can instead be rewritten so as to constrain this function. I think this should give something equivalent to what we currently have

class PredOrder' (α : Type*) [Preorder α] extends WeakPredOrder α where
  isMin_of_isSuccLimit {a : α} : IsSuccLimit a → IsMin a
  eq_left_of_covBy {a b c : α} : a ⋖ c → b ⋖ c → a = b

That is, a PredOrder is an order where every non-minimal element covers another unique element.

[Daniel Weber]

isMin_of_isSuccLimit is only nontrivial for infinite types, right?

[Daniel Weber]

And it's also a consequence of archimedeaness

[Violeta Hernández]

I believe so. For the record, the definition of IsSuccLimit a is simply ∀ b, ¬ b ⋖ a.

[Violeta Hernández]

If IsSuccLimit a and ¬ IsMin a, take b < a. You can then build an increasing sequence of elements all greater than a, using that none of them can cover a, to prove α is infinite.

[Violeta Hernández]

eq_left_of_covBy should always be true for linear (directed?) orders

[Yaël Dillies]

Definitely not true for codirected orders. Take eg ℕ × ℕ

[Violeta Hernández]

What do you think about this redesign? Is it a good idea?

[Violeta Hernández]

I can try to prove the expected results first just to make sure everything is sound. Basically:

• the new classes should be equivalent to the old ones
• WeakSuccOrder is non-empty for any preorder
• if a partial order is a SuccOrder, then WeakSuccOrder is a subsingleton
• if an order is linear, WeakSuccOrder is a subsingleton

[Daniel Weber]

I personally think of pred as (a slight generalization of) modeling a parent in a forest. I think the current PredOrder models a graph-theoretic forest, while this WeakPredOrder models the parent in a more general set-theoretic tree. Do you think this intuition is correct?

[Violeta Hernández]

I think it's still accurate to say WeakPredOrder gives you a parent - the difference is that the parent can not exist, or not be unique.

[Violeta Hernández]

It is however unique at least in two cases: when you do have a PredOrder, or in a linear order.

[Violeta Hernández]

For instance, in the order with A < C, B < C, both A and B are possible (weak) predecessors of C. But every element has a unique successor.

[Daniel Weber]

I think looking at it when it isn't unique feels a bit weird. What are some usecases for that? The only thing I can think of are path decompositions in trees

[Violeta Hernández]

I'm not really sure if there's a lot of use in the case where successors/predecessors aren't unique. The idea is rather, you can always build a WeakSuccOrder, and under extra conditions like having a SuccOrder or a LinearOrder, it will be unique and thus nicely behaved.

[Yaël Dillies]

Do we care about definitional equalities? If not, then we can define succ and pred for any preorder

[Violeta Hernández]

We definitely do care, having succ x = x + 1 on naturals / ordinals is super nice.

[Yaël Dillies]

Well actually it's not so nice since this definitional equality is not syntactical, and most of the succ-pred API is based on rewriting

[Yaël Dillies]

My suggestion of throwing away the defeqs for succ and pred would come along with a new typeclass AddSuccOrder stating succ x = x + 1 and providing the succ API translated to · + 1

[Violeta Hernández]

What would the instances of it be? Just Nat and Ordinal? Maybe ENat too

[Daniel Weber]

Also Int

[Violeta Hernández]

Well, def-eqs are overrated anyways. It would in fact be pretty nice to have succ and pred on arbitrary preorders.

[Yakov Pechersky]

But if they're not unique, how would you have it as a typeclass?

[Daniel Weber]

Path decompositions still are a valid use, so I don't think always defining it with choice is good

[Violeta Hernández]

Just thought of another disadvantage of defining them with choice like that: proving results of the form succ x = f x would be more annoying. You'd first have to construct the SuccOrder instance, probably using f indirectly, then argue separately that f satisfies the characterizing properties of succ and that it's thus equal.

[Yaël Dillies]

Doesn't that just mean you need another constructor?

[Violeta Hernández]

Hmm. I guess you could have a constructor for SuccOrder from an arbitrary successor function, and a theorem saying that succ equals the function that you passed in.

[Violeta Hernández]

But the typeclass approach is definitely cleaner.

[Violeta Hernández]

In my view at least

[Yaël Dillies]

I wouldn't be so sure! I think the typeclass-less approach is worth trying

[Violeta Hernández]

Something else I don't like is that we couldn't be able to easily state results like "WeakPredOrder is a subsingleton". We could only say that a function satisfying the properties of WeakPredOrder equals the one we chose through choice, which is mathematically the same but still a bit more contrived.

[Yaël Dillies]

Surely stating that instances are unique is more contrived than stating that successor functions are unique?

[Violeta Hernández]

Hm. I guess you can restate "there is a unique WeakPredOrder as "every element covers at most one other one" which is certainly much more natural.

[Violeta Hernández]

I'll make a draft PR for this, maybe this afternoon.

[Yaël Dillies]

I strongly suggest you first add SuccAddOrder so as not to lose the API for ℕ/ℤ/Ordinal

[Daniel Weber]

Do you think that path decompositions should be done separately, and not as weak successor orders?

[Yaël Dillies]

What do you mean, concretely?

[Daniel Weber]

On trees (PredOrder, IsPredArchimedean, OrderBot), a WeakSuccOrder is exactly a choice of a child for every non-leaf element, which is the same as a path decomposition

[Violeta Hernández]

I admit to not knowing what path decompositions are, but the Wikipedia article seems to suggest they're a graph rather than an order notion

[Kevin Buzzard]

I think the idea is that the edges go from x to succ x.

[Violeta Hernández]

Ah, I see. Yeah, I guess WeakPredOrder could be used for that. But these SuccOrder / PredOrder definitions are meant for use in orders, and there might be a better and more convenient way to state this for trees.

[Violeta Hernández]

Yaël Dillies said:

I strongly suggest you first add SuccAddOrder so as not to lose the API for ℕ/ℤ/Ordinal

The PR now exists at #16484. I was able to deprecate quite a few statements, so this might take a bit to build.

[Wrenna Robson]

Just managed to find this thread eventually to work out why some proof I had was breaking.

[Wrenna Robson]

(I had only assumed PartialOrder which of course no longer works.)

[Violeta Hernández]

I don't think anything ever came out of this?

[Violeta Hernández]

Except for SuccAddOrder

[Violeta Hernández]

(I abandoned my idea to generalize Pred to cover docs#Ordinal.pred once I realized that pred x = x - 1, which implies a different refactor should be happening instead)