diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 210 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/index.rst | 1 |
5 files changed, 10 insertions, 227 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 5d471c695c..d718454364 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,6 @@ and checked to be :math:`-1`. This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. - High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst deleted file mode 100644 index 86bb0502c6..0000000000 --- a/doc/sphinx/addendum/omega.rst +++ /dev/null @@ -1,210 +0,0 @@ -.. _omega_chapter: - -Omega: a (deprecated) solver for arithmetic -===================================================================== - -:Author: Pierre Crégut - -.. warning:: - - The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` - tactic. The goal is to consolidate the arithmetic solving - capabilities of Coq into a single engine; moreover, :tacn:`lia` is - in general more powerful than :tacn:`omega` (it is a complete - Presburger arithmetic solver while :tacn:`omega` was known to be - incomplete). - - It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing - projects. We also ask that you report (in our `bug tracker - <https://github.com/coq/coq/issues>`_) any issue you encounter, especially - if the issue was not present in :tacn:`omega`. If no new issues are - reported, :tacn:`omega` will be removed soon. - - Note that replacing :tacn:`omega` with :tacn:`lia` can break - non-robust proof scripts which rely on incompleteness bugs of - :tacn:`omega` (e.g. using the pattern :g:`; try omega`). - -Description of ``omega`` ------------------------- - -.. tacn:: omega - - .. deprecated:: 8.12 - - Use :tacn:`lia` instead. - - :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequalities over the - type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. - Formulas on ``nat`` are automatically injected into ``Z``. The procedure - may use any hypothesis of the current proof session to solve the goal. - - Multiplication is handled by :tacn:`omega` but only goals where at - least one of the two multiplicands of products is a constant are - solvable. This is the restriction meant by "Presburger arithmetic". - - If the tactic cannot solve the goal, it fails with an error message. - In any case, the computation eventually stops. - -Arithmetical goals recognized by ``omega`` ------------------------------------------- - -:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: - - /\ \/ ~ -> - -on atomic formulas. Atomic formulas are built from the predicates:: - - = < <= > >= - -on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes:: - - + - * S O pred - -and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and:: - - + - * Z.succ Z.pred - -All expressions of type ``nat`` or ``Z`` not built on these -operators are considered abstractly as if they -were arbitrary variables of type ``nat`` or ``Z``. - -Messages from ``omega`` ------------------------ - -When :tacn:`omega` does not solve the goal, one of the following errors -is generated: - -.. exn:: omega can't solve this system. - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try :tacn:`intros` first; if it contains - existentials quantifiers too, :tacn:`omega` is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators not recognized by :tacn:`omega`. Finally, your goal may be simply - not true! - -.. exn:: omega: Not a quantifier-free goal. - - If your goal is universally quantified, you should first apply - :tacn:`intro` as many times as needed. - -.. exn:: omega: Unrecognized predicate or connective: @ident. - :undocumented: - -.. exn:: omega: Unrecognized atomic proposition: ... - :undocumented: - -.. exn:: omega: Can't solve a goal with proposition variables. - :undocumented: - -.. exn:: omega: Unrecognized proposition. - :undocumented: - -.. exn:: omega: Can't solve a goal with non-linear products. - :undocumented: - -.. exn:: omega: Can't solve a goal with equality on type ... - :undocumented: - - -Using ``omega`` ---------------- - -The ``omega`` tactic does not belong to the core system. It should be -loaded by - -.. coqtop:: in - - Require Import Omega. - -.. example:: - - .. coqtop:: all warn - - Require Import Omega. - - Open Scope Z_scope. - - Goal forall m n:Z, 1 + 2 * m <> 2 * n. - intros; omega. - Abort. - - Goal forall z:Z, z > 0 -> 2 * z + 1 > z. - intro; omega. - Abort. - - -Options -------- - -.. flag:: Stable Omega - - .. deprecated:: 8.5 - - This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It - resets internal name counters to make executions of :tacn:`omega` independent. - -.. flag:: Omega UseLocalDefs - - This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local - variables. - -.. flag:: Omega System - - This flag (off by default) activate the printing of debug information - -.. flag:: Omega Action - - This flag (off by default) activate the printing of debug information - -Technical data --------------- - -Overview of the tactic -~~~~~~~~~~~~~~~~~~~~~~ - - * The goal is negated twice and the first negation is introduced as a hypothesis. - * Hypotheses are decomposed in simple equations or inequalities. Multiple - goals may result from this phase. - * Equations and inequalities over ``nat`` are translated over - ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequalities are normalized. - * Goals are solved by the OMEGA decision procedure. - * The script of the solution is replayed. - -Overview of the OMEGA decision procedure -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The OMEGA decision procedure involved in the :tacn:`omega` tactic uses -a small subset of the decision procedure presented in :cite:`TheOmegaPaper` -Here is an overview, refer to the original paper for more information. - - * Equations and inequalities are normalized by division by the GCD of their - coefficients. - * Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. - * Note that each inequality cuts the Euclidean space in half. - * Inequalities are solved by projecting on the hyperspace - defined by cancelling one of the variables. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequalities from different classes define a - new edge in the projection. - * Redundant inequalities are eliminated or merged in new - equations that can be eliminated by the Banerjee test. - * The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure are not implemented, so the -decision procedure is only partial. - -Bugs ----- - - * The simplification procedure is very dumb and this results in - many redundant cases to explore. - - * Much too slow. - - * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index bf8174f246..f8d6b35226 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -778,10 +778,8 @@ The main changes include: of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. -Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq, -and we recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +Additionally, the `omega` tactic is deprecated in this version of Coq, +and we recommend users to switch to :tacn:`lia` in new proof scripts. See the `Changes in 8.12+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -1046,7 +1044,7 @@ Tactics <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). - **Changed:** The :g:`auto with zarith` tactic and variations (including - :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega` + :tacn:`intuition`) may now call :tacn:`lia` instead of `omega` (when the `Omega` module is loaded); more goals may be automatically solved, fewer section variables will be captured spuriously (`#11018 <https://github.com/coq/coq/pull/11018>`_, @@ -1142,7 +1140,7 @@ Tactics (`#11883 <https://github.com/coq/coq/pull/11883>`_, by Attila Gáspár). - **Deprecated:** - The :tacn:`omega` tactic is deprecated; + The `omega` tactic is deprecated; use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead (`#11976 <https://github.com/coq/coq/pull/11976>`_, by Vincent Laporte). @@ -2129,11 +2127,9 @@ The main changes brought by Coq version 8.11 are: - :ref:`Revision<811Reals>` of the :g:`Coq.Reals` library, its axiomatisation and instances of the constructive and classical real numbers. -Additionally, while the :tacn:`omega` tactic is not yet deprecated in +Additionally, while the `omega` tactic is not yet deprecated in this version of Coq, it should soon be the case and we already -recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter -<omega_chapter>`). +recommend users to switch to :tacn:`lia` in new proof scripts. The ``dev/doc/critical-bugs`` file documents the known critical bugs of Coq and affected releases. See the `Changes in 8.11+beta1`_ diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b1759bf71b..88fca93547 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1666,7 +1666,7 @@ Proving a subgoal as a separate lemma: abstract is chosen to get a fresh name. If the proof is closed with :cmd:`Qed`, the auxiliary lemma is inlined in the final proof term. - This is useful with tactics such as :tacn:`omega` or + This is useful with tactics such as :tacn:`discriminate` that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time @@ -2317,11 +2317,10 @@ performance issue. .. coqtop:: reset in - Set Warnings "-omega-is-deprecated". - Require Import Coq.omega.Omega. + Require Import Lia. Ltac mytauto := tauto. - Ltac tac := intros; repeat split; omega || mytauto. + Ltac tac := intros; repeat split; lia || mytauto. Notation max x y := (x + (y - x)) (only parsing). @@ -2340,7 +2339,7 @@ performance issue. Set Ltac Profiling. tac. Show Ltac Profile. - Show Ltac Profile "omega". + Show Ltac Profile "lia". .. coqtop:: in diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst index c3712b109d..e458c3a9f5 100644 --- a/doc/sphinx/proofs/automatic-tactics/index.rst +++ b/doc/sphinx/proofs/automatic-tactics/index.rst @@ -14,7 +14,6 @@ complex goals in new domains. :maxdepth: 1 logic - ../../addendum/omega ../../addendum/micromega ../../addendum/ring ../../addendum/nsatz |