OmegaCompletePartialOrder doesn't need a partial order

Stream: mathlib4

[Jad Ghalayini]

Hello! I am once again formalizing programming languages in Lean, and I have a somewhat irritating nit:

• I have a language whose initial semantics is a _preorder_; we quotient later!
• Which is in fact an omega-complete _preorder_
• But OmegaCompletePartialOrder requires things to be a PartialOrder

The issue is that it turns out it's very helpful to have the OmegaCompletePartialOrder API on both the pre-semantics and the semantics, so we can relate them. And there's nothing about omega-chains which says they need to be on a partial order rather than a preorder (though of course on a preorder ωSup makes a _choice_ of chain!)

Any nice way to deal with this?

One option might be to move the ωSup notation to another typeclass (say, OmegaSup) which only depends on LE, like for Inf and Sup, and then have an OmegaCompletePreorder class which takes a [Preorder] parameter and finally have OmegaCompletePartialOrder extend PartialOrder and OmegaCompletePreorder?

Or we could simplify and just do OmegaCompletePreorder with ωSup

I think most of the theorems in the file remain true for OmegaCompletePreorder with no additional changes.

Later PRs could then weaken many of the preconditions in Mathlib.Order.FixedPoints to OmegaCompletePreorder (since this doesn't extend anything this should be forwards-compatible); and the file is only used in Mathlib.SetTheory.Cardinal.SchroederBernstein.

This would help a lot with some of my formalization work!

Thoughts?

[Kim Morrison]

Seems fine.