17.1 Description of Omega
17.1 Description of Omega
Omega solves a goal in Presburger arithmetic, ie 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 meaned by ``Presburger arithmetic''.
If the tactic cannot solve the goal, it fails with an error message.
In any case, the computation eventually stops.
17.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
+,_,*, Zs
, 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
.
17.1.2 Messages from Omega
When Omega does not solve the goal, one of the following errors
is generated:
Error messages:
-
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 !
- Omega: Not a quantifier-free goal
If your goal is universally quantified, you should first apply Intro as many time as needed.
- Omega: Unrecognized predicate or connective:ident
- Omega: Unrecognized atomic proposition:prop
- Omega: Can't solve a goal with proposition variables
- Omega: Unrecognized proposition
- Omega: Can't solve a goal with non-linear products
- Omega: Can't solve a goal with equality on type
17.1.3 Control over the output
There are some flags that can be set to get more information on the procedure
-
Time
to get the time used by the procedure
System
to visualize the normalized systems.
Action
to visualize the actions performed by the OMEGA
procedure (see 17.3).
Use Set Omega flag to set the flag
flag. Use Unset Omega flag to unset it and
Switch Omega flag to toggle it.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.6.0.html at 8/10/98