Complete lattice interval instances

Stream: general

[Peter Nelson]

As @Yury G. Kudryashov has identified, there is a diamond issue adding complete_lattice instances for the intervals Iic and Ici : see #15135 . The problem is that the Sup/Inf fields for these instances disagree with subset_has_Sup, which is in turn needed to provide conditionally complete order instances on ord_connected subsets via ord_connected_subset_conditionally_complete_linear_order. The function subset_has_Sup needs to use default in places where no Sup exists, whereas for Ici, it will always exist; this is why they're different.

See https://leanprover-community.github.io/mathlib_docs/order/complete_lattice_intervals.html#subset_has_Sup

I don't fully understand the design issues involved here, but not having global complete_lattice instances on Iic and Ici is quite a pain (I am using them in an upcoming sequence of PRs to add matroids to mathlib).

Is there is a good resolution to this?

[Eric Wieser]

Can't you just use the if-based definition of Sup in both places?

[Eric Wieser]

Yes, one branch of the if is unreachable in the case you describe, but that doesn't matter

[Eric Wieser]

Although I now notice that docs#subset_has_Sup is not an instance; so is there actually a diamond here?

[Peter Nelson]

I'm likely out of my depth here, so I'll leave Yury to comment. One disadvantage of defining Sup on an interval with dite is that the instance becomes noncomputable, whereas Sup (S : set (Ici a)) := a ⊔ Sup (coe '' S) is computable.

[Peter Nelson]

@Yury G. Kudryashov , does the fact that the conditional objects aren't global instances mitigate this problem?

[Yury G. Kudryashov]

The instance on an ord_connected set is a global instance.

[Yury G. Kudryashov]

See docs#ord_connected_subset_conditionally_complete_linear_order