Micromega: tactics for solving arithmetic goals over ordered rings¶
 著者
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 \(\mathbb{Z}\), \(\mathbb{Q}\), and \(\mathbb{R}\) 1.
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;nia
is an incomplete proof procedure for integer nonlinear arithmetic;lra
is a decision procedure for linear (real or rational) arithmetic;nra
is an incomplete proof procedure for nonlinear (real or rational) arithmetic;psatz
D n
whereD
is \(\mathbb{Z}\) or \(\mathbb{Q}\) or \(\mathbb{R}\), andn
is an optional integer limiting the proof search depth, is an incomplete proof procedure for nonlinear arithmetic. It is based on John Harrison’s HOL Light driver to the external prover csdp 2. Note that the csdp driver is generating a proof cache which makes it possible to rerun scripts even without csdp.
The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain \(D\) ∈ {ℤ, ℚ, ℝ}. The syntax of the formulas is the following:
F ::= A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F A ::= p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p p ::= c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
where \(c\) is a numeric constant, \(x \in D\) is a numeric variable, the operators \(−, +, ×\) are respectively subtraction, addition, and product; \(p ^ n\) is exponentiation by a constant \(n\), \(P\) is an arbitrary proposition. For \(\mathbb{Q}\), equality is not Leibniz equality = but the equality of rationals ==.
For \(\mathbb{Z}\) (resp. \(\mathbb{Q}\)), \(c\) ranges over integer constants (resp. rational constants). For \(\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 \(z\) is a constant in \(\mathbb{Z}\) and \(q\) is a constant in \(\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 \(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 3.
Theorem (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. A proof based on this theorem is called a 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 an oracle which searches for \(1\) within the cone. Upon success, the oracle returns a cone expression that is normalized by the ring tactic (see The ring and field tactic families) and checked to be \(1\).
lra: a decision procedure for linear real and rational arithmetic¶

lra
¶
This tactic is searching for linear refutations using Fourier elimination 4. As a result, this tactic explores a subset of the 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 lra is the combined deductive power of ring_simplify and fourier. There is also an overlap with the field tactic e.g., \(x = 10 * x / 10\) is solved by lra.
lia: a tactic for linear integer arithmetic¶

lia
¶
This tactic offers an alternative to the omega
and romega
tactics. 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
socalled omega nightmare [Pug92].
 Goal forall x y, 27 <= 11 * x + 13 * y <= 45 > 10 <= 7 * x  9 * y <= 4 > False.
 Toplevel input, characters 5255: > Goal forall x y, 27 <= 11 * x + 13 * y <= 45 > 10 <= 7 * x  9 * y <= 4 > False. > ^^^ Error: Cannot interpret a negative number as a number of type nat
The estimation of the relative efficiency of lia
vs omega
and
romega
is under evaluation.
High level view of lia¶
Over \(\mathbb{R}\), positivstellensatz refutations are a complete proof principle 5. However, this is not the case over \(\mathbb{Z}\). Actually, positivstellensatz refutations are not even sufficient to decide linear integer arithmetic. The canonical example is \(2 * x = 1 > \mathtt{False}\) which is a theorem of \(\mathbb{Z}\) but not a theorem of \({\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 \(\mathbb{Z}\) by rounding up (rational) constants upto the closest integer.

Theorem
Bound on the ceiling function
Let \(p\) be an integer and \(c\) a rational constant. Then \(p \ge c \rightarrow p \ge \lceil{c}\rceil\).
For instance, from 2 x = 1 we can deduce
\(x \ge 1/2\) whose cut plane is \(x \ge \lceil{1/2}\rceil = 1\);
\(x \le 1/2\) whose cut plane is \(x \le \lfloor{1/2}\rfloor = 0\).
By combining these two facts (in normal form) \(x − 1 \ge 0\) and \(x \ge 0\), we conclude by exhibiting a positivstellensatz refutation: \(−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.
Theorem. Let \(p\) be an integer and \(c_1\) and \(c_2\) integer constants. Then:
\(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 \(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.
nra: a proof procedure for nonlinear arithmetic¶

nra
¶
This tactic is an experimental proof procedure for nonlinear arithmetic. The tactic performs a limited amount of nonlinear reasoning before running the linear prover of lra. This preprocessing does the following:
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\);
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\).
After this preprocessing, the linear prover of lra searches for a proof by abstracting monomials by variables.
nia: a proof procedure for nonlinear integer arithmetic¶

nia
¶
This tactic is a proof procedure for nonlinear integer arithmetic. It performs a preprocessing similar to nra. The obtained goal is solved using the linear integer prover lia.
psatz: a proof procedure for nonlinear arithmetic¶

psatz
¶
This 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:
 Require Import ZArith Psatz.
 [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done] [Loading ML file r_syntax_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done]
 Open Scope Z_scope.
 Goal forall x, x^2 >= 0 > x  1 >= 0 > False.
 1 subgoal ============================ forall x : Z,  x ^ 2 >= 0 > x  1 >= 0 > False
 intro x.
 1 subgoal x : Z ============================  x ^ 2 >= 0 > x  1 >= 0 > False
 psatz Z 2.
 Toplevel input, characters 09: > psatz Z 2. > ^^^^^^^^^ Error: In nested Ltac calls to "psatz (constr) (int_or_var)", "xpsatz" and "psatz_Z (int_or_var) (tactic)", last call failed. Tactic failure: Skipping what remains of this tactic: the complexity of the goal requires the use of a specialized external tool called csdp. Unfortunately Coq isn't aware of the presence of any "csdp" executable in the path. Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coinor.org/Csdp.
As shown, such a goal is solved by intro x. psatz Z 2.
. The oracle returns the
cone expression \(2 \times (x1) + (\mathbf{x1}) \times (\mathbf{x−1}) + x^2\)
(polynomial hypotheses are printed in bold). By construction, this expression
belongs to \(\mathit{Cone}({−x^2,x 1})\). Moreover, by running ring we
obtain \(1\). By Theorem Psatz, the goal is valid.
 1
Support for nat and \(\mathbb{N}\) is obtained by preprocessing the goal with the zify tactic.
 2
Sources and binaries can be found at https://projects.coinor.org/Csdp
 3
Variants deal with equalities and strict inequalities.
 4
More efficient linear programming techniques could equally be employed.
 5
In practice, the oracle might fail to produce such a refutation.