Chapter 21  Omega: a solver of quantifier-free problems in Presburger Arithmetic

Pierre Crégut

21.1  Description of omega

omega solves a goal in Presburger arithmetic, i.e. a universally quantified formula made of equations and inequations. Equations may be specified either on the type nat of natural numbers or on the type Z of binary-encoded integer numbers. Formulas on nat are automatically injected into Z. 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.

21.1.1  Arithmetical goals recognized by omega

omega applied only to quantifier-free formulas built from the connectors

/\, \/, ~, ->

on atomic formulas. Atomic formulas are built from the predicates

=, le, lt, gt, ge

on nat or from the predicates

=, <, <=, >, >=

on Z. In expressions of type nat, omega recognizes

plus, minus, mult, pred, S, O

and in expressions of type Z, omega recognizes

+, -, *, Z.succ, and constants.

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.

21.1.2  Messages from omega

When omega does not solve the goal, one of the following errors is generated:


Error messages:

  1. 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 unknown from omega. Finally, your goal may be really wrong!

  2. omega: Not a quantifier-free goal

    If your goal is universally quantified, you should first apply intro as many time as needed.

  3. omega: Unrecognized predicate or connective: ident
  4. omega: Unrecognized atomic proposition: prop
  5. omega: Can’t solve a goal with proposition variables
  6. omega: Unrecognized proposition
  7. omega: Can’t solve a goal with non-linear products
  8. omega: Can’t solve a goal with equality on type

21.2  Using omega

The omega tactic does not belong to the core system. It should be loaded by

Coq < Require Import Omega.

Coq < Open Scope Z_scope.


Example 3:

Coq < Goal forall m n:Z, 1 + 2 * m <> 2 * n.
1 subgoal
  
  ============================
   forall m n : Z, 1 + 2 * m <> 2 * n

Coq < intros; omega.
No more subgoals.


Example 4:

Coq < Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
1 subgoal
  
  ============================
   forall z : Z, z > 0 -> 2 * z + 1 > z

Coq < intro; omega.
No more subgoals.

21.3  Technical data

21.3.1  Overview of the tactic

21.3.2  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

"The Omega Test: a fast and practical integer programming algorithm for dependence analysis", William Pugh, Communication of the ACM , 1992, p 102-114.

Here is an overview, look at the original paper for more information.

It may happen that there is a real solution and no integer one. The last steps of the Omega procedure (dark shadow) are not implemented, so the decision procedure is only partial.

21.4  Bugs