\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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 is also possible to get only the tactics for integers by `Require Import Lia`, only for rationals by `Require Import Lqa` or only for reals by `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` is an incomplete proof procedure for non-linear arithmetic. `D` is \(\mathbb{Z}\) or \(\mathbb{Q}\) or \(\mathbb{R}\) and `n` is an optional integer limiting the proof search depth. 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.

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.

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

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

> - `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 natural integer 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}\), the equality of rationals `==` is used 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 | Rmult c c | Rplus c c | Rminus c c | IZR z | Q2R q | Rdiv c c | Rinv c

where `z` is a constant in \(\mathbb{Z}\) and `q` is a constant in \(\mathbb{Q}\). This includes `number` 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{split}\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}\end{split}\]

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.

  Proof: Let's assume that \(\bigwedge_{p \in S} p\ge 0\) is satisfiable, meaning there exists \(x\) such that for all \(p \in S\) , we have \(p(x) \ge 0\). Since the cone building rules preserve non negativity, any polynomial in \(\mathit{Cone}(S)\) is non negative in \(x\). Thus \(-1 \in \mathit{Cone}(S)\) is non negative, which is absurd. \(\square\)

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

Tactic xlra_Q ltac_expr
Tactic xlra_R ltac_expr

  For internal use only (it may change without notice).

Tactic wlra_Q ident one_term

  For advanced users interested in deriving tactics for specific needs. See the example below and comments in `plugin/micromega/coq_micromega.mli`.

## `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 (rational) constants to integers.

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

Example: Cutting plane

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 Case split

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

Tactic xlia ltac_expr

  For internal use only (it may change without notice).

Tactic wlia ident one_term

  For advanced users interested in deriving tactics for specific needs. See the example below and comments in `plugin/micromega/coq_micromega.mli`.

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

Tactic xnra_Q ltac_expr
Tactic xnra_R ltac_expr

  For internal use only (it may change without notice).

Tactic wnra_Q ident one_term

  For advanced users interested in deriving tactics for specific needs. See the example below and comments in `plugin/micromega/coq_micromega.mli`.

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

Tactic xnia ltac_expr

  For internal use only (it may change without notice).

Tactic wnia ident one_term

  For advanced users interested in deriving tactics for specific needs. See the example below and comments in `plugin/micromega/coq_micromega.mli`.

## `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. Qed.

As shown, such a goal is solved by `intro x. psatz Z 2`. The oracle returns the cone expression \(2 \times p_2 + p_2^2 + p_1\) with \(p_1 := -x^2\) and \(p_2 := x - 1\). By construction, this expression belongs to \(\mathit{Cone}({p_1, p_2})\). Moreover, by running `ring` we obtain \(-1\). Thus, by Theorem Psatz, the goal is valid.

Tactic xsos_Q ltac_expr
Tactic xsos_R ltac_expr
Tactic xsos_Z ltac_expr
Tactic xpsatz_Q nat_or_var ltac_expr
Tactic xpsatz_R nat_or_var ltac_expr
Tactic xpsatz_Z nat_or_var ltac_expr

  For internal use only (it may change without notice).

Tactic wsos_Q ident one_term
Tactic wsos_Z ident one_term
Tactic wpsatz_Q nat_or_var ident one_term
Tactic wpsatz_Z nat_or_var ident one_term

  For advanced users interested in deriving tactics for specific needs. See the example below and comments in `plugin/micromega/coq_micromega.mli`.

## `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.divide`: `Ltac Zify.zify_post_hook ::= Z.divide_to_equations`.

  - 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.divide`, `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 `Z.to_euclidean_division_equations` tactic consists of the following passes: - `Z.divide_to_equations'`, posing characteristic equations using factors from `Z.divide` - `Z.div_mod_to_equations'`, posing characteristic equations for and generalizing over `Z.div` and `Z.modulo` - `Z.quot_rem_to_equations'`, posing characteristic equations for and generalizing over `Z.quot` and `Z.rem` - `Z.euclidean_division_equations_cleanup`, removing impossible hypotheses introduced by the above passes, such as those presupposing `x <> x` - `Z.euclidean_division_equations_find_duplicate_quotients`, which heuristically adds equations of the form `q1 = q2 \/ q1 <> q2` when it seems that two quotients might be equal, allowing `nia` to prove more goals, including those relating `Z.quot` and `Z.modulo` to `Z.quot` and `Z.rem`.

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

