Merge PR #11906: [micromega] native support for boolean operators

Reviewed-by: maximedenes
Reviewed-by: pi8027
Reviewed-by: vbgl

2 files changed, 48 insertions, 20 deletions

diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst
new file mode 100644
index 0000000000..39d1525ac3
--- /dev/null
+++ b/doc/changelog/04-tactics/11906-micromega-booleans.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`.
+  (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.)
+  (`#11906 <https://github.com/coq/coq/pull/11906>`_,  by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 77bf58aac6..c4947e6b3a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -64,16 +64,23 @@ arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\math
 The syntax of the formulas is the following:
 
  .. productionlist:: F
-   F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
+   F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F
    A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
    p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
 
-where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
+where :math:`F` is interpreted over either `Prop` or `bool`,
+:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
 operators :math:`−, +, ×` are respectively subtraction, addition, and product;
 :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
 For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of
 rationals ``==``.
 
+When :math:`F` is interpreted over `bool`, the boolean operators are
+`&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons
+in :math:`A` are also interpreted over the booleans (e.g., for
+:math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`,
+`Z.leb`).
+
 For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational
 constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the
 following expressions:
@@ -277,37 +284,54 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
    + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``.
 
+   The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
+   The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Show Zify InjTyp
-   :name: Show Zify InjTyp
+.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid
 
-   This command shows the list of types that can be injected into :g:`Z`.
+   This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``,  ``BinRel``,
+   ``UnOpSpec``, ``BinOpSpec``.
 
-.. cmd:: Show Zify BinOp
-   :name: Show Zify BinOp
+.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec }
 
-   This command shows the list of binary operators processed by :tacn:`zify`.
+   The command prints the typeclass instances of one the typeclasses
+   among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``,
+   ``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp``
+   prints the list of types that supported by :tacn:`zify` i.e.,
+   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. cmd:: Show Zify BinRel
-   :name: Show Zify BinRel
+.. cmd:: Show Zify Spec
 
-   This command shows the list of binary relations processed by :tacn:`zify`.
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``.
 
+.. cmd:: Add InjTyp
 
-.. cmd:: Show Zify UnOp
-   :name: Show Zify UnOp
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``InjTyp``.
 
-   This command shows the list of unary operators processed by :tacn:`zify`.
+.. cmd:: Add BinOp
 
-.. cmd:: Show Zify CstOp
-   :name: Show Zify CstOp
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``BinOp``.
+
+.. cmd:: Add UnOp
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``UnOp``.
+
+.. cmd:: Add CstOp
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``CstOp``.
+
+.. cmd:: Add BinRel
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``BinRel``.
 
-   This command shows the list of constants processed by :tacn:`zify`.
 
-.. cmd:: Show Zify Spec
-   :name: Show Zify Spec
 
-   This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`.
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#fnpsatz] Variants deal with equalities and strict inequalities.