# mathlibdocumentation

tactic.omega.main

meta def omega.select_domain (t s : tactic ) :
meta def omega.type_domain (x : expr) :
meta def omega.form_domain  :
expr

Detects domain of a formula from its expr.

• Returns none, if domain can be either ℤ or ℕ
• Returns some tt, if domain is exclusively ℤ
• Returns some ff, if domain is exclusively ℕ
• Fails, if domain is neither ℤ nor ℕ
meta def omega.goal_domain_aux (x : expr) :
meta def omega.goal_domain  :

Use the current goal to determine. Return tt if the domain is ℤ, and return ff if it is ℕ

meta def omega.determine_domain (opt : list name) :

Return tt if the domain is ℤ, and return ff if it is ℕ

Attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. Guesses the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables. Use omega manual to disable automatic reverts, and omega int or omega nat to specify the domain.

omega attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. In other words, the core procedure of omega works with goals of the form

∀ x₁, ... ∀ xₖ, P


where x₁, ... xₖ are integer (resp. natural number) variables, and P is a quantifier-free formula of linear integer (resp. natural number) arithmetic. For instance:

example : ∀ (x y : int), (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega


By default, omega tries to guess the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables (e.g., all variables of type nat and Props in linear natural number arithmetic, if the domain was determined to be nat) to universally close the goal before calling the main procedure. Therefore, omega will often work even if the goal is not in the above form:

example (x y : nat) (h : 2 * x + 1 = 2 * y) : false := by omega


But this behaviour is not always optimal, since it may revert irrelevant hypotheses or incorrectly guess the domain. Use omega manual to disable automatic reverts, and omega int or omega nat to specify the domain.

example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y :=
by {revert h1 x y, omega manual}

example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat

example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 :=
by {revert h2 i, omega manual int}


omega handles nat subtraction by repeatedly rewriting goals of the form P[t-s] into P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0)), where x is fresh. This means that each (distinct) occurrence of subtraction will cause the goal size to double during DNF transformation.

omega implements the real shadow step of the Omega test, but not the dark and gray shadows. Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution, but it may fail if a real solution exists, even if there is no integer/natural number solution.

You can enable set_option trace.omega true to see how omega interprets your goal.