1 files changed, 256 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
new file mode 100644
index 000000000..2617142f5
--- /dev/null
+++ b/doc/sphinx/addendum/micromega.rst
@@ -0,0 +1,256 @@
+\achapter{Micromega: tactics for solving arithmetic goals over ordered rings}
+%HEVEA\cutname{micromega.html}
+\aauthor{Frédéric Besson and Evgeny Makarov}
+\newtheorem{theorem}{Theorem}
+
+ 
+\asection{Short description of the tactics}
+\tacindex{psatz}  \tacindex{lra} \tacindex{lia}  \tacindex{nia} \tacindex{nra} 
+\label{sec:psatz-hurry}
+The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to
+several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and
+{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by
+  pre-processing the goal with the {\tt zify} tactic.}.
+It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} 
+and reals {\tt Require Import Lra}.
+\begin{itemize}
+\item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});
+\item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia});
+\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic  (see Section~\ref{sec:lra});
+\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic  (see Section~\ref{sec:nra});
+\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and
+  {\tt n} is an optional integer limiting the proof search depth is is an
+  incomplete proof procedure for non-linear arithmetic. It is based on
+  John Harrison's HOL Light driver to the external prover {\tt
+    csdp}\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} which makes it possible to
+  rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}).
+\end{itemize}
+
+The tactics solve propositional formulas parameterized by atomic arithmetic 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 \neg 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, the
+operators $-$, $+$, $\times$ are respectively subtraction, addition,
+product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an
+arbitrary proposition.
+ %
+ For {\tt Q}, equality is not Leibniz equality {\tt =} but the equality of rationals {\tt ==}.
+
+For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants).
+%% 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} & (see below) \\
+%%   \hline
+%%   n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\
+%%   \hline
+%% \end{array}
+%% \]
+For {\tt R}, the tactic recognizes as real constants the following expressions:
+\begin{verbatim}
+c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q
+    | Rdiv(c,c) | Rinv c
+\end{verbatim}
+where {\tt z} is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}.
+This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}.
+
+\asection{\emph{Positivstellensatz} refutations}
+\label{sec:psatz-back}
+
+The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which
+generalizes Hilbert's \emph{nullstellensatz}.
+%
+It relies on the notion of $\mathit{Cone}$. Given a (finite) set of
+polynomials $S$, $\mathit{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 \mathit{Cone}(S)} \quad
+\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad
+\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad
+\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\
+\end{array}
+\]
+The following theorem provides a proof principle for checking that a set
+of polynomial inequalities does 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 $\mathit{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 normalized into conjunctive 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 normalized by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be
+$-1$.
+
+
+\asection{{\tt lra}: a decision procedure for linear real and rational arithmetic}
+\label{sec:lra}
+The {\tt lra} tactic is searching for \emph{linear} refutations using
+Fourier elimination.\footnote{More efficient linear programming
+  techniques could equally be employed.} As a result, this tactic
+explores a subset of the $\mathit{Cone}$ defined as
+\[
+\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|
+~\alpha_p \mbox{ are positive constants} \right\}.
+\]
+The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}.
+%
+There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}.
+
+
+\asection{{\tt lia}: a tactic for linear integer arithmetic}
+\tacindex{lia}
+\label{sec:lia}
+
+The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt
+  romega} tactic (see Chapter~\ref{OmegaChapter}).
+%
+Roughly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}.
+%
+However, it solves linear 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}
+intros x y; lia.
+\end{coq_eval}
+The estimation of the relative efficiency of {\tt 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} arithmetic.
+%
+The canonical example 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;
+\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 \mathit{Cone}(\{x-1,x\})$.
+
+Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic.
+
+\paragraph{Case split} enumerates 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.
+
+
+\asection{{\tt nra}: a proof procedure for non-linear arithmetic}
+\tacindex{nra}
+\label{sec:nra}
+The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic.
+%
+The tactic performs a limited amount of non-linear reasoning before running the
+linear prover of {\tt lra}.
+This pre-processing does the following:
+\begin{itemize}
+\item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a
+  monomial, the context is enriched with $x^2\ge 0$;
+\item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$.
+\end{itemize}
+After this pre-processing, the linear prover of {\tt lra} searches for a proof
+by abstracting monomials by variables.
+
+\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
+\tacindex{nia}
+\label{sec:nia}
+The {\tt nia} tactic is a proof procedure for non-linear  integer arithmetic.
+%
+It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}.
+
+\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
+\label{sec:psatz}
+The {\tt psatz} tactic explores the $\mathit{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) optimization techniques that might miss a
+refutation. 
+
+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 $\mathit{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 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(\{\})$.
+%
+
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: