Chapter 22  Micromega: tactics for solving arithmetic goals over ordered rings

Frédéric Besson and Evgeny Makarov

22.1  Short description of the tactics

The Psatz module (Require Import Psatz.) gives access to several tactics for solving arithmetic goals over Z, Q, and 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.

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 ∣ F1 ∧ F2 ∣ F1 ∨ F2 ∣ F1 ↔ F2 ∣ F1 → F2 ∣ ¬ F
 A::=p1 = p2 ∣  p1 > p2 ∣ p1 < p2 ∣ p1 ≥ p2 ∣ p1 ≤ p2 
 p::=c ∣ x ∣ −p ∣ p1 − p2 ∣ p1 + p2 ∣ p1 × p2 ∣ p ^ n

where c is a numeric constant, xD is a numeric variable, 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 Leibniz equality = but the equality of rationals ==.

For Z (resp. Q ), c ranges over integer constants (resp. rational constants). For 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 Z and q is a constant in Q. This includes integer constants written using the decimal notation i.e., c%R.

22.2  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, Cone(S) is inductively defined as the smallest set of polynomials closed under the following rules:

p ∈ S
p ∈ Cone(S)
p2 ∈ Cone(S)
p1 ∈ Cone(S)    p2 ∈ Cone(S)    ⑅ ∈ {+,*}
p1 ⑅ p2 ∈ Cone(S)

The following theorem provides a proof principle for checking that a set of polynomial inequalities does not have solutions.3

Theorem 1   Let S be a set of polynomials.
−1 belongs to Cone(S) then the conjunction pS p≥ 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 ∧i Ci where Ci has the general form (∧jSi pj ⑅ 0) → False) and ⑅ ∈ {>,≥,=} for D∈ {ℚ,ℝ} and ⑅ ∈ {≥, =} for ℤ. For each conjunct Ci, the tactic calls a oracle which searches for −1 within the cone. Upon success, the oracle returns a cone expression that is normalized by the ring tactic (see chapter 25) and checked to be −1.

22.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 ∈ 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.

22.4  lia: a tactic for linear integer arithmetic

The tactic lia offers an alternative to the omega and romega tactic (see Chapter 21). 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 so-called omega nightmare [130].

Coq < Goal forall x y,
        27 <= 11 * x + 13 * y <= 45 ->
        -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 arithmetic. The canonical example 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:

Cutting plane proofs

are a way to take into account the discreetness of ℤ by rounding up (rational) constants up-to the closest integer.

Theorem 2   Let p be an integer and c a rational constant.
  p ≥ c ⇒ p ≥ ⌈ c ⌉

For instance, from 2 x = 1 we can deduce

By combining these two facts (in normal form) x − 1 ≥ 0 and −x ≥ 0, we conclude by exhibiting a positivstellensatz refutation: −1 ≡ x−1 + xCone({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 3   Let p be an integer and c1 and c2 integer constants.
  c1 ≤ p ≤ c2 ⇒ 
x ∈ [c1,c2]
 p = x

Our current oracle tries to find an expression e with a small range [c1,c2]. We generate c2c1 subgoals which contexts are enriched with an equation e = i for i ∈ [c1,c2] and recursively search for a proof.

22.5  nra: a proof procedure for non-linear arithmetic

The nra 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:

After this pre-processing, the linear prover of lra searches for a proof by abstracting monomials by variables.

22.6  nia: a proof procedure for non-linear integer arithmetic

The nia 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 prover lia.

22.7  psatz: a proof procedure for non-linear 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) optimization techniques that might miss a refutation.

To illustrate the working of the tactic, consider we wish to prove the following Coq goal.

Coq < Goal forall x, -x^>= 0 -> x - 1 >= 0 -> False.

Such a goal is solved by intro x; psatz Z 2. The oracle returns the cone expression 2 × (x−1) + (x−1) × (x−1) + x2 (polynomial hypotheses are printed in bold). By construction, this expression belongs to Cone({−x2, x −1}). Moreover, by running ring we obtain −1. By Theorem 1, the goal is valid.

Support for nat and N is obtained by pre-processing the goal with the zify tactic.
Sources and binaries can be found at
Variants deal with equalities and strict inequalities.
More efficient linear programming techniques could equally be employed.
In practice, the oracle might fail to produce such a refutation.