Merge PR #14108: [zify] bugfix

Reviewed-by: Zimmi48
Reviewed-by: vbgl

5 files changed, 52 insertions, 7 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index d718454364..24e35dd85a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    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:: Add Zify @add_zify @one_term
+.. cmd:: Add Zify @add_zify @qualid
 
    .. insertprodn add_zify add_zify
 
@@ -304,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
       | {| PropOp | PropBinOp | PropUOp | Saturate }
 
    Registers an instance of the specified typeclass.
+   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
+   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
+   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
 
 .. cmd:: Show Zify @show_zify
 
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index b780c1833e..3ea7408067 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -46,6 +46,7 @@ let mkrel = lazy (zify "mkrel")
 let iff_refl = lazy (zify "iff_refl")
 let eq_iff = lazy (zify "eq_iff")
 let rew_iff = lazy (zify "rew_iff")
+let rew_iff_rev = lazy (zify "rew_iff_rev")
 
 (* propositional logic *)
 
@@ -621,14 +622,20 @@ module MakeTable (E : Elt) = struct
       failwith ("Cannot register term " ^ t)
     | Some a -> E.mk_elt evd i a
 
+  let safe_ref evd c =
+    try
+      fst (EConstr.destRef evd c)
+    with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++
+                                          gl_pr_constr c ++ str " should be a global reference")
+
   let register_hint evd t elt =
     match EConstr.kind evd t with
     | App (c, _) ->
-      let gr = fst (EConstr.destRef evd c) in
-      E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+       let gr = safe_ref evd c in
+       E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
     | _ ->
-      let gr = fst (EConstr.destRef evd t) in
-      E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
+       let gr = safe_ref evd t in
+       E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
 
   let register_constr env evd c =
     let c = EConstr.of_constr c in
@@ -1365,7 +1372,15 @@ let trans_concl prfp =
         Tactics.change_concl t')
   | TProof (t, prf) ->
     Proofview.Goal.enter (fun gl ->
-        Equality.general_rewrite true Locus.AllOccurrences true false prf)
+        let env = Tacmach.New.pf_env gl in
+        let evd = Tacmach.New.project gl in
+        let typ = get_type_of env evd prf in
+        match EConstr.kind evd typ with
+        | App (c, a) when Array.length a = 2 ->
+          Tactics.apply
+            (EConstr.mkApp (Lazy.force rew_iff_rev, [|a.(0); a.(1); prf|]))
+        | _ ->
+          raise (CErrors.anomaly Pp.(str "zify cannot transform conclusion")))
 
 let tclTHENOpt e tac tac' =
   match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v
new file mode 100644
index 0000000000..e62b5b8d9e
--- /dev/null
+++ b/test-suite/micromega/bug_11089.v
@@ -0,0 +1,13 @@
+Require Import Lia.
+Unset Lia Cache.
+Definition t := nat.
+Goal forall (n : t), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
+Goal let t' := nat in forall (n : t'), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index a12623c3c0..2ea320047d 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -167,6 +167,12 @@ Goal  @zero znat = 0%nat.
   reflexivity.
 Qed.
 
+Require Import ZifyBool.
+Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
+  { TUOp := id; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_bool_inj.
+
+
 Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
     (F P + 1 = 1 + F P)%positive.
 Proof.
@@ -228,6 +234,7 @@ Proof.
   intros. lia.
 Qed.
 
+
 Ltac Zify.zify_pre_hook ::= unfold is_true in *.
 
 Goal forall x y : nat, is_true (Nat.eqb x 1) ->
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 019d11d951..25d9fa9104 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -7,7 +7,6 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-Set Primitive Projections.
 
 (** An alternative to [zify] in ML parametrised by user-provided classes instances.
 
@@ -220,6 +219,13 @@ Proof.
   exact (fun H => proj1 IFF H).
 Qed.
 
+Lemma rew_iff_rev  (P Q : Prop) (IFF : P <-> Q) :  Q -> P.
+Proof.
+  exact (fun H => proj2 IFF H).
+Qed.
+
+
+
 (** Registering constants for use by the plugin *)
 Register eq_iff      as ZifyClasses.eq_iff.
 Register target_prop as ZifyClasses.target_prop.
@@ -247,6 +253,7 @@ Register eq          as ZifyClasses.eq.
 Register mkinjprop   as ZifyClasses.mkinjprop.
 Register iff_refl    as ZifyClasses.iff_refl.
 Register rew_iff     as ZifyClasses.rew_iff.
+Register rew_iff_rev as ZifyClasses.rew_iff_rev.
 Register source_prop as ZifyClasses.source_prop.
 Register injprop_ok  as ZifyClasses.injprop_ok.
 Register iff         as ZifyClasses.iff.