← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/Omega.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/Omega.tex
 
1
\achapter{Omega: a solver of quantifier-free problems in
 
2
Presburger Arithmetic}
 
3
\aauthor{Pierre Cr�gut}
 
4
\label{OmegaChapter}
 
5
 
 
6
\asection{Description of {\tt omega}}
 
7
\tacindex{omega}
 
8
\label{description}
 
9
 
 
10
{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
 
11
quantified formula made of equations and inequations. Equations may
 
12
be specified either on the type \verb=nat= of natural numbers or on
 
13
the type \verb=Z= of binary-encoded integer numbers. Formulas on
 
14
\verb=nat= are automatically injected into \verb=Z=.  The procedure
 
15
may use any hypothesis of the current proof session to solve the goal.
 
16
 
 
17
Multiplication is handled by {\tt omega} but only goals where at
 
18
least one of the two multiplicands of products is a constant are
 
19
solvable. This is the restriction meant by ``Presburger arithmetic''.
 
20
 
 
21
If the tactic cannot solve the goal, it fails with an error message.
 
22
In any case, the computation eventually stops.
 
23
 
 
24
\asubsection{Arithmetical goals recognized by {\tt omega}}
 
25
 
 
26
{\tt omega} applied only to quantifier-free formulas built from the
 
27
connectors
 
28
 
 
29
\begin{quote}
 
30
\verb=/\, \/, ~, ->=
 
31
\end{quote}
 
32
 
 
33
on atomic formulas. Atomic formulas are built from the predicates 
 
34
 
 
35
\begin{quote}
 
36
\verb!=, le, lt, gt, ge!
 
37
\end{quote}
 
38
 
 
39
 on \verb=nat= or from the predicates
 
40
 
 
41
\begin{quote}
 
42
\verb!=, <, <=, >, >=!
 
43
\end{quote}
 
44
 
 
45
 on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
 
46
 
 
47
\begin{quote}
 
48
\verb!plus, minus, mult, pred, S, O!
 
49
\end{quote}
 
50
 
 
51
and in expressions of type \verb=Z=, {\tt omega} recognizes 
 
52
 
 
53
\begin{quote}
 
54
\verb!+, -, *, Zsucc!, and constants.
 
55
\end{quote}
 
56
 
 
57
All expressions of type \verb=nat= or \verb=Z= not built on these
 
58
operators are considered abstractly as if they
 
59
were arbitrary variables of type \verb=nat= or \verb=Z=.
 
60
 
 
61
\asubsection{Messages from {\tt omega}}
 
62
\label{errors}
 
63
 
 
64
When {\tt omega} does not solve the goal, one of the following errors
 
65
is generated:
 
66
 
 
67
\begin{ErrMsgs}
 
68
 
 
69
\item \errindex{omega can't solve this system}
 
70
 
 
71
  This may happen if your goal is not quantifier-free (if it is
 
72
  universally quantified, try {\tt intros} first; if it contains
 
73
  existentials quantifiers too, {\tt omega} is not strong enough to solve your
 
74
  goal). This may happen also if your goal contains arithmetical
 
75
  operators unknown from {\tt omega}. Finally, your goal may be really
 
76
  wrong!
 
77
 
 
78
\item \errindex{omega: Not a quantifier-free goal}
 
79
  
 
80
  If your goal is universally quantified, you should first apply {\tt
 
81
    intro} as many time as needed.
 
82
 
 
83
\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
 
84
 
 
85
\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
 
86
  
 
87
\item \errindex{omega: Can't solve a goal with proposition variables}
 
88
 
 
89
\item \errindex{omega: Unrecognized proposition}
 
90
 
 
91
\item \errindex{omega: Can't solve a goal with non-linear products}
 
92
 
 
93
\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
 
94
 
 
95
\end{ErrMsgs}
 
96
 
 
97
%% Ce code est d�branch� pour l'instant
 
98
%% 
 
99
% \asubsection{Control over the output}
 
100
% There are some flags that can be set to get more information on the procedure
 
101
 
 
102
% \begin{itemize}
 
103
% \item \verb=Time= to get the time used by the procedure
 
104
% \item \verb=System= to visualize the normalized systems.
 
105
% \item \verb=Action= to visualize the actions performed by the OMEGA
 
106
%      procedure (see \ref{technical}).
 
107
% \end{itemize}
 
108
 
 
109
% \comindex{Set omega Time}
 
110
% \comindex{UnSet omega Time}
 
111
% \comindex{Switch omega Time}
 
112
% \comindex{Set omega System}
 
113
% \comindex{UnSet omega System}
 
114
% \comindex{Switch omega System}
 
115
% \comindex{Set omega Action}
 
116
% \comindex{UnSet omega Action}
 
117
% \comindex{Switch omega Action}
 
118
 
 
119
% Use {\tt Set omega {\rm\sl flag}} to set the flag
 
120
% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
 
121
% {\tt Switch omega {\rm\sl flag}} to toggle it.
 
122
 
 
123
\section{Using {\tt omega}}
 
124
 
 
125
The {\tt omega} tactic does not belong to the core system. It should be
 
126
loaded by
 
127
\begin{coq_example*}
 
128
Require Import Omega.
 
129
Open Scope Z_scope.
 
130
\end{coq_example*}
 
131
 
 
132
\example{}
 
133
 
 
134
\begin{coq_example}
 
135
Goal forall m n:Z, 1 + 2 * m <> 2 * n.
 
136
intros; omega.
 
137
\end{coq_example}
 
138
\begin{coq_eval}
 
139
Abort.
 
140
\end{coq_eval}
 
141
 
 
142
\example{}
 
143
 
 
144
\begin{coq_example}
 
145
Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
 
146
intro; omega.
 
147
\end{coq_example}
 
148
 
 
149
% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
 
150
 
 
151
\asection{Technical data}
 
152
\label{technical}
 
153
 
 
154
\asubsection{Overview of the tactic}
 
155
\begin{itemize}
 
156
 
 
157
\item The goal is negated twice and the first negation is introduced as an
 
158
     hypothesis.
 
159
\item Hypothesis are decomposed in simple equations or inequations. Multiple
 
160
     goals may result from this phase.
 
161
\item Equations and inequations over \verb=nat= are translated over
 
162
     \verb=Z=, multiple goals may result from the translation of
 
163
     substraction.
 
164
\item Equations and inequations are normalized.
 
165
\item Goals are solved by the {\it OMEGA} decision procedure.
 
166
\item The script of the solution is replayed.
 
167
 
 
168
\end{itemize}
 
169
 
 
170
\asubsection{Overview of the {\it OMEGA} decision procedure}
 
171
 
 
172
The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
 
173
a small subset of the decision procedure presented in
 
174
 
 
175
\begin{quote}
 
176
  "The Omega Test: a fast and practical integer programming
 
177
algorithm for dependence analysis", William Pugh, Communication of the
 
178
ACM , 1992, p 102-114.
 
179
\end{quote}
 
180
 
 
181
Here is an overview, look at the original paper for more information.
 
182
 
 
183
\begin{itemize}
 
184
 
 
185
\item Equations and inequations are normalized by division by the GCD of their
 
186
     coefficients.
 
187
\item Equations are eliminated, using the Banerjee test to get a coefficient 
 
188
     equal to one.
 
189
\item Note that each inequation defines a half space in the space of real value
 
190
     of the variables.
 
191
   \item Inequations are solved by projecting on the hyperspace
 
192
     defined by cancelling one of the variable.  They are partitioned
 
193
     according to the sign of the coefficient of the eliminated
 
194
     variable. Pairs of inequations from different classes define a
 
195
     new edge in the projection.
 
196
   \item Redundant inequations are eliminated or merged in new
 
197
     equations that can be eliminated by the Banerjee test.
 
198
\item The last two steps are iterated until a contradiction is reached
 
199
     (success) or there is no more variable to eliminate (failure).
 
200
 
 
201
\end{itemize}
 
202
 
 
203
It may happen that there is a real solution and no integer one. The last
 
204
steps of the Omega procedure (dark shadow) are not implemented, so the 
 
205
decision procedure is only partial.
 
206
 
 
207
\asection{Bugs}
 
208
 
 
209
\begin{itemize}
 
210
\item The simplification procedure is very dumb and this results in
 
211
  many redundant cases to explore.
 
212
 
 
213
\item Much too slow.
 
214
 
 
215
\item Certainly other bugs! You can report them to
 
216
 
 
217
\begin{quote}
 
218
  \url{Pierre.Cregut@cnet.francetelecom.fr}
 
219
\end{quote}
 
220
 
 
221
\end{itemize}
 
222
 
 
223
%%% Local Variables: 
 
224
%%% mode: latex
 
225
%%% TeX-master: "Reference-Manual"
 
226
%%% End: