\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

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 also possible to get the tactics for integers by a Require Import Lia, rationals Require Import Lqa and reals 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 where D is \(\mathbb{Z}\) or \(\mathbb{Q}\) or \(\mathbb{R}\), and n is an optional integer limiting the proof search depth, is an incomplete proof procedure for non-linear arithmetic. 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.

Flag Simplex

Deprecated since version 8.14.

This flag (set by default) instructs the decision procedures to use the Simplex method for solving linear goals instead of the deprecated Fourier elimination.

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 (only meaningful if flag Simplex is set).

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 over \(\mathbb{Z}\) is:

F::=A​P​True​False​F /\ F​F \/ F​F <-> F​F -> F​~ F​F = FA::=p = p​p > p​p < p​p >= p​p <= pp::=c​x​−p​p − p​p + p​p * p​p ^ n

where

• F is interpreted over either Prop or bool

• 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 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}\), use the equality of rationals == 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 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c

where \(z\) is a constant in \(\mathbb{Z}\) and \(q\) is a constant in \(\mathbb{Q}\). This includes integer constants 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:

\(\begin{array}{l} \dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad \dfrac{}{p^2 \in \mathit{Cone}(S)} \quad \dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad \Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ \end{array}\)

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. 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 of field tactic e.g., \(x = 10 * x / 10\) is solved by lra.

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 for Z, nat, positive and N by pre-processing via the zify 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 up (rational) constants up-to the closest integer.

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

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. 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 which contexts are enriched with an equation \(e = i\) for \(i \in [c_1,c_2]\) and recursively search for a proof.

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.

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

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 Coq goal:

Require Import ZArith Psatz. Open Scope Z_scope. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. intro x. psatz Z 2.

As shown, such a goal is solved by intro x. psatz Z 2.. The oracle returns the cone expression \(2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2\) (polynomial hypotheses are printed in bold). By construction, this expression belongs to \(\mathit{Cone}({−x^2,x -1})\). Moreover, by running ring we obtain \(-1\). By Theorem Psatz, the goal is valid.

zify: pre-processing of arithmetic goals

Tactic zify

This tactic is internally called by lia to support additional types, e.g., nat, positive and N. Additional support is provided by the following modules:

• For boolean operators (e.g., Nat.leb), require the module ZifyBool.

• For comparison operators (e.g., Z.compare), require the module ZifyComparison.

• 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, and Nat.pow, require the module ZifyNat.

• For operators N.div, N.mod, and N.pow, require the module ZifyN.

zify can also be extended by rebinding the tactics Zify.zify_pre_hook and Zify.zify_post_hook that are respectively run in the first and the last steps of zify.

• To support Z.div and Z.modulo: Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.

• To support Z.quot and Z.rem: Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations.

• To support Z.div, Z.modulo, Z.quot and Z.rem: either Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations or Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).

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 module ZifyClasses and the default instances can be found in the module ZifyInst.

Command Add Zify add_zify qualid

add_zify::=InjTyp​BinOp​UnOp​CstOp​BinRel​UnOpSpec​BinOpSpec|PropOp​PropBinOp​PropUOp​Saturate

Registers an instance of the specified typeclass. The typeclass type (e.g. BinOp Z.mul or BinRel (@eq Z)) has the additional constraint that the non-implicit argument (here, Z.mul or (@eq Z)) is either a reference (here, Z.mul) or the application of a reference (here, @eq) to a sequence of one_term.

Command Show Zify show_zify

show_zify::=InjTyp​BinOp​UnOp​CstOp​BinRel​UnOpSpec​BinOpSpec​Spec

Prints instances for the specified typeclass. For instance, Show Zify InjTyp prints the list of types that supported by zify i.e., Z, nat, positive and N.

1

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

2

Variants deal with equalities and strict inequalities.

3

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