[Sphinx] Add chapter 22

Thanks to Paul Steckler for porting this chapter.

2 files changed, 249 insertions, 251 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2617142f5..e850587c8 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -1,256 +1,252 @@
-\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} \}$.
+.. _ micromega:
+
+Micromega: tactics for solving arithmetic goals over ordered rings
+==================================================================
+
+:Authors: Frédéric Besson and Evgeny Makarov
+
+Short description of the tactics
+--------------------------------
+
+The Psatz module (``Require Import Psatz.``) gives access to several
+tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_.
+It also possible to get the tactics for integers by a ``Require Import Lia``,
+rationals ``Require Import Lqa`` and reals ``Require Import Lra``.
+
++ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`);
++ ``nia`` is an incomplete proof procedure for integer non-linear
+  arithmetic (see Section :ref:`nia <nia>`);
++ ``lra`` is a decision procedure for linear (real or rational) arithmetic
+  (see Section :ref:`lra <lra>`);
++ ``nra`` is an incomplete proof procedure for non-linear (real or
+  rational) arithmetic (see Section :ref:`nra <nra>`);
++ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and
+  ``n`` is an optional integer limiting the proof search depth
+  is an incomplete proof procedure for non-linear arithmetic.
+  It is based on John Harrison’s HOL Light
+  driver to the external prover `csdp` [#]_. Note that the `csdp` driver is
+  generating a *proof cache* which makes it possible to rerun scripts
+  even without `csdp` (see Section :ref:`psatz <psatz>`).
+
+The tactics solve propositional formulas parameterized by atomic
+arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}.
 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}
+
+ .. productionlist:: `F`
+   F : A ∣ P ∣ True ∣ False ∣ F 1 ∧ F 2 ∣ F 1 ∨ F 2 ∣ F 1 ↔ F 2 ∣ F 1 → F 2 ∣ ¬ F
+   A : p 1 = p 2 ∣ p 1 > p 2 ∣ p 1 < p 2 ∣ p 1 ≥ p 2 ∣ p 1 ≤ p 2
+   p : c ∣ x ∣ −p ∣ p 1 − p 2 ∣ p 1 + p 2 ∣ p 1 × p 2 ∣ p ^ n
+		     
+where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
+operators :math:`−, +, ×` are respectively subtraction, addition, and product;
+:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
+For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of
+rationals ==.
+
+For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational
+constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the
+following expressions:
+
+::
+
+   c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c
+
+where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`.
+This includes integer constants written using the decimal notation, *i.e.*, c%R.
+
+
+*Positivstellensatz* refutations
+--------------------------------
+
+The name `psatz` is an abbreviation for *positivstellensatz* – literally
+"positivity theorem" – which generalizes Hilbert’s *nullstellensatz*. It
+relies on the notion of Cone. Given a (finite) set of polynomials :math:`S`,
+:math:`\mathit{Cone}(S)` is inductively defined as the smallest set of polynomials
+closed under the following rules:
+
+:math:`\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: 
+\end{array}`
+
+The following theorem provides a proof principle for checking that a
+set of polynomial inequalities does not have solutions [#]_.
+
+.. _psatz_thm:
+
+**Theorem (Psatz)**. Let :math:`S` be a set of polynomials.
+If :math:`-1` belongs to :math:`\mathit{Cone}(S)`, then the conjunction
+:math:`\bigwedge_{p \in S} p\ge 0`  is unsatisfiable.
+A proof based on this theorem is called a *positivstellensatz*
+refutation. The tactics work as follows. Formulas are normalized into
+conjunctive normal form :math:`\bigwedge_i C_i` where :math:`C_i` has the
+general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})` and
+:math:`\Join \in \{>,\ge,=\}` for :math:`D\in \{\mathbb{Q},\mathbb{R}\}` and
+:math:`\Join \in \{\ge, =\}` for :math:`\mathbb{Z}`.
+
+For each conjunct :math:`C_i`, the tactic calls a oracle which searches for
+:math:`-1` within the cone. Upon success, the oracle returns a *cone
+expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`)
+and checked to be :math:`-1`.
+
+.. _lra:
+
+`lra`: a decision procedure for linear real and rational arithmetic
+-------------------------------------------------------------------
+
+The `lra` tactic is searching for *linear* refutations using Fourier
+elimination [#]_. As a result, this tactic explores a subset of the *Cone*
+defined as
+
+  :math:`\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 `lra` is the combined deductive power of
+`ring_simplify` and `fourier`. There is also an overlap with the field
+tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
+
+
+.. _lia:
+
+`lia`: a tactic for linear integer arithmetic
+---------------------------------------------
+
+The tactic lia offers an alternative to the omega and romega tactic
+(see :ref:`omega`). Roughly speaking, the deductive power of lia is
+the combined deductive power of `ring_simplify` and `omega`. However, it
+solves linear goals that `omega` and `romega` do not solve, such as the
+following so-called *omega nightmare* :cite:`TheOmegaPaper`.
+
+.. coqtop:: in
+
+   Goal forall x y,
+     27 <= 11 * x + 13 * y <= 45 ->
+     -10 <= 7 * x - 9 * y <= 4 -> False.
+
+The estimation of the relative efficiency of `lia` *vs* `omega` and `romega`
+is under evaluation.
+
+High level view of `lia`
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof
+principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually,
+*positivstellensatz* refutations are not even sufficient to decide
+linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}`
+which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this
+weakness, the `lia` tactic is using recursively a combination of:
+
++ linear *positivstellensatz* refutations;
++ cutting plane proofs;
++ case split.
+  
+Cutting plane proofs
+~~~~~~~~~~~~~~~~~~~~~~
+
+are a way to take into account the discreteness of :math:`\mathbb{Z}` by rounding up
+(rational) constants up-to the closest integer.
+
+.. _ceil_thm:
+
+**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then
+
+ :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`
+
+For instance, from 2 x = 1 we can deduce
+
++ :math:`x \ge 1/2` whose cut plane is :math:`x \ge \lceil{1/2}\rceil = 1`;
++ :math:`x \le 1/2` whose cut plane is :math:`x \le \lfloor{1/2}\rfloor = 0`.
+
+By combining these two facts (in normal form) :math:`x − 1 \ge 0` and
+:math:`-x \ge 0`, we conclude by exhibiting a *positivstellensatz* refutation:
+:math:`−1 \equiv x−1 + −x \in \mathit{Cone}({x−1,x})`.
+
+Cutting plane proofs and linear *positivstellensatz* refutations are a
+complete proof principle for integer linear arithmetic.
+
+Case split
+~~~~~~~~~~~
+
+enumerates over the possible values of an expression.
+
+.. _casesplit_thm:
+
+**Theorem**. Let :math:`p` be an integer and :math:`c_1` and :math:`c_2`
+integer constants. Then:
+
+  :math:`c_1 \le p \le c_2 \Rightarrow \bigvee_{x \in [c_1,c_2]} p = x`
+
+Our current oracle tries to find an expression :math:`e` with a small range
+:math:`[c_1,c_2]`. We generate :math:`c_2 − c_1` subgoals which contexts are enriched
+with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for
+a proof.
+
+.. _nra:
+
+`nra`: a proof procedure for non-linear arithmetic
+--------------------------------------------------
+
+The `nra` tactic is an *experimental* proof procedure for non-linear
+arithmetic. The tactic performs a limited amount of non-linear
+reasoning before running the linear prover of `lra`. This pre-processing
+does the following:
+
+
++ If the context contains an arithmetic expression of the form
+  :math:`e[x^2]` where :math:`x` is a monomial, the context is enriched with
+  :math:`x^2 \ge 0`;
++ For all pairs of hypotheses :math:`e_1 \ge 0`, :math:`e_2 \ge 0`, the context is
+  enriched with :math:`e_1 \times e_2 \ge 0`.
+
+After this pre-processing, the linear prover of `lra` searches for a
+proof by abstracting monomials by variables.
+
+.. _nia:
+
+`nia`: a proof procedure for non-linear integer arithmetic
+----------------------------------------------------------
+
+The `nia` tactic is a proof procedure for non-linear integer arithmetic.
+It performs a pre-processing similar to `nra`. The obtained goal is
+solved using the linear integer prover `lia`.
+
+.. _psatz:
+
+`psatz`: a proof procedure for non-linear arithmetic
+----------------------------------------------------
+
+The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the
+depth parameter :math:`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:
+
+.. coqtop:: all
+
+  Require Import ZArith Psatz.
+  Open Scope Z_scope.
+  Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+  intro x.
+  psatz Z 2.
+
+As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the
+cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2`
+(polynomial hypotheses are printed in bold). By construction, this expression
+belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we
+obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
+
+.. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with
+  the `zify` tactic.
+.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
+.. [#] Variants deal with equalities and strict inequalities.
+.. [#] More efficient linear programming techniques could equally be employed.
+.. [#] In practice, the oracle might fail to produce such a refutation.
+
+.. comment in original TeX:
+.. %% \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(\{\})$.
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 4566db494..ddcb4c4cb 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -43,6 +43,8 @@ Table of contents
 .. toctree::
    :caption: Addendum
 
+   addendum/micromega
+
 .. toctree::
    :caption: Reference