1 files changed, 0 insertions, 222 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
deleted file mode 100644
index 5f9ed443..00000000
--- a/doc/refman/Micromega.tex
+++ /dev/null
@@ -1,222 +0,0 @@
-\achapter{Micromega : tactics for solving arithmetic goals over ordered rings}
-\aauthor{Frédéric Besson and Evgeny Makarov}
-\newtheorem{theorem}{Theorem}
-
- 
-\asection{Short description of the tactics}
-\tacindex{psatz}  \tacindex{lra} 
-\label{sec:psatz-hurry}
-The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics for solving arithmetic goals over
- {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}:
-\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 goals (see Section~\ref{sec:lra});
-\item {\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 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 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} (see Section~\ref{sec:psatz}). 
-\end{itemize}
-
-The 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.
- %
- For {\tt Q}, equality is not leibnitz 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 recognises 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
-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$.
-
-
-\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 $Cone$ defined as:
-\[
-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 psatz} : a proof procedure for non-linear arithmetic}
-\label{sec:psatz}
-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. 
-
-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 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} : 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}). 
-%
-Rougthly 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}
-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;
-\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.
-
-\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic}
-\tacindex{nia}
-\label{sec:nia}
-The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear  integer arithmetic.
-%
-The tactic performs a limited amount of non-linear reasoning before running the
-linear prover of {\tt lia}.
-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 pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables.
-
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: