\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \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{\lb}{\lambda} \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}{\mathbb{N}} \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{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \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{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \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}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

Micromega: tactics for solving 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{Z}\), \(\mathbb{Q}\), and \(\mathbb{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.

  • 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 [2]. Note that the csdp driver is generating a proof cache which makes it possible to rerun scripts even without csdp.

The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain \(D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}\). The syntax of the formulas is the following:

F ::=  A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
A ::=  p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
p ::=  c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n

where \(c\) is a numeric constant, \(x \in D\) is a numeric variable, the operators \(−, +, ×\) are respectively subtraction, addition, and product; \(p ^ n\) is exponentiation by a constant \(n\), \(P\) is an arbitrary proposition. For \(\mathbb{Q}\), equality is not Leibniz equality = but the equality of rationals ==.

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

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 The ring and field tactic families) and checked to be \(-1\).

lra: a decision procedure for linear real and rational arithmetic


This tactic is searching for linear refutations using Fourier elimination [4]. 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


This tactic offers an alternative to the omega and romega tactics. 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 [Pug92].

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 \(\mathbb{R}\), positivstellensatz refutations are a complete proof principle [5]. 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 -> \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


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


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


This tactic explores the \(\mathit{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:

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.

[1]Support for nat and N is obtained by pre-processing the goal with the zify tactic.
[2]Sources and binaries can be found at https://projects.coin-or.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.