Arithmetic on autopilot
omega proves whole-number arithmetic from your hypotheses, or shows a counterexample.
In this course 3 / 8
omega proves arithmetic facts about whole numbers on its own. It understands +, -, multiplying by a fixed number, =, <, ≤, and every hypothesis in the context. It also knows exactly how Nat subtraction stops at zero.
example (a b : Nat) (h : a ≤ b) : a < b + 1 := by
omegaIt cannot multiply two unknowns: a * b = b * a is beyond it. And when the claim is false, it says so, with values that may break it:
example (n : Nat) : n + 1 < n := by
omegaomega could not prove the goal: a possible counterexample may satisfy the constraints a ≥ 0 where a := ↑n
Read that as: “with n any number a ≥ 0, the claim can fail”. ↑n is just n seen as an integer. When omega fails, first ask whether the claim is true.
Use omega at the end, once unfold or simp has turned the goal into plain arithmetic.
Worked example
example (a b : Nat) (h : a ≤ b) : increase a ≤ increase b := by
unfold increase
omega
example (n : Nat) : 0 + n = n := by
omega
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
0 + n = n cannot be proved by rfl, because Lean computes addition on its second argument. omega does not compute; it reasons about arithmetic.
omega closes arithmetic goals with +, -, constants and comparisons, using your hypotheses. If it reports a counterexample, check the claim.
On Nat, a - b + b = a fails when b is bigger than a. Prove it when b ≤ a.
Suggested steps
- Let omega use the hypothesis
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct