feat(library/tactic): add 'exact' tactic

library/init/meta/tactic.lean

@@ -100,6 +100,7 @@ meta_constant mk_app        : name → list expr → tactic expr
      @ite.{1} (a > b) (nat.decidable_gt a b) nat a b -/
 meta_constant mk_mapp       : name → list (option expr) → tactic expr
 meta_constant subst         : name → tactic unit
+meta_constant exact         : expr → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/tactic/CMakeLists.txt

@@ -1,3 +1,4 @@
 add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
   revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
-  app_builder_tactics.cpp subst_tactic.cpp elaborate.cpp init_module.cpp)
+  app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
+  elaborate.cpp init_module.cpp)

src/library/tactic/exact_tactic.cpp

@@ -0,0 +1,44 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+#include "library/tactic/app_builder_tactics.h"
+
+namespace lean {
+vm_obj exact(expr const & e, tactic_state const & s) {
+    try {
+        optional<metavar_decl> g = s.get_main_goal_decl();
+        if (!g) return mk_no_goals_exception(s);
+        metavar_context mctx = s.mctx();
+        type_context ctx     = mk_type_context_for(s, mctx);
+        expr e_type          = ctx.infer(e);
+        if (!ctx.is_def_eq(g->get_type(), e_type)) {
+            format r("exact tactic failed, type mismatch, given expression has type");
+            unsigned indent = get_pp_indent(s.get_options());
+            r += nest(indent, line() + pp_expr(s, e_type));
+            r += line() + format("but is expected to have type");
+            r += nest(indent, line() + pp_expr(s, g->get_type()));
+            return mk_tactic_exception(r, s);
+        }
+        mctx.assign(head(s.goals()), e);
+        return mk_tactic_success(set_mctx_goals(s, mctx, tail(s.goals())));
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+vm_obj tactic_exact(vm_obj const & e, vm_obj const & s) {
+    return exact(to_expr(e), to_tactic_state(s));
+}
+
+void initialize_exact_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "exact"}), tactic_exact);
+}
+
+void finalize_exact_tactic() {
+}
+}

src/library/tactic/exact_tactic.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_exact_tactic();
+void finalize_exact_tactic();
+}

src/library/tactic/init_module.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/tactic/clear_tactic.h"
 #include "library/tactic/app_builder_tactics.h"
 #include "library/tactic/subst_tactic.h"
+#include "library/tactic/exact_tactic.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -24,10 +25,12 @@ void initialize_tactic_module() {
     initialize_clear_tactic();
     initialize_app_builder_tactics();
     initialize_subst_tactic();
+    initialize_exact_tactic();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_exact_tactic();
     finalize_subst_tactic();
     finalize_app_builder_tactics();
     finalize_clear_tactic();

src/library/tactic/tactic_state.cpp

@@ -137,9 +137,13 @@ vm_obj tactic_state_to_format(vm_obj const & s) {
     return to_obj(to_tactic_state(s).pp(fmtf));
 }
 
-vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
+format pp_expr(tactic_state const & s, expr const & e) {
     formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
-    return to_obj(to_tactic_state(s).pp_expr(fmtf, to_expr(e)));
+    return s.pp_expr(fmtf, e);
+}
+
+vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
+    return to_obj(pp_expr(to_tactic_state(s), to_expr(e)));
 }
 
 optional<tactic_state> is_tactic_success(vm_obj const & o) {

src/library/tactic/tactic_state.h

@@ -93,6 +93,8 @@ vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s);
 vm_obj mk_tactic_exception(char const * msg, tactic_state const & s);
 vm_obj mk_no_goals_exception(tactic_state const & s);
 
+format pp_expr(tactic_state const & s, expr const & e);
+
 /* If r is (base_tactic_result.success a s), then return s */
 optional<tactic_state> is_tactic_success(vm_obj const & r);
 

tests/lean/run/exact_tac1.lean

@@ -0,0 +1,18 @@
+open tactic list
+
+example (a b : nat) : a = a :=
+by do
+  a ← get_local "a",
+  r ← mk_app ("eq" <.> "refl") [a],
+  exact r
+
+set_option pp.all true
+
+example (a b : nat) (f : nat → nat) : a = b → f a = f b :=
+by do
+  intro "H",
+  H ← get_local "H",
+  f ← get_local "f",
+  r ← mk_app "congr_arg" [f, H],
+  trace_expr r,
+  exact r