From 179aa79f50f4be2c9db3f818413f147f3ad7e2c4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 11:21:16 +0100 Subject: [Sphinx] Move chapter 21 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Omega.tex | 249 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/omega.rst | 249 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 250 insertions(+), 251 deletions(-) delete mode 100644 doc/refman/Omega.tex create mode 100644 doc/sphinx/addendum/omega.rst diff --git a/Makefile.doc b/Makefile.doc index df1e2d3c4..b46d93373 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -61,7 +61,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ + Program.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex deleted file mode 100644 index 82765da6e..000000000 --- a/doc/refman/Omega.tex +++ /dev/null @@ -1,249 +0,0 @@ -\achapter{Omega: a solver of quantifier-free problems in -Presburger Arithmetic} -%HEVEA\cutname{omega.html} -\aauthor{Pierre Crégut} -\label{OmegaChapter} - -\asection{Description of {\tt omega}} -\tacindex{omega} -\label{description} - -{\tt 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 \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 meant 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!+, -, *, Z.succ!, 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: {\sl ident}} - -\item \errindex{omega: Unrecognized atomic proposition: {\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 {\sl type}} - -\end{ErrMsgs} - -%% This code is currently unplugged -%% -% \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 {\tt omega} tactic does not belong to the core system. It should be -loaded by -\begin{coq_example*} -Require Import Omega. -Open Scope Z_scope. -\end{coq_example*} - -\example{} - -\begin{coq_example} -Goal forall 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 forall z:Z, z > 0 -> 2 * z + 1 > z. -intro; omega. -\end{coq_example} - -% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. - -\section{Options} - -\begin{quote} - \optindex{Stable Omega} - {\tt Unset Stable Omega} -\end{quote} -This deprecated option (on by default) is for compatibility with Coq -pre 8.5. It resets internal name counters to make executions of -{\tt omega} independent. - -\begin{quote} - \optindex{Omega UseLocalDefs} - {\tt Unset Omega UseLocalDefs} -\end{quote} -This option (on by default) allows {\tt omega} to use the bodies of -local variables. - -\begin{quote} - \optindex{Omega System} - {\tt Set Omega System} - \optindex{Omega Action} - {\tt Set Omega Action} -\end{quote} -These two options (off by default) activate the printing of debug -information. - -\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, look at 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 Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}. - -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 231742e56..afc1b9c57 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -121,7 +121,6 @@ Options A and B of the licence are {\em not} elected.} \include{Coercion.v}% \include{CanonicalStructures.v}% \include{Classes.v}% -\include{Omega.v}% \include{Micromega.v} \include{Extraction.v}% \include{Program.v}% diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst new file mode 100644 index 000000000..82765da6e --- /dev/null +++ b/doc/sphinx/addendum/omega.rst @@ -0,0 +1,249 @@ +\achapter{Omega: a solver of quantifier-free problems in +Presburger Arithmetic} +%HEVEA\cutname{omega.html} +\aauthor{Pierre Crégut} +\label{OmegaChapter} + +\asection{Description of {\tt omega}} +\tacindex{omega} +\label{description} + +{\tt 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 \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 meant 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!+, -, *, Z.succ!, 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: {\sl ident}} + +\item \errindex{omega: Unrecognized atomic proposition: {\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 {\sl type}} + +\end{ErrMsgs} + +%% This code is currently unplugged +%% +% \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 {\tt omega} tactic does not belong to the core system. It should be +loaded by +\begin{coq_example*} +Require Import Omega. +Open Scope Z_scope. +\end{coq_example*} + +\example{} + +\begin{coq_example} +Goal forall 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 forall z:Z, z > 0 -> 2 * z + 1 > z. +intro; omega. +\end{coq_example} + +% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. + +\section{Options} + +\begin{quote} + \optindex{Stable Omega} + {\tt Unset Stable Omega} +\end{quote} +This deprecated option (on by default) is for compatibility with Coq +pre 8.5. It resets internal name counters to make executions of +{\tt omega} independent. + +\begin{quote} + \optindex{Omega UseLocalDefs} + {\tt Unset Omega UseLocalDefs} +\end{quote} +This option (on by default) allows {\tt omega} to use the bodies of +local variables. + +\begin{quote} + \optindex{Omega System} + {\tt Set Omega System} + \optindex{Omega Action} + {\tt Set Omega Action} +\end{quote} +These two options (off by default) activate the printing of debug +information. + +\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, look at 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 Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}. + +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3