From f8e91cb0a227a2d0423412e7533163568e1e9fdf Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Mon, 11 May 2020 11:59:42 +0200 Subject: [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. --- doc/changelog/04-tactics/11906-micromega-booleans.rst | 4 ++++ doc/sphinx/addendum/micromega.rst | 11 +++++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 doc/changelog/04-tactics/11906-micromega-booleans.rst (limited to 'doc') 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 `_, 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: -- cgit v1.2.3 From 12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Mon, 25 May 2020 17:28:53 +0200 Subject: Update zify documentation Add Zify are documented. Add is deprecated as it clashed with the standard Add command --- doc/sphinx/addendum/micromega.rst | 53 ++++++++++++++++++++++++++------------- 1 file changed, 35 insertions(+), 18 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 717b0deb43..c4947e6b3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -284,37 +284,54 @@ obtain :math:`-1`. By Theorem :ref:`Psatz `, 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. -- cgit v1.2.3