## Stream: general

### Topic: mono losing power in special case

#### Heather Macbeth (Mar 28 2022 at 00:39):

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 (Mar 28 2022 at 00:57):

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 (Mar 28 2022 at 01:02):

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 (Mar 28 2022 at 01:06):

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 (Mar 28 2022 at 01:09):

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


Last updated: Dec 20 2023 at 11:08 UTC