diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/11906-micromega-booleans.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 11 |
2 files changed, 13 insertions, 2 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..717b0deb43 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: |