Diamond in instances on `with_top R`

Stream: new members

[Yakov Pechersky]

I'm hitting a diamond trying to define and use reasonable instances on with_top R. Can diamond/mul_action experts chime in possibly?

type mismatch at application
  concave_on' R
term
  with_top.distrib_mul_action R
has type
  @distrib_mul_action R (with_top R)
    (@monoid_with_zero.to_monoid R
       (@semiring.to_monoid_with_zero R
          (@ordered_semiring.to_semiring R (@linear_ordered_semiring.to_ordered_semiring R _inst_2))))
    (@with_top.add_monoid R
       (@add_comm_monoid.to_add_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R (@linear_ordered_semiring.to_ordered_semiring R _inst_2)))))))
but is expected to have type
  @distrib_mul_action R (with_top R)
    (@monoid_with_zero.to_monoid R
       (@semiring.to_monoid_with_zero R
          (@ordered_semiring.to_semiring R (@linear_ordered_semiring.to_ordered_semiring R _inst_2))))
    (@add_comm_monoid.to_add_monoid (with_top R)
       (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   (@linear_ordered_semiring.to_ordered_semiring R _inst_2))))))

[Yakov Pechersky]

I'll include a mwe in a minute.

[Yakov Pechersky]

On branch#pechersky/tropical-semiring,

import algebra.ordered_ring
import algebra.tropical.basic
import data.polynomial.basic

universe u

variables {R : Type*} [decidable_eq R]

instance [has_zero R] [has_mul R] : has_scalar R (with_top R) :=
⟨λ k x, (k : with_top R) * x⟩

lemma with_top.smul_def [has_zero R] [has_mul R] (k : R) (x : with_top R) :
  k • x = (k : with_top R) * x := rfl

@[simp] lemma with_top.smul_coe [has_zero R] [has_mul R] (k x : R) :
  k • (x : with_top R) = (k : with_top R) * x := rfl

@[simp] lemma with_top.zero_smul [has_zero R] [has_mul R] (x : with_top R) :
  (0 : R) • x = 0 := zero_mul x

@[simp] lemma with_top.smul_zero [has_zero R] [has_mul R] (k : R) :
  k • (0 : with_top R) = 0 := mul_zero k

lemma with_top.smul_top_of_ne_zero [has_zero R] [has_mul R] {k : R} (hk : k ≠ 0) :
  k • (⊤ : with_top R) = ⊤ :=
begin
  by_cases H : (⊤ : with_top R) = 0,
  { simp [H] },
  { refine if_neg _,
    simpa using hk }
end

variable (R)

instance [monoid_with_zero R] [no_zero_divisors R] [nontrivial R] : mul_action R (with_top R) :=
{ one_smul := by simp [with_top.smul_def],
  mul_smul := by simp [with_top.smul_def, with_top.coe_mul, mul_assoc],
  ..with_top.has_scalar }

instance [semiring R] [no_zero_divisors R] [nontrivial R] :
  distrib_mul_action R (with_top R) :=
{ smul_add := λ r x y, by {
    rcases eq_or_ne r 0 with rfl|hr,
    { simp },
    induction x using with_top.rec_top_coe,
    { simp [with_top.smul_top_of_ne_zero hr] },
    induction y using with_top.rec_top_coe,
    { simp [with_top.smul_top_of_ne_zero hr] },
    { rw [←with_top.coe_add, with_top.smul_coe, ←with_top.coe_mul, mul_add],
      simp [with_top.coe_mul, with_top.coe_add] } },
  smul_zero := λ _, mul_zero _,
  ..with_top.mul_action R }

section concave

variables {E S β : Type*} [add_comm_monoid E] [ordered_add_comm_monoid β]

variable (S)

def convex' [linear_ordered_semiring S] [distrib_mul_action S E] (s : set E) :=
∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : S⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
  a • x + b • y ∈ s

/-- Concavity of functions -/
def concave_on' [linear_ordered_semiring S] [distrib_mul_action S E] [distrib_mul_action S β]
  (s : set E) (f : E → β) : Prop :=
  convex' S s ∧
  ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : S⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
    a • f x + b • f y ≤ f (a • x + b • y)

variables {S} [linear_ordered_semiring S] [distrib_mul_action S E] [has_scalar S E]

lemma convex'_univ : convex' S (set.univ : set E) :=
λ _ _ _ _ _ _ _ _ _, trivial

end concave

instance linear_ordered_semiring.to_linear_ordered_add_comm_monoid {R : Type*}
  [h : linear_ordered_semiring R] : linear_ordered_add_comm_monoid R :=
{ ..h }

