From 8c43e795c772090b336c0f170a6e5dcab196125d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 22 Jun 2018 13:45:03 +0200 Subject: Remove fourier plugin As stated in the manual, the fourier tactic is subsumed by lra. --- doc/sphinx/addendum/micromega.rst | 13 ++++++------- doc/sphinx/language/coq-library.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 15 --------------- 3 files changed, 7 insertions(+), 23 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 0e9c23b9b..2407a9051 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -96,15 +96,14 @@ and checked to be :math:`-1`. .. tacn:: lra :name: lra -This tactic is searching for *linear* refutations using Fourier -elimination [#]_. As a result, this tactic explores a subset of the *Cone* -defined as + This tactic is searching for *linear* refutations using Fourier + elimination [#]_. 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\}` + :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 `lra` is the combined deductive power of -`ring_simplify` and `fourier`. There is also an overlap with the field -tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. + 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`. `lia`: a tactic for linear integer arithmetic diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index afb49413d..f23e04c3a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -889,7 +889,7 @@ Notation Interpretation Some tactics for real numbers +++++++++++++++++++++++++++++ -In addition to the powerful ``ring``, ``field`` and ``fourier`` +In addition to the powerful ``ring``, ``field`` and ``lra`` tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ec085a71e..562f8568d 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4319,21 +4319,6 @@ printed with the Print Fields command. See also: file plugins/setoid_ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field. -.. tacn:: fourier - :name: fourier - -This tactic written by Loïc Pottier solves linear inequalities on real -numbers using Fourier’s method :cite:`Fourier`. This tactic must be loaded by -``Require Import Fourier``. - -.. example:: - .. coqtop:: reset all - - Require Import Reals. - Require Import Fourier. - Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R. - intros; fourier. - Non-logical tactics ------------------------ -- cgit v1.2.3