Micromega: solvers for 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 is also possible to get only the tactics for integers by
Require Import Lia
, only for rationals by Require Import Lqa
or only for reals by 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
is an incomplete proof procedure for non-linear arithmetic.D
is \(\mathbb{Z}\) or \(\mathbb{Q}\) or \(\mathbb{R}\) andn
is an optional integer limiting the proof search depth. It is based on John Harrison’s HOL Light driver to the external prover CSDP 1. Note that the CSDP driver generates a proof cache which makes it possible to rerun scripts even without CSDP.
- 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.
- 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 is:
where
F
is interpreted over eitherProp
orbool
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 natural integer constant \(n\)
When \(F\) is interpreted over bool
, the boolean operators are
&&
, ||
, Bool.eqb
, Bool.implb
, Bool.negb
and the comparisons
in \(A\) are also interpreted over the booleans (e.g., for
\(\mathbb{Z}\), we have Z.eqb
, Z.gtb
, Z.ltb
, Z.geb
,
Z.leb
).
For \(\mathbb{Q}\), the equality of rationals ==
is used 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 | Rmult c c | Rplus c c | Rminus c c | IZR z | Q2R q | Rdiv c c | Rinv c
where z
is a constant in \(\mathbb{Z}\) and q
is a constant in \(\mathbb{Q}\).
This includes number
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:
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.
Proof: Let's assume that \(\bigwedge_{p \in S} p\ge 0\) is satisfiable, meaning there exists \(x\) such that for all \(p \in S\) , we have \(p(x) \ge 0\). Since the cone building rules preserve non negativity, any polynomial in \(\mathit{Cone}(S)\) is non negative in \(x\). Thus \(-1 \in \mathit{Cone}(S)\) is non negative, which is absurd. \(\square\)
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 ring and field: solvers for polynomial and rational equations) 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
.
- Tactic xlra_Q ltac_expr¶
- Tactic xlra_R ltac_expr¶
For internal use only (it may change without notice).
- Tactic wlra_Q ident one_term¶
For advanced users interested in deriving tactics for specific needs. See the example below and comments in
plugin/micromega/coq_micromega.mli
.
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 \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 (rational) constants to integers.
- 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\).
Example: Cutting plane
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 Case split¶
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 whose contexts are enriched with an equation \(e = i\) for \(i \in [c_1,c_2]\) and recursively search for a proof.
- Tactic wlia ident one_term¶
For advanced users interested in deriving tactics for specific needs. See the example below and comments in
plugin/micromega/coq_micromega.mli
.
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.
- Tactic xnra_Q ltac_expr¶
- Tactic xnra_R ltac_expr¶
For internal use only (it may change without notice).
- Tactic wnra_Q ident one_term¶
For advanced users interested in deriving tactics for specific needs. See the example below and comments in
plugin/micromega/coq_micromega.mli
.
nia
: a proof procedure for non-linear integer arithmetic¶
- Tactic nia¶
This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to
nra
. The obtained goal is solved using the linear integer proverlia
.
- Tactic wnia ident one_term¶
For advanced users interested in deriving tactics for specific needs. See the example below and comments in
plugin/micromega/coq_micromega.mli
.
psatz
: a proof procedure for non-linear arithmetic¶
- Tactic psatz one_term nat_or_var?¶
This tactic explores the Cone by increasing degrees – hence the depth parameter
nat_or_var
. 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 goal:
As shown, such a goal is solved by intro x. psatz Z 2
. The oracle returns the
cone expression \(2 \times p_2 + p_2^2 + p_1\) with \(p_1 := -x^2\)
and \(p_2 := x - 1\). By construction, this expression
belongs to \(\mathit{Cone}({p_1, p_2})\). Moreover, by running ring
we
obtain \(-1\). Thus, by Theorem Psatz, the goal is valid.
- Tactic xsos_Q ltac_expr¶
- Tactic xsos_R ltac_expr¶
- Tactic xsos_Z ltac_expr¶
- Tactic xpsatz_Q nat_or_var ltac_expr¶
- Tactic xpsatz_R nat_or_var ltac_expr¶
- Tactic xpsatz_Z nat_or_var ltac_expr¶
For internal use only (it may change without notice).
- Tactic wsos_Q ident one_term¶
- Tactic wsos_Z ident one_term¶
- Tactic wpsatz_Q nat_or_var ident one_term¶
- Tactic wpsatz_Z nat_or_var ident one_term¶
For advanced users interested in deriving tactics for specific needs. See the example below and comments in
plugin/micromega/coq_micromega.mli
.
zify
: pre-processing of arithmetic goals¶
- Tactic zify¶
This tactic is internally called by
lia
to support additional types, e.g.,nat
,positive
andN
. Additional support is provided by the following modules:For boolean operators (e.g.,
Nat.leb
), require the moduleZifyBool
.For comparison operators (e.g.,
Z.compare
), require the moduleZifyComparison
.For native unsigned 63 bit integers, require the module
ZifyUint63
.For native signed 63 bit integers, require the module
ZifySint63
.For operators
Nat.div
,Nat.mod
, andNat.pow
, require the moduleZifyNat
.For operators
N.div
,N.mod
, andN.pow
, require the moduleZifyN
.
zify
can also be extended by rebinding the tacticsZify.zify_pre_hook
andZify.zify_post_hook
that are respectively run in the first and the last steps ofzify
.To support
Z.divide
:Ltac Zify.zify_post_hook ::= Z.divide_to_equations
.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.divide
,Z.div
,Z.modulo
,Z.quot
andZ.rem
: eitherLtac Zify.zify_post_hook ::= Z.to_euclidean_division_equations
orLtac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)
. TheZ.to_euclidean_division_equations
tactic consists of the following passes: -Z.divide_to_equations'
, posing characteristic equations using factors fromZ.divide
-Z.div_mod_to_equations'
, posing characteristic equations for and generalizing overZ.div
andZ.modulo
-Z.quot_rem_to_equations'
, posing characteristic equations for and generalizing overZ.quot
andZ.rem
-Z.euclidean_division_equations_cleanup
, removing impossible hypotheses introduced by the above passes, such as those presupposingx <> x
-Z.euclidean_division_equations_find_duplicate_quotients
, which heuristically adds equations of the formq1 = q2 \/ q1 <> q2
when it seems that two quotients might be equal, allowingnia
to prove more goals, including those relatingZ.quot
andZ.modulo
toZ.quot
andZ.rem
.
The
zify
tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the moduleZifyClasses
and the default instances can be found in the moduleZifyInst
.
- Command Add Zify add_zify qualid¶
- add_zify
::=
InjTypBinOpUnOpCstOpBinRelUnOpSpecBinOpSpec|
PropOpPropBinOpPropUOpSaturateRegisters an instance of the specified typeclass. The typeclass type (e.g.
BinOp Z.mul
orBinRel (@eq Z)
) has the additional constraint that the non-implicit argument (here,Z.mul
or(@eq Z)
) is either areference
(here,Z.mul
) or the application of areference
(here,@eq
) to a sequence ofone_term
.This command supports attributes
local
,export
andglobal
. In sections onlylocal
is supported, outside sections the default isglobal
.
- Command Show Zify show_zify¶
- show_zify
::=
InjTypBinOpUnOpCstOpBinRelUnOpSpecBinOpSpecSpecPrints instances for the specified typeclass. For instance,
Show Zify
InjTyp
prints the list of types that supported byzify
i.e.,Z
,nat
,positive
andN
.
- Tactic zify_elim_let¶
- Tactic zify_iter_let ltac_expr¶
- Tactic zify_iter_specs¶
- Tactic zify_op¶
- Tactic zify_saturate¶
For internal use only (it may change without notice).
Example: Lra
The lra
tactic automatically proves the following goal.
- Require Import QArith Lqa. #[local] Open Scope Q_scope.
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
- Lemma example_lra x y : x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3.
- 1 goal x, y : Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
- Proof.
- lra.
- No more goals.
- Qed.
Although understanding what's going on under the hood is not required
to use the tactic, here are the details for curious users or advanced
users interested in deriving their own tactics for arithmetic types
other than Q
or R
from the standard library.
Mathematically speaking, one needs to prove that \(p_2 \ge 0 \land p_1 \ge 0 \land p_0 \ge 0\) is unsatisfiable with \(p_2 := 4 - x - 2y\) and \(p_1 := 4 - 2x - y\) and \(p_0 := x + y - 3\). This is done thanks to the cone expression \(p_2 + p_1 + 3 \times p_0 \equiv -1\).
- From Stdlib.micromega Require Import RingMicromega QMicromega EnvRing Tauto.
- Print example_lra.
- example_lra = fun x y : Q => let __arith : forall __x2 __x1 : Q, __x1 + 2 * __x2 <= 4 -> 2 * __x1 + __x2 <= 4 -> __x1 + __x2 < 3 := fun __x2 __x1 : Q => let __wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list in let __varmap := VarMap.Branch (VarMap.Elt __x2) __x1 VarMap.Empty in let __ff := IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) in QTautoChecker_sound __ff __wit (eq_refl <: QTautoChecker __ff __wit = true) (VarMap.find 0 __varmap) in __arith y x : forall x y : Q, x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3 Arguments example_lra (x y)%Q_scope _ _
Here, __ff
is a reified representation of the goal and __varmap
is a variable map giving the interpretation of each variable (here that
PEX 1
in __ff
stands for __x1
and PEX 2
for __x2
).
Finally, __wit
is the cone expression also called witness.
This proof could also be obtained by the following tactics where
wlra_Q wit ff
calls the oracle on the goal ff
and puts the
resulting cone expression in wit
.
QTautoChecker_sound
is a theorem stating that, when the function call
QTautoChecker ff wit
returns true
, then the goal represented by
ff
is valid.
- Lemma example_lra' x y : x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3.
- 1 goal x, y : Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
- Proof.
- pose (ff := IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp).
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
- pose (varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty).
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
- let ff' := eval unfold ff in ff in wlra_Q wit ff'.
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
- change (eval_bf (Qeval_formula (@VarMap.find Q 0 varmap)) ff).
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ eval_bf (Qeval_formula (VarMap.find 0 varmap)) ff
- apply (QTautoChecker_sound ff wit).
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ QTautoChecker ff wit = true
- vm_compute.
- 1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ true = true
- reflexivity.
- No more goals.
- Qed.
- 1
Sources and binaries can be found at https://github.com/coin-or/csdp
- 2
Variants deal with equalities and strict inequalities.
- 3
In practice, the oracle might fail to produce such a refutation.