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 non-linear arithmetic;lra
is a decision procedure for linear (real or rational) arithmetic;nra
is an incomplete proof procedure for non-linear (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 non-linear arithmetic. It is based on John Harrison’s HOL Light driver to the external provercsdp
1. Note that thecsdp
driver is generating 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 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 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 pre-processing 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 -> \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 up-to 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 non-linear arithmetic¶
-
Tactic
nra
¶ This 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 \(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 pre-processing, the linear prover of lra
searches for a
proof by abstracting monomials by variables.
nia
: a proof procedure for non-linear integer arithmetic¶
psatz
: a proof procedure for non-linear arithmetic¶
-
Tactic
psatz
¶ 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 (x-1) + (\mathbf{x-1}) \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
: pre-processing 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.coin-or.org/Csdp
- 2
Variants deal with equalities and strict inequalities.
- 3
In practice, the oracle might fail to produce such a refutation.