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

# Coq Reference Manual

# 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`1. 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:

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, 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.

| ℤ | ℚ | ℝ
c | `Z` | `Q` | {R1, R0}
n | `Z` | `Z` | `nat`

## 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:

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 do not have solutions2:

Theorem 1 Let S be a set of polynomials.
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 Ci where Ci has the general form (∧j∈ Si 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 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.

`Coq` `<``Goal forall x, -x``^``2` `>``= 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.

##### The `psatzl` tactic

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

LinCone(S) = | ⎧ ⎪ ⎨ ⎪ ⎩ |
∑
p ∈ S
| αp × p | ⎪ ⎪ ⎪ ⎪ | αp are positive constants | ⎫ ⎪ ⎬ ⎪ ⎭

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].

`Coq` `<``Goal forall x y,`
`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 principle4. 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.

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

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

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 c2 − c1 subgoals which contexts are enriched with an equation e = i for i ∈ [c1,c2] 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.