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.

What omega Solves

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

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

Key Takeaway

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

Nat vs Int

lean

1-- omega works on both Nat and Int
2example (n : Nat) : n - n = 0 := by omega
3example (n : Int) : n - n = 0 := by omega
4
5-- Careful: Nat subtraction is truncated
6example (a b : Nat) : a - b ≤ a := by omega
7example (a b : Nat) (h : a ≥ b) : a - b + b = a := by omega
8
9-- Int subtraction is normal
10example (a b : Int) : a - b + b = a := by omega

Using Hypotheses

lean

1-- omega uses all relevant 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
6example (n : Nat) (h : n > 0) (h2 : n < 3) : n = 1 ∨ n = 2 := by omega

Division and Modulo

lean

1-- omega handles div and mod
2example (n : Nat) : n / 2 ≤ n := by omega
3example (n : Nat) : n % 2 < 2 := by omega
4example (n : Nat) : 2 * (n / 2) + n % 2 = n := by omega
5
6-- Useful for proving termination arguments
7example (n : Nat) (h : n > 1) : n / 2 < n := by omega
8example (n m : Nat) (h : m > 0) : n % m < m := by omega

ℹ

omega is complete for linear arithmetic—if a goal is provable using only linear reasoning, omega will find the proof.

What omega Cannot Do

lean

1-- Non-linear: omega can't handle x * y where both are variables
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-- Symbolic: omega doesn't understand abstract functions
6-- example (f : Nat → Nat) (h : f 0 = 0) : f 0 ≤ 1 := by omega  -- fails
7
8-- Need specific Nat lemmas sometimes
9example (n : Nat) : n * 2 / 2 = n := by 
10  exact Nat.mul_div_cancel_left n (by omega : 2 > 0)

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 with simp
12example (a b : Nat) (h : a + b = 10) : a ≤ 10 := by
13  omega

Deep Dive: How omega Works

omega implements the Omega test algorithm:

Convert the goal to a conjunction of linear constraints
Eliminate variables one by one using Fourier-Motzkin elimination
Check if the remaining constraints are satisfiable
If unsatisfiable, the goal is proven

lean

1-- omega proves by contradiction:
2-- "The negation of the goal + hypotheses is unsatisfiable"
3
4example (a b : Nat) (h1 : a < b) (h2 : b < a) : False := by
5  omega  -- Detects a < b ∧ b < a is impossible

Common Patterns

Termination Arguments

lean

1-- Proving arguments decrease
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

Index Bounds

lean

1-- Array and list index bounds
2example (arr : Array Nat) (i : Nat) (h : i < arr.size) : i < arr.size + 1 := by
3  omega
4
5example (xs : List Nat) (i : Nat) (hi : i < xs.length) (hj : i + 1 < xs.length) 
6    : i < xs.length := by omega

Range Proofs

lean

1-- Proving values are in range
2example (n : Nat) (h1 : n ≥ 5) (h2 : n ≤ 10) : n > 0 := by omega
3example (x : Int) (h1 : x > -10) (h2 : x < 10) : x.natAbs < 10 := by 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

Chained Inequalities

lean

1example (a b c d e : Nat) 
2    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) 
3    : a ≤ e := by omega

Recursion & Termination Next: decide