Chapter 20  Micromega : tactics for solving arithmetics goals over ordered rings

• 20.1  The psatz tactic in a hurry
• 20.2  Positivstellensatz refutations
• 20.3   lia : the linear integer arithmetic tactic

Frédéric Besson and Evgeny Makarov

For using the tactics out-of-the-box, read Section 20.1. Section 20.2 presents some background explaining the proof principle for solving polynomials goals. Section 20.3 explains how to get a complete procedure for linear integer arithmetic.

20.1  The psatz tactic in a hurry

Load the Psatz module (Require Psatz.). This module defines the tactics: lia, psatzl D, and psatz D n where D is Z, Q or R and n is an optional integer limiting the proof search depth.

• The psatzl tactic solves linear goals using an embedded (naive) linear programming prover i.e., fourier elimination.
• The psatz tactic solves polynomial goals using John Harrison’s Hol light driver to the external prover cspd¹. Note that the csdp driver is generating a proof cache thus allowing to rerun scripts even without csdp.
• The lia (linear integer arithmetic) tactic is specialised to solve linear goals over ℤ. It extends psatzl Z and exploits the discreetness of ℤ.

These 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. The following table details for each domain D ∈ {ℤ,ℚ,ℝ} the range of constants c and exponent n.

20.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²:

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 23) and checked to be −1.

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² (polynomial hypotheses are printed in bold). By construction, this expression belongs to Cone({−x², x −1}). Moreover, by running ring we obtain −1. By Theorem 1, the goal is valid.

The psatzl tactic

is searching for linear refutations using a fourier elimination³. As a result, this tactic explore a subset of the Cone defined as:

Basically, the deductive power of psatzl is the combined deductive power of ring_simplify and fourier.

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.

20.3   lia : the linear integer arithmetic tactic

The tactic lia offers an alternative to the omega and romega tactic (see Chapter 19). It solves goals that omega and romega do not solve, such as the following so-called omega nightmare [121].

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⁴. 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 i.e., psatzl Z;
• cutting plane proofs;
• case split.

Cutting plane proofs

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

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.

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

1

Sources and binaries can be found at https://projects.coin-or.org/Csdp

2

Variants deal with equalities and strict inequalities.

3

More efficient linear programming techniques could equally be employed

4

In practice, the oracle might fail to produce such a refutation.