diff options
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | doc/refman/Micromega.tex | 256 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 252 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 1 |
5 files changed, 254 insertions, 258 deletions
diff --git a/Makefile.doc b/Makefile.doc index 2f4727ef9..4a247f1d9 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 \ Coercion.v.tex Extraction.v.tex \ - Program.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ + Program.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/Micromega.tex b/doc/refman/Micromega.tex deleted file mode 100644 index 2617142f5..000000000 --- a/doc/refman/Micromega.tex +++ /dev/null @@ -1,256 +0,0 @@ -\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: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index a49637bb2..86f123322 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -119,7 +119,6 @@ Options A and B of the licence are {\em not} elected.} \include{AddRefMan-pre}% \include{Coercion.v}% \include{Classes.v}% -\include{Micromega.v} \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst new file mode 100644 index 000000000..e850587c8 --- /dev/null +++ b/doc/sphinx/addendum/micromega.rst @@ -0,0 +1,252 @@ +.. _ 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: + + .. 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 [#]_. + +.. _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 d42e73217..c5d4936b1 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -46,6 +46,7 @@ Table of contents addendum/extended-pattern-matching addendum/canonical-structures addendum/omega + addendum/micromega .. toctree:: :caption: Reference |