Omega: a solver for quantifier-free problems in Presburger Arithmetic¶
- Author
Pierre Crégut
Warning
The omega
tactic is deprecated in favor of the lia
tactic. The goal is to consolidate the arithmetic solving
capabilities of Coq into a single engine; moreover, lia
is
in general more powerful than omega
(it is a complete
Presburger arithmetic solver while omega
was known to be
incomplete).
It is recommended to switch from omega
to lia
in existing
projects. We also ask that you report (in our bug tracker) any issue you encounter, especially
if the issue was not present in omega
. If no new issues are
reported, omega
will be removed soon.
Note that replacing omega
with lia
can break
non-robust proof scripts which rely on incompleteness bugs of
omega
(e.g. using the pattern ; try omega
).
Description of omega
¶
-
Tactic
omega
¶ Deprecated since version 8.12: Use
lia
instead.omega
is a tactic for solving goals in Presburger arithmetic, i.e. for proving formulas made of equations and inequalities over the typenat
of natural numbers or the typeZ
of binary-encoded integers. Formulas onnat
are automatically injected intoZ
. The procedure may use any hypothesis of the current proof session to solve the goal.Multiplication is handled by
omega
but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meant by "Presburger arithmetic".If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops.
Arithmetical goals recognized by omega
¶
omega
applies only to quantifier-free formulas built from the connectives:
/\ \/ ~ ->
on atomic formulas. Atomic formulas are built from the predicates:
= < <= > >=
on nat
or Z
. In expressions of type nat
, omega
recognizes:
+ - * S O pred
and in expressions of type Z
, omega
recognizes numeral constants and:
+ - * Z.succ Z.pred
All expressions of type nat
or Z
not built on these
operators are considered abstractly as if they
were arbitrary variables of type nat
or Z
.
Messages from omega
¶
When omega
does not solve the goal, one of the following errors
is generated:
-
Error
omega can't solve this system.
¶ This may happen if your goal is not quantifier-free (if it is universally quantified, try
intros
first; if it contains existentials quantifiers too,omega
is not strong enough to solve your goal). This may happen also if your goal contains arithmetical operators not recognized byomega
. Finally, your goal may be simply not true!
-
Error
omega: Not a quantifier-free goal.
¶ If your goal is universally quantified, you should first apply
intro
as many times as needed.
-
Error
omega: Unrecognized atomic proposition: ...
¶
-
Error
omega: Can't solve a goal with proposition variables.
¶
-
Error
omega: Unrecognized proposition.
¶
-
Error
omega: Can't solve a goal with non-linear products.
¶
-
Error
omega: Can't solve a goal with equality on type ...
¶
Using omega
¶
The omega
tactic does not belong to the core system. It should be
loaded by
- Require Import Omega.
- [Loading ML file newring_plugin.cmxs ... done] [Loading ML file zify_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done]
Example
- Require Import Omega.
- Open Scope Z_scope.
- Goal forall m n:Z, 1 + 2 * m <> 2 * n.
- 1 subgoal ============================ forall m n : Z, 1 + 2 * m <> 2 * n
- intros; omega.
- Toplevel input, characters 0-14: > intros; omega. > ^^^^^^^^^^^^^^ Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] No more subgoals.
- Abort.
- Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
- 1 subgoal ============================ forall z : Z, z > 0 -> 2 * z + 1 > z
- intro; omega.
- Toplevel input, characters 0-13: > intro; omega. > ^^^^^^^^^^^^^ Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] No more subgoals.
- Abort.
Options¶
-
Flag
Stable Omega
¶ Deprecated since version 8.5.
This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of
omega
independent.
-
Flag
Omega UseLocalDefs
¶ This flag (on by default) allows
omega
to use the bodies of local variables.
-
Flag
Omega System
¶ This flag (off by default) activate the printing of debug information
-
Flag
Omega Action
¶ This flag (off by default) activate the printing of debug information
Technical data¶
Overview of the tactic¶
The goal is negated twice and the first negation is introduced as a hypothesis.
Hypotheses are decomposed in simple equations or inequalities. Multiple goals may result from this phase.
Equations and inequalities over
nat
are translated overZ
, multiple goals may result from the translation of subtraction.Equations and inequalities are normalized.
Goals are solved by the OMEGA decision procedure.
The script of the solution is replayed.
Overview of the OMEGA decision procedure¶
The OMEGA decision procedure involved in the omega
tactic uses
a small subset of the decision procedure presented in [Pug92]
Here is an overview, refer to the original paper for more information.
Equations and inequalities are normalized by division by the GCD of their coefficients.
Equations are eliminated, using the Banerjee test to get a coefficient equal to one.
Note that each inequality cuts the Euclidean space in half.
Inequalities are solved by projecting on the hyperspace defined by cancelling one of the variables. They are partitioned according to the sign of the coefficient of the eliminated variable. Pairs of inequalities from different classes define a new edge in the projection.
Redundant inequalities are eliminated or merged in new equations that can be eliminated by the Banerjee test.
The last two steps are iterated until a contradiction is reached (success) or there is no more variable to eliminate (failure).
It may happen that there is a real solution and no integer one. The last steps of the Omega procedure are not implemented, so the decision procedure is only partial.
Bugs¶
The simplification procedure is very dumb and this results in many redundant cases to explore.
Much too slow.
Certainly other bugs! You can report them to https://coq.inria.fr/bugs/.