| Authors: | Frédéric Besson and Evgeny Makarov |
|---|
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 :g:`nat` and
:g:`N`. It also possible to get the tactics for integers by a
Require Import Lia, rationals Require Import Lqa and reals
Require Import Lra.
- :tacn:`lia` is a decision procedure for linear integer arithmetic;
- :tacn:`nia` is an incomplete proof procedure for integer non-linear arithmetic;
- :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic;
- :tacn:`nra` is an incomplete proof procedure for non-linear (real or rational) arithmetic;
- :tacn:`psatz`
D nwhereDis \mathbb{Z} or \mathbb{Q} or \mathbb{R}, andnis 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 is generating a proof cache which makes it possible to rerun scripts even without csdp.
.. flag:: Simplex This flag (set by default) instructs the decision procedures to use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination.
.. opt:: Dump Arith This option (unset by default) may be set to a file path where debug info will be written.
.. cmd:: Show Lia Profile This command prints some statistics about the amount of pivoting operations needed by :tacn:`lia` and may be useful to detect inefficiencies (only meaningful if flag :flag:`Simplex` is set).
.. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
.. flag:: Nia Cache This flag (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
.. flag:: Nra Cache This flag (set by default) instructs :tacn:`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 of the formulas is the following:
.. productionlist:: F F : A ∣ P | True ∣ False ∣ F ∧ F ∣ 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 F is interpreted over either Prop or bool,
c is a numeric constant, x \in D is a numeric variable, the
operators -, +, \times 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 ==.
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{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.
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 :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be -1.
.. tacn:: lra
:name: lra
This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone*
defined as
:math:`\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 :tacn:`lra` overlaps with the one of :tacn:`field`
tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
.. tacn:: lia :name: lia This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic.
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 -> \mathtt{False} which is a theorem of \mathbb{Z} but not a theorem of {\mathbb{R}}. To remedy this weakness, the :tacn:`lia` tactic is using recursively a combination of:
- linear positivstellensatz refutations;
- cutting plane proofs;
- case split.
are a way to take into account the discreteness of \mathbb{Z} by rounding up (rational) constants up-to the closest integer.
.. thm:: Bound on the ceiling function
Let :math:`p` be an integer and :math:`c` a rational constant. Then
:math:`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.
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.
.. tacn:: nra :name: 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 :tacn:`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 :tacn:`lra` searches for a proof by abstracting monomials by variables.
.. tacn:: nia :name: nia This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to :tacn:`nra`. The obtained goal is solved using the linear integer prover :tacn:`lia`.
.. tacn:: psatz :name: psatz This 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:
.. coqdoc:: 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 :tacn:`ring` we
obtain -1. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
.. tacn:: zify :name: zify This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. :tacn:`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 :tacn:`zify`. + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. The :tacn:`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``.
.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid
This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``,
``UnOpSpec``, ``BinOpSpec``.
.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec }
The command prints the typeclass instances of one the typeclasses
among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``,
``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp``
prints the list of types that supported by :tacn:`zify` i.e.,
:g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
.. cmd:: Show Zify Spec
.. deprecated:: 8.13
Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``.
.. cmd:: Add InjTyp
.. deprecated:: 8.13
Use instead either :cmd:`Add Zify` ``InjTyp``.
.. cmd:: Add BinOp
.. deprecated:: 8.13
Use instead either :cmd:`Add Zify` ``BinOp``.
.. cmd:: Add UnOp
.. deprecated:: 8.13
Use instead either :cmd:`Add Zify` ``UnOp``.
.. cmd:: Add CstOp
.. deprecated:: 8.13
Use instead either :cmd:`Add Zify` ``CstOp``.
.. cmd:: Add BinRel
.. deprecated:: 8.13
Use instead either :cmd:`Add Zify` ``BinRel``.
| [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. |