feat(library/tactic/tactic_state): add tactic.mk_instance

library/init/meta/tactic.lean

@@ -103,6 +103,9 @@ meta_constant subst         : name → tactic unit
 meta_constant exact         : expr → tactic unit
 /- Elaborate the given quoted expression with respect to the current main goal. -/
 meta_constant to_expr       : qexpr → tactic expr
+/- Try to create an instance of the given type class -/
+meta_constant mk_instance   : expr → tactic expr
+
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/tactic/tactic_state.cpp

@@ -276,6 +276,23 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & s0) {
     }
 }
 
+vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) {
+    tactic_state const & s = to_tactic_state(s0);
+    metavar_context mctx   = s.mctx();
+    type_context ctx       = mk_type_context_for(s, mctx);
+    try {
+        if (auto r = ctx.mk_class_instance(to_expr(e))) {
+            return mk_tactic_success(to_obj(*r), s);
+        } else {
+            format m("tactic.mk_instance failed to generate instance for");
+            m += nest(get_pp_indent(s.get_options()), line() + pp_expr(s, to_expr(e)));
+            return mk_tactic_exception(m, s);
+        }
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 vm_obj tactic_unify_core(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & s0) {
     tactic_state const & s = to_tactic_state(s0);
     metavar_context mctx   = s.mctx();
@@ -326,6 +343,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "format_result"}),     tactic_format_result);
     DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}),        tactic_infer_type);
     DECLARE_VM_BUILTIN(name({"tactic", "whnf"}),              tactic_whnf);
+    DECLARE_VM_BUILTIN(name({"tactic", "mk_instance"}),       tactic_mk_instance);
     DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}),        tactic_unify_core);
     DECLARE_VM_BUILTIN(name({"tactic", "get_local"}),         tactic_get_local);
     DECLARE_VM_BUILTIN(name({"tactic", "local_context"}),     tactic_local_context);

tests/lean/run/mk_instance1.lean

@@ -0,0 +1,18 @@
+open tactic
+
+example (a b : nat) : decidable (a = b) :=
+by do t ← mk_app "decidable_eq" [expr.const "nat" []],
+      i ← mk_instance t,
+      a ← get_local "a",
+      b ← get_local "b",
+      trace_expr i,
+      exact (expr.app (expr.app i a) b)
+
+example (a b : nat) : decidable (a = b) :=
+by do t ← target,
+      i ← mk_instance t,
+      trace_expr i,
+      exact i
+
+example (a b : nat) : decidable (a = b) :=
+by target >>= mk_instance >>= exact