diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 8 |
2 files changed, 8 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c01e6a5aa6..d7e4c9c804 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,7 @@ High level view of `lia` Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide -linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` +linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 \to \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this weakness, the :tacn:`lia` tactic is using recursively a combination of: diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ed2e1ea58c..ed93145622 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -34,6 +34,12 @@ Nsatz: tactics for proving equalities in integral domains You can load the ``Nsatz`` module with the command ``Require Import Nsatz``. + Alternatively, if you prefer not to transitively depend on the + files declaring the axioms used to define the real numbers, you can + ``Require Import NsatzTactic`` instead; this will still allow + :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`, + :math:`\mathbb{Q}` and any user-registered rings. + More about `nsatz` --------------------- @@ -85,4 +91,4 @@ performed using :ref:`typeclasses`. then `lvar` is replaced by all the variables which are not in `parameters`. -See the file `Nsatz.v` for many examples, especially in geometry. +See the test-suite file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_ for many examples, especially in geometry. |