behaviour of `linarith`

Stream: new members

[Jujian Zhang]

Is linarith meant to solve the following? If not, what is the tactic? (Assuming, the following example is true for every linear ordered cancel add comm monoid)

import tactic.linarith

example (A : Type) [linear_ordered_cancel_add_comm_monoid A] (a b c d : A) (h1 : a < c) (h2 : b < d) : a + b < c + d :=
by linarith

Thank you!

[Ruben Van de Velde]

Not sure if linarith should solve it, but it's true:

example (A : Type) [linear_ordered_cancel_add_comm_monoid A] (a b c d : A) (h1 : a < c) (h2 : b < d) : a + b < c + d :=
by { apply add_lt_add; assumption }

[Jujian Zhang]

In the above example maybe linear_ordered_cancel_add_comm_monoid is too strong because we are not actually cancelling anything.

import tactic.linarith

example (A : Type) [linear_ordered_cancel_add_comm_monoid A]
(a b c d : A) (h1 : a + b = c + d) (h2 : a < c) : d < b := by linarith

This example would be slightly more painful to write it by hand.

[Rob Lewis]

The algorithm linarith implements needs extra type class assumptions.

import tactic.linarith
import tactic.abel

example (A : Type) [linear_ordered_comm_ring A]
(a b c d : A) (h1 : a + b = c + d) (h2 : a < c) : d < b := by linarith