Improvements to OmegaCompletePartialOrder.lean

Stream: mathlib4

[Anthony Vandikas]

As part of the work @Kiarash Sotoudeh and I have been doing on formalizing (ω) quasi-borel spaces, we have been filling in some missing functionality that I believe belongs in OmegaCompletePartialOrder.lean. This includes:

• Teaching fun_prop about ωScottContinuous functions.
• OmegaCompletePartialOrder instances for Option, Sum, and Sigma.
• Various Chain constructions necessary for the aforementioned instances.
• ωScottContinuous proofs for various basic functions (e.g., Prod.fst, ite, ...).

Is this appropriate for mathlib? I've made an initial PR for the first item (#33941).

[Ruben Van de Velde]

Sounds welcome, yeah

[Yaël Dillies]

Sure, yes! Feel free to request my review in case the other reviewing avenues become too slow

[Chris Henson]

This will be appreciated downstream as well, where it will be useful for programming language semantics!

One question I have about OmegaCompletePartialOrder instances for Option α (and WithBot α) is that sometimes we would like the "flat" ωCPO where we just have ⊥ ≤ (a : α) and ignore the ordering on α. Can we scope things so that users can choose what instances they want?

[Yaël Dillies]

Shouldn't that be the order on WithBot (Discrete α) instead?

[Anthony Vandikas]

Part behaves like this and already has an OmegaCompletePartialOrder instance.

[Violeta Hernández]

I thought Part was discouraged if not outright deprecated.

[Chris Henson]

Violeta Hernández said:

I thought Part was discouraged if not outright deprecated.

Part does have the instance I meant, but I similarly had the impression that WithBot was the preferred way to attach a bottom element. Yaël's suggestion of WithBot (Discrete α) seems very nice mathematically, though I don't know at a glance if universes will be an annoyance.

[Anthony Vandikas]

Violeta Hernández said:

I thought Part was discouraged if not outright deprecated.

Is this documented somewhere? Closest I could find is #mathlib4 > deprecate Mathlib.Data.Nat.PartENat?, and I am not sure that the consensus was to remove Part (at most, it looks like it would be moved to batteries).

---

I have submitted another PR #33985 containing the OmegaCompletePartialOrder instance for Sum.

[Violeta Hernández]

Assuming choice, Part is entirely equivalent to Option, which has much more API. And the consensus (though not universal) is that Mathlib shouldn't bother much with constructivism or decidability.

[Aaron Liu]

I don't like Part for a different reason, because it's not the right definition for computations that have the potential to run on forever but are otherwise safe.

[Anthony Vandikas]

I have made two more PRs: #34054 for the Sigma instance and #34093 for Option instance.

I expect that I should split up OmegaCompletePartialOrder.lean before any further work as it is getting quite long.

Yaël Dillies said:

Sure, yes! Feel free to request my review in case the other reviewing avenues become too slow

If it's not too much trouble I'd like to take you up on your offer (apologies if a week is too soon, this is my first experience making a PR here :smile:).