Practise it in the Academy:Linear arithmetic with omega →

Module 5 · Lesson 1

omega — Linear Arithmetic

omega is a decision procedure for linear arithmetic over integers and natural numbers. It automatically solves goals involving <, ≤, =, +, -, and multiplication by constants. When an arithmetic goal about whole numbers looks obviously true, try omega first.

Why omega Matters

Arithmetic reasoning appears constantly in programming and mathematics. Array bounds, loop termination, index validity—all require proving facts about numbers. Withoutomega, you'd need to manually construct these proofs using lemmas like transitivity, commutativity, and associativity. With omega, you just state what you need and let Lean figure out the details.

Think of omega as a calculator for proofs. You don't explain how 2 + 3 = 5—you just know it's true. Similarly, omega "knows" facts like "if x < y and y < z, then x < z" without you spelling out every step.

What omega Solves

omega handles linear arithmetic—inequalities and equations where variables are only multiplied by constants. This includes:

Comparisons: <, ≤, =, ≠, >, ≥
Operations: +, -, multiplication by constants
Division/modulo: /, % by constants
Types: Nat and Int

lean

1-- Simple inequalities
2example (n : Nat) : n ≤ n + 1 := by omega
3example (a b : Nat) (h : a < b) : a + 1 ≤ b := by omega
4example (x : Int) (h : x > 0) : x ≥ 1 := by omega
5
6-- Arithmetic combinations
7example (a b c : Nat) : a + b + c = c + b + a := by omega
8example (n : Nat) : 2 * n = n + n := by omega
9example (x y : Int) : x - y + y = x := by omega
10
11-- Constants are OK
12example (n : Nat) : 3 * n + 5 * n = 8 * n := by omega
13example (x : Int) : 100 * x - 99 * x = x := by omega

Key Takeaway

Use omega for any goal that's "obviously true" by arithmetic reasoning. It handles +, -, *, /, %, <, ≤, =, ≠ on Nat and Int.

Understanding "Linear"

The word "linear" means variables appear with degree 1 at most. You can have3 * x (constant times variable), but notx * y (variable times variable) orx * x (variable squared).

lean

1-- ✅ Linear: variables multiplied by constants
2example (x y : Int) : 3*x + 2*y = 2*y + 3*x := by omega
3
4-- ❌ Non-linear: variables multiplied by variables
5-- example (x y : Int) : x * y = y * x := by omega  -- Fails!
6-- Use 'ring' instead for polynomial equality
7
8-- ✅ This is still linear (100 is a constant)
9example (n : Nat) : 100 * n > 99 * n ↔ n > 0 := by omega

Nat vs Int: Key Differences

omega works on both Nat andInt, but there are important behavioral differences—especially for subtraction.

Natural Number Subtraction is Truncated

In Nat, subtraction can't go negative. Instead,a - b = 0 when a < b. This is called "truncated subtraction" and omega understands it:

lean