Tactic zify_elim_let
Tactic zify_iter_let ltac_expr
Tactic zify_iter_specs
Tactic zify_op
Tactic zify_saturate

  For internal use only (it may change without notice).

Example: Lra

The `lra` tactic automatically proves the following goal.

Require Import QArith Lqa. #[local] Open Scope Q_scope.
  [Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
Lemma example_lra x y : x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3.
  1 goal x, y : Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
Proof.
lra.
  No more goals.
Qed.

Although understanding what's going on under the hood is not required to use the tactic, here are the details for curious users or advanced users interested in deriving their own tactics for arithmetic types other than `Q` or `R` from the standard library.

Mathematically speaking, one needs to prove that \(p_2 \ge 0 \land p_1 \ge 0 \land p_0 \ge 0\) is unsatisfiable with \(p_2 := 4 - x - 2y\) and \(p_1 := 4 - 2x - y\) and \(p_0 := x + y - 3\). This is done thanks to the cone expression \(p_2 + p_1 + 3 \times p_0 \equiv -1\).

From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto.
Print example_lra.
  example_lra = fun x y : Q => let __arith : forall __x2 __x1 : Q, __x1 + 2 * __x2 <= 4 -> 2 * __x1 + __x2 <= 4 -> __x1 + __x2 < 3 := fun __x2 __x1 : Q => let __wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list in let __varmap := VarMap.Branch (VarMap.Elt __x2) __x1 VarMap.Empty in let __ff := IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) in QTautoChecker_sound __ff __wit (eq_refl <: QTautoChecker __ff __wit = true) (VarMap.find 0 __varmap) in __arith y x : forall x y : Q, x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3 Arguments example_lra (x y)%Q_scope _ _

Here, `__ff` is a reified representation of the goal and `__varmap` is a variable map giving the interpretation of each variable (here that `PEX 1` in `__ff` stands for `__x1` and `PEX 2` for `__x2`). Finally, `__wit` is the cone expression also called witness.

This proof could also be obtained by the following tactics where `wlra_Q wit ff` calls the oracle on the goal `ff` and puts the resulting cone expression in `wit`. `QTautoChecker_sound` is a theorem stating that, when the function call `QTautoChecker ff wit` returns `true`, then the goal represented by `ff` is valid.

Lemma example_lra' x y : x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3.
  1 goal x, y : Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
Proof.
pose (ff := IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp).
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3

pose (varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty).
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
let ff' := eval unfold ff in ff in wlra_Q wit ff'.
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ x + 2 * y <= 4 -> 2 * x + y <= 4 -> x + y < 3
change (eval_bf (Qeval_formula (@VarMap.find Q 0 varmap)) ff).
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ eval_bf (Qeval_formula (VarMap.find 0 varmap)) ff
apply (QTautoChecker_sound ff wit).
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ QTautoChecker ff wit = true

vm_compute.
  1 goal x, y : Q ff := (IMPL (A isProp {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp {| Flhs := PEadd (PEX 1) (PEX 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp) : BFormula (Formula Q) isProp varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty : VarMap.t Q wit := (PsatzAdd (PsatzIn Q 2) (PsatzAdd (PsatzIn Q 1) (PsatzMulE (PsatzC 3) (PsatzIn Q 0))) :: nil)%list : list QWitness ============================ true = true
reflexivity.
  No more goals.
Qed.

[1]

Sources and binaries can be found at https://github.com/coin-or/csdp

[2]

Variants deal with equalities and strict inequalities.

[3]

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

Other versions v: 8.20.0

Versions
  dev
  stable
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF