linarith failing on simple inequality proofs

Stream: new members

[Rado Kirov]

I have been relying heavily on linarith for some quite complicated proofs involving inequalities. To my surprise, sometimes it fails on much simpler ones. Here are two examples:

example {a b c: ℚ} (ha: a > 0) (hbc: b * c < 0): a * (b * c) < 0 := by linarith -- fails

example {a b c: ℚ} (ha: a > 0) (hbc : b * c > 0) : a * (c * b) > 0 := by linarith  -- fails (but works if simp_all first)

Is this expected? I wonder if some of those are bugs/improvements for linarith but I am not even sure if this is all working as expected or not, before I file github issues.

[Ruben Van de Velde]

Have you tried nlinarith?

[Rado Kirov]

nope, first time I heard about it.

[Aaron Liu]

Rado Kirov said:

I have been relying heavily on linarith for some quite complicated proofs involving inequalities. To my surprise, sometimes it fails on much simpler ones. Here are two examples:

example {a b c: ℚ} (ha: a > 0) (hbc: b * c < 0): a * (b * c) < 0 := by linarith -- fails

example {a b c: ℚ} (ha: a > 0) (hbc : b * c > 0) : a * (c * b) > 0 := by linarith  -- fails (but works if simp_all first)

Is this expected? I wonder if some of those are bugs/improvements for linarith but I am not even sure if this is all working as expected or not, before I file github issues.

Well in this case it's not linear arithmetic anymore, since you have multiplication by a variable (as opposed to a numeric literal)

[Rado Kirov]

nlinarith does close these, which is great.

The comment about these not being linear made sense, so I tried to add set d := b * c first, but to my surprise, even this is too much for plain linarith

example {a b: ℚ} (ha: a > 0) (hb: b < 0): a * b < 0 := by linarith -- can't close

playground

[Aaron Liu]

Well you still have multiplication of variables, it's still not linear

[Rado Kirov]

I see the conclusion needs to be linear combination of hypothesis too.