Chapter 21 Micromega : tactics for solving arithmetic goals over ordered rings
 21.1 Short description of the tactics
 21.2 Positivstellensatz refutations
 21.3 lra : a decision procedure for linear real and rational arithmetic
 21.4 psatz : a proof procedure for nonlinear arithmetic
 21.5 lia : a tactic for linear integer arithmetic
 21.6 nia : a proof procedure for nonlinear integer arithmetic
Frédéric Besson and Evgeny Makarov
21.1 Short description of the tactics
The Psatz module (Require Psatz.) gives access to several tactics for solving arithmetic goals over Z^{1}, Q and R:
 lia is a decision procedure for linear integer arithmetic (see Section 21.5);
 nia is an incomplete proof procedure for integer nonlinear arithmetic (see Section 21.6);
 lra is a decision procedure for linear (real or rational) arithmetic goals (see Section 21.3);
 psatz D n where D is Z, Q or R and n is an optional integer limiting the proof search depth is is an incomplete proof procedure for nonlinear arithmetic. It is based on John Harrison’s Hol light driver to the external prover cspd^{2}. Note that the csdp driver is generating a proof cache thus allowing to rerun scripts even without csdp (see Section 21.4).
The tactics solve propositional formulas parameterised by atomic arithmetics expressions interpreted over a domain D ∈ {ℤ, ℚ, ℝ }. The syntax of the formulas is the following:

where c is a numeric constant, x∈ D is a numeric variable and the operators −, +, ×, are
respectively subtraction, addition, product, p ^
n is exponentiation by a constant n, P is an
arbitrary proposition.
For Q, equality is not leibnitz equality = but the equality of rationals ==.
For Z (resp. Q ), c ranges over integer constants (resp. rational constants). For R, the tactic recognises 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 Z and q is a constant in Q. This includes integer constants written using the decimal notation i.e., c\char045R.
21.2 Positivstellensatz refutations
The name psatz is an abbreviation for positivstellensatz – literally positivity theorem – which generalises Hilbert’s nullstellensatz. It relies on the notion of Cone. Given a (finite) set of polynomials S, 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 do not have solutions^{3}:
If −1 belongs to Cone(S) then the conjunction ∧_{p ∈ S} p≥ 0 is unsatisfiable.
A proof based on this theorem is called a positivstellensatz refutation. The tactics work as follows. Formulas are normalised into conjonctive normal form ∧_{i} C_{i} where C_{i} has the general form (∧_{j∈ Si} p_{j} ⑅ 0) → False) and ⑅ ∈ {>,≥,=} for D∈ {ℚ,ℝ} and ⑅ ∈ {≥, =} for ℤ. For each conjunct C_{i}, the tactic calls a oracle which searches for −1 within the cone. Upon success, the oracle returns a cone expression that is normalised by the ring tactic (see chapter 24) and checked to be −1.
21.3 lra : a decision procedure for linear real and rational arithmetic
The lra tactic is searching for linear refutations using Fourier elimination^{4}. As a result, this tactic explores a subset of the Cone defined as:
LinCone(S) =  ⎧ ⎪ ⎨ ⎪ ⎩ 
 α_{p} × p  ⎪ ⎪ ⎪ ⎪  α_{p} are positive constants  ⎫ ⎪ ⎬ ⎪ ⎭ 
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.
21.4 psatz : a proof procedure for nonlinear arithmetic
The 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.
To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
Such a goal is solved by intro x; psatz Z 2. The oracle returns the cone expression 2 × (x−1) + x−1×x−1 + −x^{2} (polynomial hypotheses are printed in bold). By construction, this expression belongs to Cone({−x^{2}, x −1}). Moreover, by running ring we obtain −1. By Theorem 1, the goal is valid.
21.5 lia : a tactic for linear integer arithmetic
The tactic lia offers an alternative to the omega and romega tactic (see Chapter 20). Rougthly 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 [122].
Coq < 27 <= 11 * x + 13 * y <= 45 >
Coq < 10 <= 7 * x  9 * y <= 4 > False.
The estimation of the relative efficiency of lia vs omega and romega is under evaluation.
High level view of lia.
Over ℝ, positivstellensatz refutations are a complete proof principle^{5}. However, this is not the case over ℤ. Actually, positivstellensatz refutations are not even sufficient to decide linear integer arithmetics. The canonical exemple is 2 * x = 1 > False which is a theorem of ℤ but not a theorem of ℝ. 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 discreetness of ℤ by rounding up (rational) constants upto the closest integer.
p ≥ c ⇒ p ≥ ⌈ c ⌉ 
For instance, from 2 * x = 1 we can deduce
 x ≥ 1/2 which cut plane is x ≥ ⌈ 1/2 ⌉ = 1;
 x ≤ 1/2 which cut plane is x ≤ ⌊ 1/2 ⌋ = 0.
By combining these two facts (in normal form) x − 1 ≥ 0 and −x ≥ 0, we conclude by exhibiting a positivstellensatz refutation (−1 ≡ x−1 + −x ∈ Cone({x−1,x})).
Cutting plane proofs and linear positivstellensatz refutations are a complete proof principle for integer linear arithmetic.
Case split
allow to enumerate over the possible values of an expression.
c_{1} ≤ p ≤ 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 ∈ [c_{1},c_{2}] and recursively search for a proof.
21.6 nia : a proof procedure for nonlinear integer arithmetic
The nia tactic is an experimental proof procedure for nonlinear integer arithmetic. The tactic performs a limited amount of nonlinear reasoning before running the linear prover of lia. 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}≥ 0;
 For all pairs of hypotheses e_{1}≥ 0, e_{2} ≥ 0, the context is enriched with e_{1} × e_{2} ≥ 0.
After preprocessing, the linear prover of lia is searching for a proof by abstracting monomials by variables.
 1
 Support for nat and 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.