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 :=
  refl -- nope

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

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₂ }
  ..with_top.order_top }


@[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