Module 5 · Lesson 4

linarith — Linear Arithmetic

Solve linear arithmetic goals over ordered rings. linarithhandles inequalities and equalities involving addition and scalar multiplication. When you have a chain of inequalities and need to derive a conclusion, linarith finds the proof automatically.

❗

linarith requires Mathlib. Add import Mathlib.Tactic.Linarith to use this tactic.

The Problem linarith Solves

Suppose you know x < y and y < z, and need to prove x < z. This is "obviously" true by transitivity, but spelling it out in Lean requires finding and applying the right lemmas. linarith handles this automatically—and much more complex chains too:

lean

1import Mathlib.Tactic.Linarith
2
3-- Simple transitivity
4example (x y z : Int) (h1 : x < y) (h2 : y < z) : x < z := by linarith
5
6-- More complex chains
7example (a b c d e : Int) 
8    (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) (h4 : d < e) 
9    : a < e := by linarith
10
11-- Combining many constraints
12example (x y z : Int) 
13    (h1 : x + y ≤ 10) (h2 : y + z ≤ 10) (h3 : z + x ≤ 10) 
14    : x + y + z ≤ 15 := by linarith

Basic Usage

linarith automatically proves goals that follow from linear arithmetic over ordered rings. It examines all hypotheses involving addition, subtraction, and scalar multiplication, then determines if the goal follows logically.

lean

1import Mathlib.Tactic.Linarith
2
3-- Basic inequalities
4example (x y : Int) (h1 : x < y) (h2 : y < x + 2) : y = x + 1 := by
5  linarith
6
7example (a b c : Int) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
8  linarith
9
10example (x : Int) (h : x > 0) : x ≥ 1 := by
11  linarith
12
13-- Works with equalities too
14example (a b : Int) (h1 : a ≤ b) (h2 : b ≤ a) : a = b := by
15  linarith

Key Takeaway

linarith proves goals by finding linear combinations of hypotheses that establish the result. It automatically uses all relevant inequalities in your context.

Understanding "Linear"

Like omega, linarith handles linear expressions—where variables appear with degree 1. You can have 3 * x but notx * y or x².

lean

1import Mathlib.Tactic.Linarith
2
3-- ✅ Linear: coefficients are constants
4example (x y : Int) (h : 3*x + 2*y ≤ 10) (hx : x ≥ 0) (hy : y ≥ 0) : x ≤ 3 := by
5  linarith
6
7-- ✅ Subtraction and negation are fine
8example (a b : Int) (h : a ≤ b) : -b ≤ -a := by linarith
9
10-- ❌ Non-linear: variable times variable
11-- example (x y : Int) : x * y = y * x := by linarith  -- Fails!
12
13-- ❌ Non-linear: squaring
14-- example (x : Int) : x^2 ≥ 0 := by linarith  -- Fails!

How linarith Reasons

Under the hood, linarith finds a linear combination of your hypotheses that implies the goal. It multiplies inequalities by non-negative constants and adds them together:

lean

1import Mathlib.Tactic.Linarith
2
3-- Example: Prove a ≤ c from a ≤ b and b ≤ c
4-- linarith adds: 1*(a ≤ b) + 1*(b ≤ c) gives a ≤ c
5
6example (a b c : Int) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by linarith
7
8-- Example: Prove x ≤ 3 from x + y ≤ 5 and y ≥ 2
9-- linarith uses: (x + y ≤ 5) + (-1)*(y ≥ 2) which gives x ≤ 3
10
11example (x y : Int) (h1 : x + y ≤ 5) (h2 : y ≥ 2) : x ≤ 3 := by linarith

Proving False from Contradictions

A powerful use case is proving False when your hypotheses are contradictory. If the constraints are impossible to satisfy simultaneously,linarith finds the contradiction:

lean

1import Mathlib.Tactic.Linarith
2
3-- Direct contradiction
4example (x : Int) (h1 : x > 5) (h2 : x < 3) : False := by linarith
5
6-- More subtle: these three together are impossible
7example (a b c : Int) 
8    (h1 : a + b > c) 
9    (h2 : b + c > a) 
10    (h3 : c + a > b)
11    (h4 : a + b + c ≤ 0) : False := by linarith
12
13-- Finding implicit contradictions
14example (x y : Int) (h1 : x > y) (h2 : y > x) : False := by linarith

linarith vs omega

Both tactics handle linear arithmetic, but they have different strengths:

Feature	omega	linarith
Part of	Lean 4 core	Mathlib
Nat support	✅ Excellent	⚠️ Often needs omega
Int support	✅ Good	✅ Excellent
Rat/Real support	❌ No	✅ Yes
Div/mod	✅ Yes	❌ No
Disjunctions	✅ Yes	❌ No

💡

For Nat arithmetic, preferomega (core Lean 4). Use linarithfor Int, Rat, andReal.

Working with Different Types

