\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

Omega: a solver for quantifier-free problems in Presburger Arithmetic

Author:Pierre Crégut

Description of omega

omega

omega is a tactic for solving goals in Presburger arithmetic, i.e. for proving formulas made of equations and inequalities over the type nat of natural numbers or the type Z of binary-encoded integers. 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.

Variant romega

Deprecated since version 8.9: Use lia instead.

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 by omega. 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 predicate or connective: ident.
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 quote_plugin.cmxs ... done] [Loading ML file newring_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.
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.
No more subgoals.
Abort.

Options

Flag Stable Omega

Deprecated since version 8.5.

This deprecated option (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 option (on by default) allows omega to use the bodies of local variables.

Flag Omega System

This option (off by default) activate the printing of debug information

Flag Omega Action

This option (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 over Z, 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/.