diff options
author | 2015-07-31 17:01:39 +0200 | |
---|---|---|
committer | 2015-07-31 17:01:39 +0200 | |
commit | 947206269dc31bb6b919fce935e1748bc440d960 (patch) | |
tree | fc236d7c8404f3fae3efb0913fa7ff866e5b8e76 | |
parent | ce4c3ddec6c91dc277c922aaac58395c92941710 (diff) |
Fix typos in the Micromega part of the reference manual.
-rw-r--r-- | doc/refman/Micromega.tex | 135 |
1 files changed, 78 insertions, 57 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 551f6c205..1efed6ef7 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -1,4 +1,4 @@ -\achapter{Micromega : tactics for solving arithmetic goals over ordered rings} +\achapter{Micromega: tactics for solving arithmetic goals over ordered rings} \aauthor{Frédéric Besson and Evgeny Makarov} \newtheorem{theorem}{Theorem} @@ -6,33 +6,40 @@ \asection{Short description of the tactics} \tacindex{psatz} \tacindex{lra} \label{sec:psatz-hurry} -The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over - {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}: +The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to +several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and +{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by + pre-processing the goal with the {\tt zify} tactic.} \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); \item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); -\item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is -is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. - Note that the {\tt csdp} driver is generating - a \emph{proof cache} which allows rerunning scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). +\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and + {\tt n} is an optional integer limiting the proof search depth is is an + incomplete proof procedure for non-linear arithmetic. It is based on + John Harrison's HOL Light driver to the external prover {\tt + csdp}\footnote{Sources and binaries can be found at + \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} + driver is generating a \emph{proof cache} which makes it possible to + rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). \end{itemize} -The tactics solve propositional formulas parameterised by atomic arithmetics expressions +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: \[ \begin{array}{lcl} - F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \sim F\\ + F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \neg F\\ A &::=& p_1 = p_2 \mid p_1 > p_2 \mid p_1 < p_2 \mid p_1 \ge p_2 \mid p_1 \le p_2 \\ p &::=& c \mid x \mid {-}p \mid p_1 - p_2 \mid p_1 + p_2 \mid p_1 \times p_2 \mid p \verb!^! n - \end{array} - \] - where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are - respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an - arbitrary proposition. +\end{array} +\] +where $c$ is a numeric constant, $x\in D$ is a numeric variable, the +operators $-$, $+$, $\times$ are respectively subtraction, addition, +product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an +arbitrary proposition. % - For {\tt Q}, equality is not leibnitz equality {\tt =} but the equality of rationals {\tt ==}. + For {\tt Q}, equality is not Leibniz equality {\tt =} but the equality of rationals {\tt ==}. For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants). %% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. @@ -47,79 +54,89 @@ For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational %% \hline %% \end{array} %% \] -For {\tt R}, the tactic recognises as real constants the following expressions: +For {\tt R}, the tactic recognizes as real constants the following expressions: \begin{verbatim} -c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c +c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q + | Rdiv(c,c) | Rinv c \end{verbatim} -where ${\tt z}$ is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. +where {\tt z} is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}. \asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which -generalises Hilbert's \emph{nullstellensatz}. +generalizes Hilbert's \emph{nullstellensatz}. % -It relies on the notion of $\mathit{Cone}$. Given a (finite) set of polynomials $S$, $Cone(S)$ is -inductively defined as the smallest set of polynomials closed under the following rules: +It relies on the notion of $\mathit{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 Cone(S)} \quad -\dfrac{}{p^2 \in Cone(S)} \quad -\dfrac{p_1 \in Cone(S) \quad p_2 \in Cone(S) \quad \Join \in \{+,*\}} {p_1 \Join p_2 \in Cone(S)}\\ +\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 do not have solutions\footnote{Variants deal with equalities and strict inequalities.}: +The following theorem provides a proof principle for checking that a set +of polynomial inequalities does not have solutions.\footnote{Variants + deal with equalities and strict inequalities.} \begin{theorem} \label{thm:psatz} Let $S$ be a set of polynomials.\\ - If ${-}1$ belongs to $Cone(S)$ then the conjunction $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. + If ${-}1$ belongs to $\mathit{Cone}(S)$ then the conjunction + $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. \end{theorem} A proof based on this theorem is called a \emph{positivstellensatz} refutation. % -The tactics work as follows. Formulas are normalised into conjonctive normal form $\bigwedge_i C_i$ where +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 a oracle which searches for $-1$ within the cone. % -Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be +Upon success, the oracle returns a \emph{cone expression} that is normalized by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be $-1$. -\asection{{\tt lra} : a decision procedure for linear real and rational arithmetic} +\asection{{\tt lra}: a decision procedure for linear real and rational arithmetic} \label{sec:lra} The {\tt lra} tactic is searching for \emph{linear} refutations using -Fourier elimination\footnote{More efficient linear programming techniques could equally be employed}. As a -result, this tactic explores a subset of the $Cone$ defined as: +Fourier elimination.\footnote{More efficient linear programming + techniques could equally be employed.} As a result, this tactic +explores a subset of the $\mathit{Cone}$ defined as \[ -LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} +\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 {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{ {\tt psatz} : a proof procedure for non-linear arithmetic} +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} \label{sec:psatz} -The {\tt psatz} tactic explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. +The {\tt psatz} 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) optimisation techniques that might miss a +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.\\ +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. \begin{coq_eval} - Require Import ZArith Psatz. - Open Scope Z_scope. +Require Import ZArith Psatz. +Open Scope Z_scope. \end{coq_eval} \begin{coq_example*} - Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. \end{coq_example*} \begin{coq_eval} intro x; psatz Z 2. \end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the cone expression $2 \times -(\mathbf{x-1}) + \mathbf{x-1}\times\mathbf{x-1} + \mathbf{-x^2}$ (polynomial hypotheses are printed in bold). By construction, this -expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By Theorem~\ref{thm:psatz}, the goal is valid. % @@ -128,14 +145,14 @@ Theorem~\ref{thm:psatz}, the goal is valid. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\asection{ {\tt lia} : a tactic for linear integer arithmetic } +\asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} \label{sec:lia} -The tactic {\tt lia} ({\tt Require Lia.}) offers an alternative to the {\tt omega} and {\tt romega} tactic (see -Chapter~\ref{OmegaChapter}). +The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt + romega} tactic (see Chapter~\ref{OmegaChapter}). % -Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. +Roughly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. % However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. @@ -147,18 +164,20 @@ Goal forall x y, \begin{coq_eval} intros x y; lia. \end{coq_eval} -The estimation of the relative efficiency of lia \emph{vs} {\tt omega} +The estimation of the relative efficiency of {\tt lia} \emph{vs} {\tt omega} and {\tt romega} is under evaluation. \paragraph{High level view of {\tt lia}.} -Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete proof principle\footnote{In practice, the oracle might fail to produce such a refutation.}. +Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete +proof principle.\footnote{In practice, the oracle might fail to produce + such a refutation.} % However, this is not the case over $\mathbb{Z}$. % -Actually, \emph{positivstellensatz} refutations are not even sufficient to decide linear \emph{integer} -arithmetics. +Actually, \emph{positivstellensatz} refutations are not even sufficient +to decide linear \emph{integer} arithmetic. % -The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. +The canonical example is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. % To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: % @@ -177,17 +196,18 @@ To remedy this weakness, the {\tt lia} tactic is using recursively a combination p \ge c \Rightarrow p \ge \lceil c \rceil \] \end{theorem} -For instance, from $2 * x = 1$ we can deduce +For instance, from $2 x = 1$ we can deduce \begin{itemize} \item $x \ge 1/2$ which cut plane is $ x \ge \lceil 1/2 \rceil = 1$; \item $ x \le 1/2$ which cut plane is $ x \le \lfloor 1/2 \rfloor = 0$. \end{itemize} -By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge 0$, we conclude by exhibiting a -\emph{positivstellensatz} refutation ($-1 \equiv \mathbf{x-1} + \mathbf{-x} \in Cone(\{x-1,x\})$). +By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge +0$, we conclude by exhibiting a \emph{positivstellensatz} refutation: $-1 +\equiv \mathbf{x-1} + \mathbf{-x} \in \mathit{Cone}(\{x-1,x\})$. Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic. -\paragraph{Case split} allow to enumerate over the possible values of an expression. +\paragraph{Case split} enumerates over the possible values of an expression. \begin{theorem} Let $p$ be an integer and $c_1$ and $c_2$ integer constants. \[ @@ -199,7 +219,7 @@ 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. -\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic} +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} \tacindex{nia} \label{sec:nia} The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. @@ -212,7 +232,8 @@ This pre-processing does the following: monomial, the context is enriched with $x^2\ge 0$; \item 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$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables. +After pre-processing, the linear prover of {\tt lia} searches for a proof +by abstracting monomials by variables. |