semilattice_sup to directed_order

Stream: general

[Yaël Dillies]

Is there any reason we don't have this instance?

instance semilattice_sup.to_directed_order {α : Type*} [h : semilattice_sup α] :
  directed_order α :=
{ directed := λ a b,  ⟨a ⊔ b, le_sup_left, le_sup_right⟩,
  ..h }

[Yaël Dillies]

Supposedly it's strictly more general than linear_order.to_directed_order. Maybe that causes defeqness problems with lattice_of_linear_order?

[Riccardo Brasca]

I don't know the answer to your question, but you can check if there are defeqness problems just by testing if rfl proves that the two instances you are talking about are equal.

[Yaël Dillies]

example {α : Type*} [h : linear_order α] :
 @semilattice_sup.to_directed_order α (@lattice.to_semilattice_sup α (@lattice_of_linear_order α h))
 = @linear_order.to_directed_order α h :=
rfl

:tada:

[Adam Topaz]

It has been tried see #7980
Maybe the semilattice sup case only wouldn't cause such problems.. feel free to try it!

[Yaël Dillies]

Oooh, nice.

[Yaël Dillies]

I opened #9200. Let's see what happens.

[Yaël Dillies]

So I think that creates a problematic diamond?

[Yaël Dillies]

The current build fails because I have a lower_adjoint lemma that takes in preorders of the form partial_order.to_preorder, but the lower_adjoint coe I'm trying to apply it to has preorders of the form directed_order.to_preorder. Is that possibly the problem?

[Yaël Dillies]

It's quite unclear to me whether having derived instances (eg partial_order.to_preorder) appearing in definitions is bad. Will a derived instance only match the same derived instance? I'd assume it happens all the time, so probably that's fine?

[Yaël Dillies]

Yaël Dillies said:

So I think that creates a problematic diamond?

The diamond in question is

example {α : Type*} [h : semilattice_sup α] :
  @partial_order.to_preorder α (@semilattice_sup.to_partial_order α h) =
  @directed_order.to_preorder α (@semilattice_sup.to_directed_order α h) := rfl

[Yaël Dillies]

But it is defeq :thinking:

[Yaël Dillies]

Ahah! @Aaron Anderson, you used the wrong lower_adjoint lemma. I don't know how it still worked though. Probably some defeq abuse.
You did

lemma closure_le : closure L s ≤ S ↔ s ⊆ S := (closure L).closure_le_closed_iff_le s S.closed

but the goal type is ⇑(closure L) s ≤ S ↔ s ⊆ ↑S while lower_adjoint.closure_le_closed_iff_le s S.closed has type ↑(⇑(closure L) s) ≤ ↑S ↔ s ≤ ↑S. The correct thing here was

lemma closure_le : closure L s ≤ S ↔ s ⊆ S := (closure L).le_iff_subset s S

[Yaël Dillies]

Everything that fails here is because directed_order.to_preorder doesn't match with partial_order.to_preorder (even though they are defeq) when applying lemmas. Adding semilattice_sup.to_directed_order doesn't cause the problem. It just makes one path more direct.