[zify] elim let in ML

6 files changed, 53 insertions, 21 deletions

diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst
new file mode 100644
index 0000000000..4eb2732106
--- /dev/null
+++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst
@@ -0,0 +1,3 @@
+- **Changed**
+  Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml.
+  (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson).
diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v
index 785a53fafa..18cd196148 100644
--- a/plugins/micromega/Zify.v
+++ b/plugins/micromega/Zify.v
@@ -87,4 +87,4 @@ Ltac applySpec S :=
 (** [zify_post_hook] is there to be redefined. *)
 Ltac zify_post_hook := idtac.
 
-Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook.
+Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook.
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 66f263c0b1..2b5fac32a2 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
 END
 
 TACTIC EXTEND ITER
-| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t }
+| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t }
 END
 
 TACTIC EXTEND TRANS
 | [ "zify_op"  ] -> { Zify.zify_tac }
-| [ "saturate"  ] -> { Zify.saturate }
+| [ "zify_saturate"  ] -> { Zify.saturate }
+| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t }
 END
 
 VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 5d8ae83853..e71c89b4db 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -965,6 +965,43 @@ let trans_concl t =
 let tclTHENOpt e tac tac' =
   match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
 
+let assert_inj t =
+  init_cache ();
+  Proofview.Goal.enter (fun gl ->
+      let env = Tacmach.New.pf_env gl in
+      let evd = Tacmach.New.project gl in
+      try
+        ignore (get_injection env evd t);
+        Tacticals.New.tclIDTAC
+      with Not_found ->
+        Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist"))
+
+let do_let tac (h : Constr.named_declaration) =
+  match h with
+  | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC
+  | Context.Named.Declaration.LocalDef (id, t, ty) ->
+    Proofview.Goal.enter (fun gl ->
+        let env = Tacmach.New.pf_env gl in
+        let evd = Tacmach.New.project gl in
+        try
+          ignore (get_injection env evd (EConstr.of_constr ty));
+          tac id.Context.binder_name t ty
+        with Not_found -> Tacticals.New.tclIDTAC)
+
+let iter_let tac =
+  Proofview.Goal.enter (fun gl ->
+      let env = Tacmach.New.pf_env gl in
+      let sign = Environ.named_context env in
+      Tacticals.New.tclMAP (do_let tac) sign)
+
+let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) =
+  init_cache ();
+  iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) ->
+      Ltac_plugin.Tacinterp.Value.apply tac
+        [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id)
+        ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t)
+        ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ])
+
 let zify_tac =
   Proofview.Goal.enter (fun gl ->
       Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"];
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 9e3cf5d24c..4930a845c9 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -27,3 +27,5 @@ module Saturate : S
 val zify_tac : unit Proofview.tactic
 val saturate : unit Proofview.tactic
 val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
+val assert_inj : EConstr.constr -> unit Proofview.tactic
+val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index f5d53cbbf3..34533670f8 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -573,27 +573,16 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 Require  Import ZifyClasses ZifyInst.
 Require  Zify.
 
-
-(** [is_inj T] returns true iff the type T has an injection *)
-Ltac is_inj T :=
-  match T with
-  | _  => let x := constr:(_ : InjTyp T _ ) in true
-  | _  => false
-  end.
-
 (* [elim_let] replaces a let binding (x := e : t)
    by an equation (x = e) if t is an injected type *)
-Ltac elim_let :=
-  repeat
-  match goal with
-  | x := ?t : ?ty |- _ =>
-         let b := is_inj ty in
-         match b with
-         | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
-         end
-  end.
 
+Ltac elim_binding x t ty :=
+  let h := fresh "heq_" x in
+  pose proof (@eq_refl ty x : @eq ty x t) as h;
+  try clearbody x.
+
+Ltac elim_let := zify_iter_let elim_binding.
 
 Ltac zify :=
   intros ; elim_let ;
-  Zify.zify  ; ZifyInst.saturate.
+  Zify.zify  ; ZifyInst.zify_saturate.