feat(library/tactic/tactic_state): add 'is_class' and 'apply_instance' tactics

library/init/meta/tactic.lean

@@ -100,6 +100,8 @@ 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
+/- Return true if the given expression is a type class. -/
+meta_constant is_class      : expr → tactic bool
 /- Try to create an instance of the given type class. -/
 meta_constant mk_instance   : expr → tactic expr
 /- Simplify the given expression using [defeq] lemmas.
@@ -232,4 +234,10 @@ apply_core e transparency.semireducible
 meta_definition fapply (e : expr) : tactic unit :=
 fapply_core e transparency.semireducible
 
+meta_definition apply_instance : tactic unit :=
+do tgt ← target,
+   b   ← is_class tgt,
+   if b = tt then mk_instance tgt >>= exact
+   else fail "apply_instance tactic fail, target is not a type class"
+
 end tactic

src/library/tactic/tactic_state.cpp

@@ -292,6 +292,17 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & s0) {
     }
 }
 
+vm_obj tactic_is_class(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 {
+        return mk_tactic_success(mk_vm_bool(static_cast<bool>(ctx.is_class(to_expr(e)))), s);
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
 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();
@@ -406,6 +417,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", "is_class"}),          tactic_is_class);
     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);

tests/lean/run/apply4.lean

@@ -0,0 +1,16 @@
+open tactic
+
+constant foo {A : Type} [inhabited A] (a b : A) : a = default A → a = b
+
+example (a b : nat) : a = 0 → a = b :=
+by do
+  intro "H",
+  apply (expr.const "foo" [level.of_nat 1]),
+  trace_state,
+  assumption
+
+definition ex : inhabited (nat × nat × bool) :=
+by apply_instance
+
+set_option pp.all true
+print ex