Add a pre-hook mechanism for the `zify` tactic

4 files changed, 20 insertions, 3 deletions

diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
new file mode 100644
index 0000000000..975c917b19
--- /dev/null
+++ b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook`
+  tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index c4947e6b3a..c01e6a5aa6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -278,7 +278,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
    This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`.
    By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported.
-   :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`.
+   :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are
+   respectively run in the first and the last steps of :tacn:`zify`.
 
    + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index 8fd7398638..a12623c3c0 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -159,7 +159,7 @@ Require Import ZifyClasses.
 Require Import ZifyInst.
 
 Instance Zero : CstOp (@zero znat : nat) := Op_O.
-Add CstOp Zero.
+Add Zify CstOp Zero.
 
 
 Goal  @zero znat = 0%nat.
@@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
 Proof.
   intros. lia.
 Qed.
+
+Ltac Zify.zify_pre_hook ::= unfold is_true in *.
+
+Goal forall x y : nat, is_true (Nat.eqb x 1) ->
+                       is_true (Nat.eqb y 0) ->
+                       is_true (Nat.eqb (x + y) 1).
+Proof.
+lia.
+Qed.
diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v
index 2df3c57d32..183fd6a914 100644
--- a/theories/micromega/Zify.v
+++ b/theories/micromega/Zify.v
@@ -11,12 +11,15 @@
 Require Import ZifyClasses ZifyInst.
 Declare ML Module "zify_plugin".
 
-(** [zify_post_hook] is there to be redefined. *)
+(** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *)
+Ltac zify_pre_hook := idtac.
+
 Ltac zify_post_hook := idtac.
 
 Ltac iter_specs := zify_iter_specs.
 
 Ltac zify := intros;
+             zify_pre_hook ;
              zify_elim_let ;
              zify_op ;
              (zify_iter_specs) ;