feat(order/succ_pred/limit): predecessor from a succ_order

[vihdzp]

We define order.pred' such that order.pred' a = a for a successor limit a, and order.pred' (succ a) = a for a non-maximal element a. We prove that in an archimedean partial successor order, order.pred' satisfies the properties of an archimedean predecessor order. We then use this to golf the instances for nat and int.

This opens up the possibility for two future refactors:

• supercede ordinal.pred by the equivalent but more general order.pred'.
• unify is_succ_archimedean and is_pred_archimedean into a single typeclass, with constructors from either the successor or predecessor.

---

[YaelDillies]

Can you please inline pred' into succ_order.to_pred_order and get rid of the unnecessary lemmas (that is, all the ones that are not used to construct succ_order.to_pred_order )?

[vihdzp]

I would rather not inline pred'. As I mentioned, ordinal.pred is equivalent to my new order.pred', but ordinals aren't a succ-archimedean order. Which means that this definition is useful outside of that context.

I can separate the theorems not needed to prove succ_order.to_pred_order into a new PR, though.

[vihdzp]

Actually, I'd rather not even separate the "extra" lemmas. There's just three of them: pred'_bot, le_succ_pred', pred'_succ, and their order duals. And two of them are trivial.

[YaelDillies]

Yes, so you can do

instance : pred_order ordinal := succ_order.to_pred_order

pred' is equal to pred, you proved it yourself. You are not defining a new function, but writing a new constructor for succ_order. The lemmas about pred' are lemmas about a specific instantiation of pred and we already have them for a general pred.

[vihdzp]

I proved that pred' is equal to pred on a succ-archimedean order specifically. Which ordinals are not. You can't define a pred_order instance on ordinal since there's nowhere to send ω to.

Proof

[YaelDillies]

This to me suggests that pred_order is too strict. I designed it to allow orders with a bottom element, but you still get a problem when you're at a succ-limit. So possibly we could allow pred a = a when a is succ-limit (rather than merely minimal). But maybe any order would be a pred_order then?

[vihdzp]

I think the current definition for a pred_order is fine. It means that partial orders without minimum elements behave just as you'd expect, and partial orders with a minimum element behave almost as you'd expect with the exception of whatever happens on that minimum element.

If order.pred' were a valid predecessor function on a partial order as you suggest, then we would lose results like pred being injective and strictly antitone on unbounded orders. And without a typeclass for orders without successor limits (which seems too specific for my taste), we wouldn't be able to get them back in a nice form.

Further, any partial succ-order would also be a pred-order. At that point, given that we quote "don't care about preorders", we would have to consider merging succ_order and pred_order into a single class.

If you need the weaker notion of a predecessor that order.pred' allows, then this PR allows you to use that.

[YaelDillies]

... except that "a typeclass for orders without successor limits" is exactly very close to being is_succ_archimedean (they differ for ℤ ⊕ ℤ).

[vihdzp]

I think I can sum this issue up like this: do we expect that any succ_order should also be a pred_order? If yes, then these typeclasses should be merged into one and their assumptions changed accordingly. If not, then having order.pred' for the weaker notion of a predecessor should be fine.

Unless we feel really strongly about this issue, I'd rather take the path of least effort 😅

[vihdzp]

There's been some Zulip discussion regarding this PR. I'll draft it until we figure out what to do.