1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
\achapter{Micromega : tactics for solving arithmetics goals over ordered rings}
\aauthor{Frédéric Besson and Evgeny Makarov}
\newtheorem{theorem}{Theorem}
For using the tactics out-of-the-box, read Section~\ref{sec:psatz-hurry}.
%
Section~\ref{sec:psatz-back} presents some background explaining the proof principle for solving polynomials goals.
%
Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic.
\asection{The {\tt psatz} tactic in a hurry}
\tacindex{psatz}
\label{sec:psatz-hurry}
Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tactics:
{\tt lia}, {\tt psatzl D}, %{\tt sos D}
and {\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.
%
\begin{itemize}
\item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.},
fourier elimination.
\item The {\tt psatz} tactic solves polynomial goals using 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}.
\item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$.
It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$.
%% \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover. In theory, it is less general than
%% {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see
%% Section~\ref{sec:psatz-back} for details.
\end{itemize}
These 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. %that is mostly ignored.
%%
%% Over $\mathbb{Z}$, $c$ is an integer ($c \in \mathtt{Z}$), over $\mathbb{Q}$, $c$ is
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} & \{R1, R0\} \\
\hline
n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\
\hline
\end{array}
\]
\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$.
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 psatzl} tactic} is searching for \emph{linear} refutations using a fourier
elimination\footnote{More efficient linear programming techniques could equally be employed}.
As a result, this tactic explore 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\}
\]
Basically, the deductive power of {\tt psatzl} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}.
\paragraph{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.
%% \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} : the linear integer arithmetic tactic }
\tacindex{lia}
\label{sec:lia}
The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see
Chapter~\ref{OmegaChapter}). It solves 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 \emph{i.e.}, {\tt psatzl Z};
\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.
% This technique is used to solve so-called \emph{Omega nightmare}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
