# Zulip Chat Archive

## Stream: new members

### Topic: Another with_top diamond

#### Yakov Pechersky (Sep 01 2021 at 21:25):

For the mathlib sleuths:

```
import order.bounded_lattice
universe u
variables (R : Type*) [linear_order R]
def LHS : semilattice_inf (with_top R) :=
@lattice.to_semilattice_inf _ (@lattice_of_linear_order (with_top R) with_top.linear_order)
def RHS : semilattice_inf (with_top R) :=
@semilattice_inf_top.to_semilattice_inf (with_top R) with_top.semilattice_inf
example : LHS R = RHS R :=
begin
refl -- nope
end
```

#### Yakov Pechersky (Sep 01 2021 at 22:49):

In particular, it seems like a lower priority instance is appearing when it shouldn't:

```
import algebra.ordered_ring
import topology.algebra.polynomial
import analysis.convex.basic
universes u v
variables (R : Type u)
def tropical : Type u := R
variable {R}
@[pp_nodot] def trop : R → tropical R := id
@[pp_nodot] def untrop : tropical R → R := id
section add
variable [linear_order R]
protected def add (x y : tropical R) : tropical R :=
trop (min (untrop x) (untrop y))
instance add_inst : add_comm_semigroup (tropical R) :=
{ add := add,
add_assoc := sorry,
add_comm := sorry }
@[simp] lemma untrop_add (x y : tropical R) : untrop (x + y) = min (untrop x) (untrop y) := rfl
end add
instance [linear_ordered_add_comm_monoid_with_top R] : comm_semiring (tropical R) :=
{ zero := trop ⊤,
zero_add := sorry,
add_zero := sorry,
mul := λ x y, trop (x + y),
left_distrib := sorry,
right_distrib := sorry,
zero_mul := sorry,
mul_zero := sorry,
mul_assoc := sorry,
mul_comm := sorry,
one := trop 0,
one_mul := sorry,
mul_one := sorry,
..add_inst }
variables [decidable_eq R] [nontrivial R]
variables [linear_ordered_semiring R] [no_zero_divisors R]
instance shortcut : linear_ordered_add_comm_monoid R :=
{ ..(show (linear_ordered_semiring R), from infer_instance) }
open polynomial
@[simp] def polynomial.eval_tropical_aux (p : polynomial (tropical (with_top R))) (x : R) :
tropical (with_top R) :=
eval (trop (x : with_top R)) p
def polynomial.eval_tropical' (p : polynomial (tropical (with_top R))) (x : R) :
with_top R :=
untrop (p.eval_tropical_aux x)
lemma eval_tropical'_add (p q : polynomial (tropical (with_top R))) :
(p + q).eval_tropical' = p.eval_tropical' ⊓ q.eval_tropical' :=
funext $ λ _, by { simp only [polynomial.eval_tropical', untrop_add,
inf_apply, untrop_add, eval_add, polynomial.eval_tropical_aux],
-- why is this necessary, where is the lower-prio instance coming from
convert inf_eq_min.symm,
refine semilattice_inf.ext _,
simp }
```

#### Eric Wieser (Sep 02 2021 at 04:25):

Does making with_top semireducible fix this one?

#### Yakov Pechersky (Sep 02 2021 at 05:11):

No, there are truly incompatible `inf`

definitions as far as I understand. I just don't know why in my bigger example, it is choosing to use the lower prio instance.

#### Yakov Pechersky (Sep 02 2021 at 05:13):

Of course one can get past this by using `semilattice_inf.ext`

, and in another case, doing `attribute [ext] has_inf`

and doing a

```
ext x y z : 4,
convert rfl,
refine lattice.ext _,
simp
```

but I still don't know why it's using the other instance.

#### Eric Wieser (Sep 02 2021 at 05:15):

Instance priority isn't an appropriate tool for diamonds, because the instance that ends up in an expression varies according to the way in which intermediate definitions weaken stronger typeclasses

#### Eric Wieser (Sep 02 2021 at 05:16):

What are the conflicting inf definitions?

#### Eric Wieser (Sep 02 2021 at 05:17):

You can probably find out by applying `@semilattice_inf.inf _`

to either side of your original mwe, and then using dsimp with some steering

#### Yakov Pechersky (Sep 02 2021 at 05:17):

```
instance semilattice_inf [semilattice_inf α] : semilattice_inf_top (with_top α) :=
{ inf := option.lift_or_get (⊓),
inf_le_left := λ o₁ o₂ a ha,
by cases ha; cases o₂; simp [option.lift_or_get],
inf_le_right := λ o₁ o₂ a ha,
by cases ha; cases o₁; simp [option.lift_or_get],
le_inf := λ o₁ o₂ o₃ h₁ h₂ a ha, begin
cases o₂ with b; cases o₃ with c; cases ha,
{ exact h₂ a rfl },
{ exact h₁ a rfl },
{ rcases h₁ b rfl with ⟨d, ⟨⟩, h₁'⟩,
simp at h₂,
exact ⟨d, rfl, le_inf h₁' h₂⟩ }
end,
..with_top.order_top }
```

and

```
@[priority 100] -- see Note [lower instance priority]
instance lattice_of_linear_order {α : Type u} [o : linear_order α] :
lattice α :=
{ sup := max,
le_sup_left := le_max_left,
le_sup_right := le_max_right,
sup_le := assume a b c, max_le,
inf := min,
inf_le_left := min_le_left,
inf_le_right := min_le_right,
le_inf := assume a b c, le_min,
..o }
```

#### Yakov Pechersky (Sep 02 2021 at 05:18):

where the `le`

that is used for `min`

is

```
instance [preorder α] : preorder (with_top α) :=
{ le := λ o₁ o₂ : option α, ∀ a ∈ o₂, ∃ b ∈ o₁, b ≤ a,
lt := (<),
lt_iff_le_not_le := by { intros; cases a; cases b;
simp [lt_iff_le_not_le]; simp [(<),(≤)] },
le_refl := λ o a ha, ⟨a, ha, le_refl _⟩,
le_trans := λ o₁ o₂ o₃ h₁ h₂ c hc,
let ⟨b, hb, bc⟩ := h₂ c hc, ⟨a, ha, ab⟩ := h₁ b hb in
⟨a, ha, le_trans ab bc⟩,
}
```

#### Eric Wieser (Sep 02 2021 at 05:19):

Can you do the dsimp I suggest and see what things unfold to?

#### Eric Wieser (Sep 02 2021 at 05:20):

I'm pretty sure `lattice_of_linear_order`

is to blame here, and the resolution would be to make sup and inf fields of linear_order

#### Eric Wieser (Sep 02 2021 at 05:21):

There might already be a PR about that instance

#### Yakov Pechersky (Sep 02 2021 at 05:21):

Sorry, I won't be able to get to running the experiment for several hours.

#### Eric Wieser (Sep 02 2021 at 09:54):

lean#609 fixed this diamond, we just need to wait for a lean release.

#### Eric Rodriguez (Sep 02 2021 at 20:34):

I've got some light work on this in branch#max-min-fix, but currently as there's no release you'll need to build locally to work on it

Last updated: Dec 20 2023 at 11:08 UTC