unify for Ltac2

Fixes #14083

6 files changed, 58 insertions, 0 deletions

diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
new file mode 100644
index 0000000000..a2de3ab763
--- /dev/null
+++ b/test-suite/ltac2/std_tactics.v
@@ -0,0 +1,34 @@
+Require Import Ltac2.Ltac2.
+
+Axiom f: nat -> nat.
+Definition g := f.
+
+Axiom Foo1: nat -> Prop.
+Axiom Foo2: nat -> Prop.
+Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n).
+
+Create HintDb foo discriminated.
+#[export] Hint Constants Opaque : foo.
+#[export] Hint Resolve Impl : foo.
+
+Goal forall x, Foo1 (f x) -> Foo2 (g x).
+Proof.
+  auto with foo.
+
+  #[export] Hint Transparent g : foo.
+
+  auto with foo.
+Qed.
+
+Goal forall (x: nat), exists y, f x = g y.
+Proof.
+  intros.
+  eexists.
+  unify f g.
+  Fail unify f g with core.
+  unify f g with foo.
+  lazy_match! goal with
+  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs with foo
+  end.
+  let dbname := @foo in Std.unify 'f 'g (Some dbname).
+Abort.
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 931d753521..77531121cb 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -593,6 +593,8 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0)))
 
 Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 
+Ltac2 Notation "unify" x(constr) y(constr) db(opt(seq("with", ident))) := Std.unify x y db.
+
 (** Congruence *)
 
 Ltac2 f_equal0 () := ltac1:(f_equal).
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index b69a95faf3..17741e563d 100644
--- a/user-contrib/Ltac2/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -259,3 +259,5 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden
 Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
+
+Ltac2 @ external unify : constr -> constr -> ident option -> unit := "ltac2" "tac_unify".
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index 895b6d3975..faa0499049 100644
--- a/user-contrib/Ltac2/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -572,3 +572,7 @@ end
 let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs ->
   Tac2tactics.typeclasses_eauto str n dbs
 end
+
+let () = define_prim3 "tac_unify" constr constr (option ident) begin fun x y db ->
+  Tac2tactics.unify x y db
+end
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 54f5a2cf68..de88f2e306 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -414,6 +414,20 @@ let typeclasses_eauto strategy depth dbs =
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
+let unify x y dbname =
+  match dbname with
+  | None -> Tactics.unify x y
+  | Some name ->
+    let base = Id.to_string name in
+    let table = try Some (Hints.searchtable_map base) with Not_found -> None in
+    match table with
+    | None ->
+      let msg = str "Hint table " ++ str base ++ str " not found" in
+      Tacticals.New.tclZEROMSG msg
+    | Some t ->
+      let state = Hints.Hint_db.transparent_state t in
+      Tactics.unify ~state x y
+
 (** Inversion *)
 
 let inversion knd arg pat ids =
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index f63f7e722a..44041a9e78 100644
--- a/user-contrib/Ltac2/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -119,6 +119,8 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
+val unify : constr -> constr -> Id.t option -> unit tactic
+
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic