1 files changed, 223 insertions, 0 deletions
diff --git a/doc/Omega.tex b/doc/Omega.tex
new file mode 100755
index 000000000..286c151c4
--- /dev/null
+++ b/doc/Omega.tex
@@ -0,0 +1,223 @@
+\achapter{\texttt{Omega}: a solver of quantifier-free problems in
+Presburger Arithmetic}
+\aauthor{Pierre Crégut}
+
+\asection{Description of {\tt Omega}}
+\tacindex{Omega}
+\label{description}
+
+{\tt 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 \verb=nat= of natural numbers or on
+the type \verb=Z= of binary-encoded integer numbers. Formulas on
+\verb=nat= are automatically injected into \verb=Z=.  The procedure
+may use any hypothesis of the current proof session to solve the goal.
+
+Multiplication is handled by {\tt 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.
+
+\asubsection{Arithmetical goals recognized by {\tt Omega}}
+
+{\tt Omega}~applied only to quantifier-free formulas built from the
+connectors
+
+\begin{quote}
+\verb=/\, \/, ~, ->=
+\end{quote}
+
+on atomic formulas. Atomic formulas are built from the predicates 
+
+\begin{quote}
+\verb!=, le, lt, gt, ge!
+\end{quote}
+
+ on \verb=nat= or from the predicates
+
+\begin{quote}
+\verb!=, <, <=, >, >=!
+\end{quote}
+
+ on \verb=Z=. In expressions of type \verb=nat=, {\tt Omega}~recognizes 
+
+\begin{quote}
+\verb!plus, minus, mult, pred, S, O!
+\end{quote}
+
+and in expressions of type \verb=Z=, {\tt Omega}~recognizes 
+
+\begin{quote}
+\verb!+,_,*, Zs!, and constants.
+\end{quote}
+
+All expressions of type \verb=nat= or \verb=Z= not built on these
+operators are considered abstractly as if they
+were arbitrary variables of type \verb=nat= or \verb=Z=.
+
+\asubsection{Messages from {\tt Omega}}
+\label{errors}
+
+When {\tt Omega}~does not solve the goal, one of the following errors
+is generated:
+
+\begin{ErrMsgs}
+\item \errindex{Omega can't solve this system}\\
+  This may happen if your goal is not quantifier-free (if it is
+  universally quantified, try {\tt Intros} first; if it contains
+  existentials quantifiers too, {\tt Omega}\ is not strong enough to solve your
+  goal). This may happen also if your goal contains arithmetical
+  operators unknown from {\tt Omega}. Finally, your goal may be really
+  wrong !
+
+\item \errindex{Omega: Not a quantifier-free goal}\\
+  If your goal is universally quantified, you should first apply {\tt
+    Intro} as many time as needed.
+
+\item \errindex{Omega: Unrecognized predicate or connective:{\rm\sl ident}}
+
+\item \errindex{Omega: Unrecognized atomic proposition:{\rm\sl prop}}
+  
+\item \errindex{Omega: Can't solve a goal with proposition variables}
+
+\item \errindex{Omega: Unrecognized proposition}
+
+\item \errindex{Omega: Can't solve a goal with non-linear products}
+
+\item \errindex{Omega: Can't solve a goal with equality on {\rm\sl type}}
+
+\end{ErrMsgs}
+
+%% Ce code est débranché pour l'instant
+%% 
+% \asubsection{Control over the output}
+% There are some flags that can be set to get more information on the procedure
+
+% \begin{itemize}
+% \item \verb=Time= to get the time used by the procedure
+% \item \verb=System= to visualize the normalized systems.
+% \item \verb=Action= to visualize the actions performed by the OMEGA
+%      procedure (see \ref{technical}).
+% \end{itemize}
+
+% \comindex{Set Omega Time}
+% \comindex{UnSet Omega Time}
+% \comindex{Switch Omega Time}
+% \comindex{Set Omega System}
+% \comindex{UnSet Omega System}
+% \comindex{Switch Omega System}
+% \comindex{Set Omega Action}
+% \comindex{UnSet Omega Action}
+% \comindex{Switch Omega Action}
+
+ Use {\tt Set Omega {\rm\sl flag}} to set the flag
+ {\rm\sl flag}. Use {\tt Unset Omega {\rm\sl flag}} to unset it and
+{\tt Switch Omega {\rm\sl flag}} to toggle it.
+
+\section{Using {\tt Omega}}
+
+The tactic {\tt Omega}~does not belong to the core system. It should be
+loaded by
+
+\begin{coq_example*}
+Require Omega.
+\end{coq_example*}
+
+\example{}
+
+\begin{coq_example}
+Goal (m,n:Z) ~ `1+2*m = 2*n`.
+Intros; Omega.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\example{}
+
+\begin{coq_example}
+Goal (z:Z)`z>0` -> `2*z + 1 > z`.
+Intro; Omega.
+\end{coq_example}
+
+Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
+
+\asection{Technical data}
+\label{technical}
+
+\asubsection{Overview of the tactic}
+\begin{itemize}
+
+\item The goal is negated twice and the first negation is introduced as an
+     hypothesis.
+\item Hypothesis are decomposed in simple equations or inequations. Multiple
+     goals may result from this phase.
+\item Equations and inequations over \verb=nat= are translated over
+     \verb=Z=, multiple goals may result from the translation of
+     substraction.
+\item Equations and inequations are normalized.
+\item Goals are solved by the {\it OMEGA} decision procedure.
+\item The script of the solution is replayed.
+
+\end{itemize}
+
+\asubsection{Overview of the {\it OMEGA} decision procedure}
+
+The {\it OMEGA} decision procedure involved in the {\tt Omega}~tactic uses
+a small subset of the decision procedure presented in
+
+\begin{quote}
+  "The Omega Test: a fast and practical integer programming
+algorithm for dependence analysis", William Pugh, Communication of the
+ACM , 1992, p 102-114.
+\end{quote}
+
+Here is an overview.
+The reader is refered to the original paper for more information.
+
+\begin{itemize}
+
+\item Equations and inequations are normalized by division by the GCD of their
+     coefficients.
+\item Equations are eliminated, using the Banerjee test to get a coefficient 
+     equal to one.
+\item Note that each inequation defines a half space in the space of real value
+     of the variables.
+\item Inequations are solved by projecting on the hyperspace defined by 
+     cancelling one of the variable. 
+     They are partitioned according to the sign of
+     the coefficient of the eliminated variable. Pairs of inequations from
+     different classes define a new edge in the projection.
+\item Redundant inequations are eliminated or merged in new equations that can
+     be eliminated by the Banerjee test.
+\item The last two steps are iterated until a contradiction is reached
+     (success) or there is no more variable to eliminate (failure).
+
+\end{itemize}
+
+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.
+
+\asection{Bugs}
+
+\begin{itemize}
+\item The simplification procedure is very dumb and this results in
+  many redundant cases to explore.
+
+\item Much too slow.
+
+\item Certainely plenty other bugs !! You can report them to
+
+\begin{quote}
+  \verb=Pierre.Cregut@cnet.francetelecom.fr= 
+\end{quote}
+
+\end{itemize}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: