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
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
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
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:
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
to specify the domain.
nat subtraction by repeatedly rewriting goals of the form
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.