linarith

Summary

The linarith tactic solves certain kind of linear equalities and inequalities. Unlike the ring tactic, linarith uses hypotheses in the tactic state. It’s very handy for epsilon-delta proofs.

Examples

If your local context looks like this:

a b c d : ℝ
h1 : a < b
h2 : b ≤ c
h3 : c = d
⊢ a + a < d + b

then you would like to say that the goal “obviously” follows from the conclusions. but actually proving it from first principles is a little bit messy, and will involve knowing or discovering the names of lemmas such as lt_of_lt_of_le and add_lt_add. Fortunately, you don’t have to do this: linarith closes this goal immediately. Note that in contrast to ring, linarith does have access to the hypotheses in your local context.

If you have a goal of the form |x| < ε then linarith might not be much help yet, because it doesn’t know about absolute values. So you could rw abs_lt and get a goal of the form -ε < x ∧ x < ε. Well, linarith still won’t be of any help, because it doesn’t know about goals with ∧ in either! However after you split, perhaps linarith will be able to help you.

import tactic
import data.real.basic

example (x ε : ℝ) (hε : 0 < ε) (h1 : x < ε / 2) (h2 : -x < ε / 2) : |x| < ε :=
begin
  rw abs_lt, -- `⊢ -ε < x ∧ x < ε`
  split; -- semicolon instead of comma means "do next tactic on all the goals this tactic produces"
  linarith -- solves both goals
end