lean

1import Mathlib.Tactic.Linarith
2
3-- Integers
4example (x y : Int) (h : x ≤ y) : -y ≤ -x := by linarith
5
6-- Rationals
7example (p q : Rat) (h1 : p ≤ q) (h2 : q ≤ p) : p = q := by linarith
8
9-- With Mathlib, also works on:
10-- ℝ (reals), ℚ (rationals), and other ordered rings

Providing Extra Hypotheses

Sometimes linarith needs extra facts that aren't in your context. You can provide them in brackets:

lean

1import Mathlib.Tactic.Linarith
2
3-- Provide additional lemmas in brackets
4example (x y : Int) (h : x * x + y * y = 0) (hx : x * x ≥ 0) (hy : y * y ≥ 0) 
5    : x * x = 0 := by linarith
6
7-- Combining with computed facts
8example (n : Int) (h : n ≥ 0) : 2 * n ≥ n := by linarith

nlinarith: The Non-linear Extension

For goals involving products of variables, use nlinarith:

lean

1import Mathlib.Tactic.Linarith
2
3-- nlinarith handles some nonlinear cases
4example (x : Int) (h : x ≥ 2) : x * x ≥ 4 := by
5  nlinarith [sq_nonneg x, sq_nonneg (x - 2)]
6
7-- Square is always ≥ 0
8example (x : Int) : x * x ≥ 0 := by nlinarith [sq_nonneg x]
9
10-- Product of positive numbers is positive
11example (x y : Int) (hx : x > 0) (hy : y > 0) : x * y > 0 := by nlinarith

Deep Dive: How linarith Works: The Simplex Algorithm

linarith uses techniques from linear programming to find proofs:

Collection: Gather all linear inequalities from the context
Negation: Add the negation of the goal as an additional constraint
Feasibility Check: Use the Simplex algorithm to check if the constraint system is satisfiable
Certificate: If unsatisfiable, extract a proof certificate (the linear combination)

If the negated goal creates an unsatisfiable system, the original goal must be true.

Real-World Examples

Triangle Inequality

lean

1import Mathlib.Tactic.Linarith
2
3-- Given sides of a valid triangle, prove bounds
4theorem triangle_sides (a b c : Int) 
5    (h1 : a + b > c) (h2 : b + c > a) (h3 : c + a > b)
6    (ha : a > 0) (hb : b > 0) (hc : c > 0) :
7    a < b + c := by linarith

Bounds Propagation

lean

1import Mathlib.Tactic.Linarith
2
3-- If we know bounds on parts, derive bounds on whole
4theorem bound_sum (x y z : Int) 
5    (hx : 0 ≤ x) (hx' : x ≤ 10)
6    (hy : 0 ≤ y) (hy' : y ≤ 10)
7    (hz : 0 ≤ z) (hz' : z ≤ 10) :
8    x + y + z ≤ 30 := by linarith
9
10-- Tighter bound when we know the sum
11theorem bound_from_sum (x y : Int) (h : x + y = 10) (hx : x ≥ 3) : y ≤ 7 := by
12  linarith

Ordering Proofs

lean

1import Mathlib.Tactic.Linarith
2
3-- Mixed strict and non-strict inequalities
4example (a b c d : Int) (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) : a < d := by
5  linarith
6
7-- Averaging
8example (a b m : Int) (h : 2 * m = a + b) (hab : a ≤ b) : a ≤ m := by
9  linarith

Common Patterns

lean

1import Mathlib.Tactic.Linarith
2
3-- Absolute value bounds (given expanded form)
4example (x : Int) (h1 : -5 ≤ x) (h2 : x ≤ 5) : -5 ≤ x ∧ x ≤ 5 := by
5  constructor <;> linarith
6
7-- Sandwich theorem setup
8example (a b c : Int) (h1 : a ≤ b) (h2 : b ≤ c) (h3 : a = c) : b = a := by
9  linarith
10
11-- Interval arithmetic
12example (x y : Int) (hx : 1 ≤ x) (hx' : x ≤ 3) (hy : 2 ≤ y) (hy' : y ≤ 4) 
13    : 3 ≤ x + y := by linarith

Exercise 1: Transitivity

Use linarith to prove transitivity.

lean

1import Mathlib.Tactic.Linarith
2
3example (a b c : Int) (h1 : a < b) (h2 : b < c) : a < c := by linarith

Exercise 2: Contradiction

Find the contradiction in these constraints.

lean

1import Mathlib.Tactic.Linarith
2
3example (x : Int) (h1 : x > 10) (h2 : x < 5) : False := by linarith

Exercise 3: Bound Derivation

Derive a bound from constraints.

lean

1import Mathlib.Tactic.Linarith
2
3example (x y : Int) (h1 : x + y ≤ 100) (h2 : y ≥ 60) : x ≤ 40 := by linarith

field_simp Next: nlinarith