From bb03fa4eaf74e776b94b7a4b93754742d20f6d3d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 11:33:41 +0100 Subject: [Sphinx] Move chapter 22 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Micromega.tex | 256 -------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/micromega.rst | 256 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 257 insertions(+), 258 deletions(-) delete mode 100644 doc/refman/Micromega.tex create mode 100644 doc/sphinx/addendum/micromega.rst diff --git a/Makefile.doc b/Makefile.doc index df1e2d3c4..940a3ebd7 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 \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ + Program.v.tex Omega.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 231742e56..4b7f9d91b 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -122,7 +122,6 @@ Options A and B of the licence are {\em not} elected.} \include{CanonicalStructures.v}% \include{Classes.v}% \include{Omega.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..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: -- cgit v1.2.3