From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 10 Jul 2010 15:57:24 +0100 Subject: Remove non-DFSG contents --- doc/refman/Micromega.tex | 198 ----------------------------------------------- 1 file changed, 198 deletions(-) delete mode 100644 doc/refman/Micromega.tex (limited to 'doc/refman/Micromega.tex') diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex deleted file mode 100644 index 2fe7c2f7..00000000 --- a/doc/refman/Micromega.tex +++ /dev/null @@ -1,198 +0,0 @@ -\achapter{Micromega : tactics for solving arithmetics goals over ordered rings} -\aauthor{Frédéric Besson and Evgeny Makarov} -\newtheorem{theorem}{Theorem} - -For using the tactics out-of-the-box, read Section~\ref{sec:psatz-hurry}. -% -Section~\ref{sec:psatz-back} presents some background explaining the proof principle for solving polynomials goals. -% -Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic. - -\asection{The {\tt psatz} tactic in a hurry} -\tacindex{psatz} -\label{sec:psatz-hurry} -Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tactics: -{\tt lia}, {\tt psatzl D}, %{\tt sos D} -and {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth. - % - \begin{itemize} - \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.}, - fourier elimination. - \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating - a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. - \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$. - It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$. -%% \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover. In theory, it is less general than -%% {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see -%% Section~\ref{sec:psatz-back} for details. - \end{itemize} - -These tactics solve propositional formulas parameterised by atomic arithmetics expressions -interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$. -The syntax of the formulas is the following: -\[ -\begin{array}{lcl} - F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \sim F\\ - A &::=& p_1 = p_2 \mid p_1 > p_2 \mid p_1 < p_2 \mid p_1 \ge p_2 \mid p_1 \le p_2 \\ - p &::=& c \mid x \mid {-}p \mid p_1 - p_2 \mid p_1 + p_2 \mid p_1 \times p_2 \mid p \verb!^! n - \end{array} - \] - where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are - respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an - arbitrary proposition. %that is mostly ignored. -%% -%% Over $\mathbb{Z}$, $c$ is an integer ($c \in \mathtt{Z}$), over $\mathbb{Q}$, $c$ is -The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. -\[ -\begin{array}{|c|c|c|c|} - \hline - &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\ - \hline - c &\mathtt{Z} & \mathtt{Q} & \{R1, R0\} \\ - \hline - n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\ - \hline -\end{array} -\] - -\asection{\emph{Positivstellensatz} refutations} -\label{sec:psatz-back} - -The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which -generalises Hilbert's \emph{nullstellensatz}. -% -It relies on the notion of $\mathit{Cone}$. Given a (finite) set of polynomials $S$, $Cone(S)$ is -inductively defined as the smallest set of polynomials closed under the following rules: -\[ -\begin{array}{l} -\dfrac{p \in S}{p \in Cone(S)} \quad -\dfrac{}{p^2 \in Cone(S)} \quad -\dfrac{p_1 \in Cone(S) \quad p_2 \in Cone(S) \quad \Join \in \{+,*\}} {p_1 \Join p_2 \in Cone(S)}\\ -\end{array} -\] -The following theorem provides a proof principle for checking that a set of polynomial inequalities do not have solutions\footnote{Variants deal with equalities and strict inequalities.}: -\begin{theorem} - \label{thm:psatz} - Let $S$ be a set of polynomials.\\ - If ${-}1$ belongs to $Cone(S)$ then the conjunction $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. -\end{theorem} -A proof based on this theorem is called a \emph{positivstellensatz} refutation. -% -The tactics work as follows. Formulas are normalised into conjonctive normal form $\bigwedge_i C_i$ where -$C_i$ has the general form $(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})$ and $\Join \in \{>,\ge,=\}$ for $D\in -\{\mathbb{Q},\mathbb{R}\}$ and $\Join \in \{\ge, =\}$ for $\mathbb{Z}$. -% -For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ within the cone. -% -Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be -$-1$. - -To illustrate the working of the tactic, consider we wish to prove the following Coq goal.\\ -\begin{coq_eval} - Require Import ZArith Psatz. - Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example*} - Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; psatz Z 2. -\end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the cone expression $2 \times -(\mathbf{x-1}) + \mathbf{x-1}\times\mathbf{x-1} + \mathbf{-x^2}$ (polynomial hypotheses are printed in bold). By construction, this -expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By -Theorem~\ref{thm:psatz}, the goal is valid. -% - -\paragraph{The {\tt psatzl} tactic} is searching for \emph{linear} refutations using a fourier -elimination\footnote{More efficient linear programming techniques could equally be employed}. -As a result, this tactic explore a subset of the $Cone$ defined as: -\[ -LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} -\] -Basically, the deductive power of {\tt psatzl} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. - -\paragraph{The {\tt psatz} tactic} explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a -refutation. - -%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a -%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. -%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. -% - -\asection{ {\tt lia} : the linear integer arithmetic tactic } -\tacindex{lia} -\label{sec:lia} - -The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see -Chapter~\ref{OmegaChapter}). It solves goals that {\tt omega} and {\tt romega} do not solve, such as the -following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. -\begin{coq_example*} - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; lia; -\end{coq_eval} -The estimation of the relative efficiency of lia \emph{vs} {\tt omega} -and {\tt romega} is under evaluation. - -\paragraph{High level view of {\tt lia}.} -Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete proof principle\footnote{In practice, the oracle might fail to produce such a refutation.}. -% -However, this is not the case over $\mathbb{Z}$. -% -Actually, \emph{positivstellensatz} refutations are not even sufficient to decide linear \emph{integer} -arithmetics. -% -The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. -% -To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: -% -\begin{itemize} -\item linear \emph{positivstellensatz} refutations \emph{i.e.}, {\tt psatzl Z}; -\item cutting plane proofs; -\item case split. -\end{itemize} - -\paragraph{Cutting plane proofs} are a way to take into account the discreetness of $\mathbb{Z}$ by rounding up -(rational) constants up-to the closest integer. -% -\begin{theorem} - Let $p$ be an integer and $c$ a rational constant. - \[ - p \ge c \Rightarrow p \ge \lceil c \rceil - \] -\end{theorem} -For instance, from $2 * x = 1$ we can deduce -\begin{itemize} -\item $x \ge 1/2$ which cut plane is $ x \ge \lceil 1/2 \rceil = 1$; -\item $ x \le 1/2$ which cut plane is $ x \le \lfloor 1/2 \rfloor = 0$. -\end{itemize} -By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge 0$, we conclude by exhibiting a -\emph{positivstellensatz} refutation ($-1 \equiv \mathbf{x-1} + \mathbf{-x} \in Cone(\{x-1,x\})$). - -Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic. - -\paragraph{Case split} allow to enumerate over the possible values of an expression. -\begin{theorem} - Let $p$ be an integer and $c_1$ and $c_2$ integer constants. - \[ - c_1 \le p \le c_2 \Rightarrow \bigvee_{x \in [c_1,c_2]} p = x - \] -\end{theorem} -Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]$. -% -We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and -recursively search for a proof. - -% This technique is used to solve so-called \emph{Omega nightmare} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: -- cgit v1.2.3