mono losing power in special case

Stream: general

[Heather Macbeth]

I hit the following odd behaviour in mono today:

import tactic.monotonicity

variables {α : Type*} [linear_ordered_ring α]

example {a b c d : α} : a * c ≤ b * d :=
begin
  mono*, -- takes action
end

example {a b c d : α} : a * c ≤ b * c :=
begin
  mono*, -- doesn't take action
end

I don't see why mono should do something in the first (strictly more general) case but not the second. Unless it's that there's some other, ultimately unhelpful, lemma which it tries to apply in the second case but gets "blocked" on, and that lemma doesn't apply in the more general first case?

[Kyle Miller]

If you remove the * in the second case, it looks like it reports an error:

/-
12:3: ambiguous match:

mul_mono_nonpos
c ≤ 0
b ≤ a

mul_mono_nonneg
0 ≤ c
a ≤ b

Tip: try asserting a side condition to distinguish between the lemmas
-/

[Heather Macbeth]

That's very interesting, because there ought even to be three lemmas among which it's ambiguous, not just two: there's also the lemma docs#mul_le_mul, which is the one applied in the first case.

[Kyle Miller]

There seems to be a disambiguation engine that ranks possibilities -- maybe that one didn't make the cut?

(mono with a ≤ b, seems to work for the second one.)

[Heather Macbeth]

Interestingly, the behaviour is not stable under order of multiplication

example {a b c : α} : a * c ≤ b * c :=
begin
  mono*, -- doesn't take action
end

example {a b c : α} : c * a ≤ c * b :=
begin
  mono*, -- takes action
end