diff options
| author | fbesson | 2009-09-24 12:02:42 +0000 |
|---|---|---|
| committer | fbesson | 2009-09-24 12:02:42 +0000 |
| commit | 9abfed86acb129d836423e73d05f1a53766c56a7 (patch) | |
| tree | ba368f904de2fd1fc5c76a4b3a5b9d023e7d5a51 /doc | |
| parent | 492b5280384263a5dc9f5fb60c9c8d6bcbc8afce (diff) | |
Micromega doc : psatz Z -> psatz Z 2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12353 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Micromega.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index a43cd15b06..2fe7c2f7f7 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -96,9 +96,9 @@ To illustrate the working of the tactic, consider we wish to prove the following Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. \end{coq_example*} \begin{coq_eval} -intro x; psatz Z. +intro x; psatz Z 2. \end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z}. The oracle returns the cone expression $2 \times +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 Theorem~\ref{thm:psatz}, the goal is valid. |