Another with_top diamond

Stream: new members

[Yakov Pechersky]

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]

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]

Does making with_top semireducible fix this one?

[Yakov Pechersky]

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]

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]

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]

What are the conflicting inf definitions?

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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]

There might already be a PR about that instance

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Rodriguez]

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