variables [linear_ordered_semiring R] [no_zero_divisors R]

example : distrib_mul_action R (with_top R) := with_top.distrib_mul_action R

def polynomial.eval_tropical' (p : polynomial (tropical (with_top R))) : R → R := sorry

lemma concave_on_eval_tropical' (p : polynomial (tropical (with_top R))) :
  @concave_on' R R (with_top R) _ _ _ _ (with_top.distrib_mul_action R) set.univ p.eval_tropical' :=
  sorry

[Eric Wieser]

Looking at the erro message only, it looks like there are two different add_comm_monoid structures on with_top R.

What's _inst_2 in that context?

[Yakov Pechersky]

linear_ordered_semiring R

[Sebastien Gouezel]

Reduced just a little bit:

import algebra.ordered_ring
variables {R : Type*} [h : ordered_semiring R]

lemma fails : (@with_top.add_comm_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
rfl

[Eric Wieser]

Is that on master?

[Eric Wieser]

Perhaps the nsmul actions are not defeq?

[Sebastien Gouezel]

Yes, it's on master.

[Sebastien Gouezel]

The nsmul structures are the same:

lemma works : @add_comm_monoid.nsmul _ (@with_top.add_comm_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       @add_comm_monoid.nsmul _ (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
rfl

So are the add fields and the zero fields...

[Sebastien Gouezel]

But the nsmul_zero' is not:

lemma fails : @add_comm_monoid.nsmul_zero' _ (@with_top.add_comm_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       @add_comm_monoid.nsmul_zero' _ (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
rfl

Since nsmul_zero' is ∀ x, nsmul 0 x = 0 . try_refl_tac, this looks like our old problem with pi types, or try_refl_tac is confusing Lean somewhere.

[Yakov Pechersky]

Do we need to have definitional equality of propositions to have defeq of structures?

[Yakov Pechersky]

Or is it that the . try_refl_tac is somehow preventing proof_irrel from firing?

[Yakov Pechersky]

This is a question for lean4 experts then as well -- would we hit this diamond in current lean4? @Mario Carneiro

[Mario Carneiro]

Unclear, can you make a smaller example?

[Mario Carneiro]

it sounds like a bug

[Yakov Pechersky]

We have

instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
{ zero := 0,
  add := (+),
  ..@additive.add_comm_monoid _ $ @comm_monoid_with_zero.to_comm_monoid _ $
    @with_zero.comm_monoid_with_zero (multiplicative α) _ }

Maybe this issue has to do with the defeq abuse around using with_zero. Checking that.

[Mario Carneiro]

a mathlib free example would be good

[Yakov Pechersky]

Working on making that. In the meantime, I have the following:

type mismatch at application
  add_comm_monoid.nsmul_zero' = add_comm_monoid.nsmul_zero'
term
  add_comm_monoid.nsmul_zero'
has type
  auto_param
    (∀ (x : with_top R),
       @add_comm_monoid.nsmul (with_top R)
           (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
              (@with_top.ordered_add_comm_monoid R
                 (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                    (@ordered_semiring.to_ordered_cancel_add_comm_monoid R h))))
           0
           x =
         0)
    (name.mk_string "try_refl_tac" name.anonymous)
but is expected to have type
  auto_param
    (∀ (x : with_top R),
       @add_comm_monoid.nsmul (with_top R)
           (@with_top.add_comm_monoid' R
              (@non_unital_non_assoc_semiring.to_add_comm_monoid R
                 (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                    (@semiring.to_non_assoc_semiring R (@ordered_semiring.to_semiring R h)))))
           0
           x =
         0)
    (name.mk_string "try_refl_tac" name.anonymous)

[Eric Wieser]

Oh, I assumed from the message above that simply rfl could not prove the result, not that the statement was ill-formed

[Yakov Pechersky]

This is from me trying to undo the definition of the algebraic instances from additive (with_zero ...) but manually.

[Eric Wieser]

Elaborating on Sebastien's post:

import algebra.ordered_ring
variables {R : Type*} [h : ordered_semiring R]

lemma with_irrel : @add_comm_monoid.nsmul_zero' _ (@with_top.add_comm_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       @add_comm_monoid.nsmul_zero' _ (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
proof_irrel _ _ -- ok

lemma with_rfl : @add_comm_monoid.nsmul_zero' _ (@with_top.add_comm_monoid R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       @add_comm_monoid.nsmul_zero' _ (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
rfl  -- fails

[Eric Wieser]

(λ (h₁ h₂ : (_ : Prop)), show h₁ = h₂, from rfl) _ _ works as a proof too

[Yakov Pechersky]

Yes, I think this is due to the (ab)use of defeq via with_zero:

import algebra.ordered_ring
variables {α R : Type*} [h : ordered_semiring R]

local attribute [-instance] with_top.add_semigroup with_top.add_comm_semigroup with_top.add_monoid
  with_top.add_comm_monoid with_top.ordered_add_comm_monoid

instance with_top.add_semigroup' [add_semigroup α] : add_semigroup (with_top α) :=
{ add_assoc :=
  begin
    refine with_top.rec_top_coe _ _,
    simp [←with_top.coe_add, add_assoc],
    intro, refine with_top.rec_top_coe _ _;
    simp [←with_top.coe_add, add_assoc],
    intro, refine with_top.rec_top_coe _ _;
    simp [←with_top.coe_add, add_assoc]
  end,
  ..with_top.has_add }

instance with_top.add_comm_semigroup' [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
{ add_comm :=
  begin
    refine with_top.rec_top_coe _ _,
    simp [←with_top.coe_add, add_comm],
    intro, refine with_top.rec_top_coe _ _;
    simp [←with_top.coe_add, add_comm]
  end,
  ..with_top.add_semigroup' }

instance with_top.add_monoid' [add_monoid α] : add_monoid (with_top α) :=
{ zero_add :=
  begin
    refine with_top.rec_top_coe _ _,
    { simpa },
    { intro,
      rw [←with_top.coe_zero, ←with_top.coe_add, zero_add] }
  end,
  add_zero :=
  begin
    refine with_top.rec_top_coe _ _,
    { simpa },
    { intro,
      rw [←with_top.coe_zero, ←with_top.coe_add, add_zero] }
  end,
  ..with_top.has_zero,
  ..with_top.add_semigroup' }


instance with_top.add_comm_monoid' [add_comm_monoid α] : add_comm_monoid (with_top α) :=
{ ..with_top.add_monoid', ..with_top.add_comm_semigroup' }

instance with_top.ordered_add_comm_monoid' [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
{ add_le_add_left :=
    begin
      rintros a b h (_|c), { simp [with_top.none_eq_top] },
      rcases b with (_|b), { simp [with_top.none_eq_top] },
      rcases with_top.le_coe_iff.1 h with ⟨a, rfl, h⟩,
      simp only [with_top.some_eq_coe, ← with_top.coe_add, with_top.coe_le_coe] at h ⊢,
      exact add_le_add_left h c
    end,
  lt_of_add_lt_add_left :=
    begin
      intros a b c h,
      rcases with_top.lt_iff_exists_coe.1 h with ⟨ab, hab, hlt⟩,
      rcases with_top.add_eq_coe.1 hab with ⟨a, b, rfl, rfl, rfl⟩,
      rw with_top.coe_lt_iff,
      rintro c rfl,
      exact lt_of_add_lt_add_left (with_top.coe_lt_coe.1 hlt)
    end,
  ..with_top.partial_order, ..with_top.add_comm_monoid' }

lemma no_longer_fails : (@with_top.add_comm_monoid' R
          (@non_unital_non_assoc_semiring.to_add_comm_monoid R
             (@non_assoc_semiring.to_non_unital_non_assoc_semiring R
                (@semiring.to_non_assoc_semiring R
                   (@ordered_semiring.to_semiring R h)))))
        =
       (@ordered_add_comm_monoid.to_add_comm_monoid (with_top R)
          (@with_top.ordered_add_comm_monoid' R
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid R
                (@ordered_semiring.to_ordered_cancel_add_comm_monoid R
                   h)))) :=
rfl

[Eric Wieser]

Adding attribute [semireducible] with_zero to the mwe fixes it (with_zero is irreducible)

[Eric Wieser]

So this is the tensor_algebra.ring problem resurfacing

[Yakov Pechersky]

#8926

[Yakov Pechersky]

Link for the tensor_algebra.ring issue tracker?

[Eric Wieser]

No issue, but we have these comments:

• https://github.com/leanprover-community/mathlib/blob/1e89df22bbce32e6f6fea2c95d6aa52dfadef012/src/algebra/free_algebra.lean#L287-L289
• https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/tensor_algebra.lean#L106-L109
• https://github.com/leanprover-community/mathlib/blob/1e89df22bbce32e6f6fea2c95d6aa52dfadef012/src/linear_algebra/exterior_algebra.lean#L140-L142

which link to this Zulip thread