diff options
| author | Frédéric Besson | 2020-05-11 11:59:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-14 11:26:41 +0200 |
| commit | f8e91cb0a227a2d0423412e7533163568e1e9fdf (patch) | |
| tree | 3a16a91e7167cb942686ab6657b76e3b86c151df /doc | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[micromega] native support for boolean operators
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
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: |