1-- omega knows Nat subtraction is truncated (can't go negative)
2example (n : Nat) : n - n = 0 := by omega
3example (a b : Nat) : a - b ≤ a := by omega  -- Always true!
4
5-- When a ≥ b, subtraction works normally
6example (a b : Nat) (h : a ≥ b) : a - b + b = a := by omega
7
8-- When a < b, a - b = 0
9example (a b : Nat) (h : a < b) : a - b = 0 := by omega

Integer Subtraction is Standard

lean

1-- Int subtraction works as expected (can be negative)
2example (n : Int) : n - n = 0 := by omega
3example (a b : Int) : a - b + b = a := by omega  -- Always true!
4
5-- Negative numbers are fine
6example (x : Int) (h : x < 0) : x ≤ -1 := by omega
7example (a b : Int) : a - b = -(b - a) := by omega

💡

If your proof involves subtraction on Nat and omega is struggling, try adding a hypothesis like h : a ≥ bto ensure the subtraction doesn't truncate.

Using Hypotheses

omega automatically uses all relevant hypotheses in your context. You don't need to tell it which ones to use—it examines them all:

lean

1-- omega uses all hypotheses automatically
2example (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by omega
3
4example (x y : Int) (h1 : x < y) (h2 : y < x + 2) : y = x + 1 := by omega
5
6-- It can combine many constraints
7example (n : Nat) (h1 : n > 0) (h2 : n < 3) : n = 1 ∨ n = 2 := by omega
8
9-- Complex chains work too
10example (a b c d e : Nat) 
11    (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) (h4 : d < e) 
12    : a < e := by omega

Division and Modulo

omega handles division and modulo by numerals, which is particularly useful for proving termination arguments and index bounds. Division by a variable is not linear, so for those facts use the library lemmas:

lean

1-- Division bounds
2example (n : Nat) : n / 2 ≤ n := by omega
3example (n : Nat) (h : n > 1) : n / 2 < n := by omega
4
5-- Modulo bounds
6example (n : Nat) : n % 2 < 2 := by omega
7example (n m : Nat) (h : m > 0) : n % m < m := Nat.mod_lt n h  -- m is a variable
8
9-- The fundamental division identity
10example (n : Nat) : 2 * (n / 2) + n % 2 = n := by omega
11example (n m : Nat) : m * (n / m) + n % m = n := Nat.div_add_mod n m
12
13-- Parity
14example (n : Nat) (h : n % 2 = 0) : 2 * (n / 2) = n := by omega
15example (n : Nat) (h : n % 2 = 1) : 2 * (n / 2) + 1 = n := by omega

ℹ

In practice omega proves almost every true goal of this linear kind. Lean's implementation leaves out some rare steps of the full algorithm, so on an unusual goal it can still fail.

What omega Cannot Do

Understanding omega's limitations helps you know when to reach for other tactics:

Non-linear Multiplication

lean

1-- ❌ Variable × variable is non-linear
2-- example (x y : Nat) : x * y = y * x := by omega  -- Fails!
3example (x y : Nat) : x * y = y * x := by ring  -- Use ring instead
4
5-- ❌ Squaring is non-linear
6-- example (x : Int) : x * x ≥ 0 := by omega  -- Fails!
7example (x : Int) : x * x ≥ 0 := by nlinarith [sq_nonneg x]

Abstract Functions

lean

1-- ❌ omega doesn't understand function behavior
2-- example (f : Nat → Nat) (h : f 0 = 0) : f 0 ≤ 1 := by omega
3
4-- ✅ But it works if you extract the needed fact
5example (f : Nat → Nat) (h : f 0 = 0) : f 0 ≤ 1 := by
6  rw [h]   -- Now goal is: 0 ≤ 1
7  omega    -- This works!

When to Use Alternatives

Situation	Use
Linear arithmetic (Nat/Int)	`omega`
Polynomial equality	`ring`
Non-linear inequalities	`nlinarith`
Decidable propositions	`decide`
Definitional equality	`rfl`

Deep Dive: How omega Works: The Omega Test

omega implements the Omega test algorithm, invented by William Pugh in 1991. It works by:

Normalization: Convert the goal to a conjunction of linear constraints
Negation: Negate the goal and add it to the hypotheses
Variable Elimination: Use Fourier-Motzkin elimination to remove variables one by one
Contradiction Check: If the remaining constraints are unsatisfiable (like 1 ≤ 0), the original goal is proven

lean

1-- omega proves by contradiction:
2-- "The negation of the goal + hypotheses is unsatisfiable"
3
4-- Example: Prove a < c from a < b and b < c
5-- omega adds ¬(a < c), i.e., a ≥ c
6-- Combined with a < b and b < c, this is impossible
7-- Therefore a < c must be true
8
9example (a b c : Nat) (h1 : a < b) (h2 : b < c) : a < c := by
10  omega  -- Finds that a ≥ c contradicts h1 and h2
11
12-- Detecting impossible constraint sets
13example (a b : Nat) (h1 : a < b) (h2 : b < a) : False := by
14  omega  -- Detects a < b ∧ b < a is impossible

Common Patterns

Termination Arguments

When writing recursive functions, you often need to prove that arguments decrease.omega is perfect for this:

lean

1-- Proving arguments decrease for termination
2def myFun (n : Nat) : Nat :=
3  if n < 2 then n
4  else myFun (n / 2) + myFun (n / 2)
5termination_by n
6decreasing_by all_goals omega
7
8-- Why it works: omega proves n / 2 < n when n ≥ 2
9example (n : Nat) (h : n ≥ 2) : n / 2 < n := by omega

Index Bounds

lean

1-- Array and list index bounds
2example (arr : Array Nat) (i : Nat) (h : i < arr.size) : 
3    i < arr.size + 1 := by omega
4
5example (xs : List Nat) (i : Nat) (hi : i < xs.length) (hj : i + 1 < xs.length) 
6    : i < xs.length := by omega
7
8-- Off-by-one reasoning
9example (n i : Nat) (h : i < n) : i ≤ n - 1 := by omega
10example (n i : Nat) (h : i ≤ n - 1) (hn : n > 0) : i < n := by omega

Range Proofs

lean

1-- Proving values are in range
2example (n : Nat) (h1 : n ≥ 5) (h2 : n ≤ 10) : n > 0 := by omega
3
4-- Combining constraints
5example (x y : Nat) (h1 : x + y = 10) (h2 : x ≤ 3) : y ≥ 7 := by omega
6
7-- Disjunction from range
8example (n : Nat) (h1 : n ≥ 1) (h2 : n ≤ 3) : n = 1 ∨ n = 2 ∨ n = 3 := by omega

Chained Inequalities

lean

1-- Transitivity chains
2example (a b c d e : Nat) 
3    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) 
4    : a ≤ e := by omega
5
6-- Mixed strict and non-strict
7example (a b c d : Nat) 
8    (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) 
9    : a < d := by omega

Combining with Other Tactics

lean

1-- omega after simplification
2example (xs : List Nat) : xs.length ≤ xs.length + 1 := by
3  omega
4
5-- omega in subgoals
6example (n : Nat) : n = 0 ∨ n > 0 := by
7  cases n with
8  | zero => left; rfl
9  | succ m => right; omega
10
11-- omega after rewriting
12example (a b c : Nat) (h : a = b + c) : a ≥ b := by
13  rw [h]
14  omega
15
16-- omega with cases
17example (n : Nat) (h : n % 2 = 0 ∨ n % 2 = 1) : n % 2 < 2 := by
18  omega

Examples

Triangle Inequality Consequence

lean

1example (a b c : Nat) (h1 : a + b > c) (h2 : b + c > a) (h3 : c + a > b) 
2    : a < b + c := by omega

Division Properties

lean

1example (n : Nat) (h : n ≥ 2) : n / 2 ≥ 1 := by omega
2example (n : Nat) (h : n % 2 = 0) : 2 * (n / 2) = n := by omega

Exercise 1: Simple Inequality

Let omega solve a basic inequality using a hypothesis.

lean

1example (n : Nat) (h : n ≤ 7) : n + 1 ≤ 8 := by omega

Exercise 2: Combine Constraints

Prove a fact that requires combining two hypotheses.

lean

1example (x y : Nat) (h1 : x ≤ y) (h2 : y ≤ x + 5) : y ≤ x + 5 := by omega

Exercise 3: Division Bound

Prove that division by 2 is strictly smaller (when n > 1).

lean

1example (n : Nat) (h : n > 1) : n / 2 < n := by omega

cases & induction Next: decide