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 \(\mathbb{Q}\),
\(\mathbb{R}\), and \(\mathbb{Z}\) but also nat
and
N
. 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 provercsdp
1. Note that thecsdp
driver generates a proof cache which makes it possible to rerun scripts even withoutcsdp
.

Flag
Simplex
¶ This flag (set by default) instructs the decision procedures to use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination.

Option
Dump Arith
¶ This option (unset by default) may be set to a file path where debug info will be written.

Command
Show Lia Profile
¶ This command prints some statistics about the amount of pivoting operations needed by
lia
and may be useful to detect inefficiencies (only meaningful if flagSimplex
is set).

Flag
Lia Cache
¶ This flag (set by default) instructs
lia
to cache its results in the file.lia.cache

Flag
Nia Cache
¶ This flag (set by default) instructs
nia
to cache its results in the file.nia.cache

Flag
Nra Cache
¶ This flag (set by default) instructs
nra
to cache its results in the file.nra.cache
The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain \(D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}\). The syntax for formulas over \(\mathbb{Z}\) is:
where
P
is an arbitrary proposition
c
is a numeric constant of \(D\)
x
\(\in D\) is a numeric variable
−
,+
and*
are respectively subtraction, addition and product
p ^ n
is exponentiation by a constant \(n\)
For \(\mathbb{Q}\), use the equality of rationals ==
rather than
Leibniz equality =
.
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 2.
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¶

Tactic
lra
¶ This tactic is searching for linear refutations. 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
overlaps with the one offield
tactic e.g., \(x = 10 * x / 10\) is solved bylra
.
lia
: a tactic for linear integer arithmetic¶

Tactic
lia
¶ This tactic solves linear goals over
Z
by searching for linear refutations and cutting planes.lia
provides support forZ
,nat
,positive
andN
by preprocessing via thezify
tactic.
High level view of lia
¶
Over \(\mathbb{R}\), positivstellensatz refutations are a complete proof
principle 3. 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 \to \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¶

Tactic
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¶
psatz
: a proof procedure for nonlinear arithmetic¶

Tactic
psatz one_term int_or_var?
¶ This 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) optimization techniques that might miss a refutation.
To illustrate the working of the tactic, consider we wish to prove the following Coq goal:
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.
zify
: preprocessing of arithmetic goals¶

Tactic
zify
¶ This tactic is internally called by
lia
to support additional types e.g.,nat
,positive
andN
. By requiring the moduleZifyBool
, the boolean typebool
and some comparison operators are also supported.zify
can also be extended by rebinding the tacticZify.zify_post_hook
that is run immediately afterzify
.To support
Z.div
andZ.modulo
:Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations
.To support
Z.quot
andZ.rem
:Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations
.To support
Z.div
,Z.modulo
,Z.quot
, andZ.rem
:Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations
.

Command
Show Zify InjTyp
¶ This command shows the list of types that can be injected into
Z
.

Command
Show Zify Spec
¶ This command shows the list of operators over
Z
that are compiled using their specification e.g.,Z.min
.
 1
Sources and binaries can be found at https://projects.coinor.org/Csdp
 2
Variants deal with equalities and strict inequalities.
 3
In practice, the oracle might fail to produce such a refutation.