## 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

variable [linear_order R]

protected def add (x y : tropical R) : tropical R :=
trop (min (untrop x) (untrop y))

@[simp] lemma untrop_add (x y : tropical R) : untrop (x + y) = min (untrop x) (untrop y) := rfl

instance [linear_ordered_add_comm_monoid_with_top R] : comm_semiring (tropical R) :=
{ zero := trop ⊤,
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,

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,
-- 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

#### 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