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

Remark: the new assert tactic does have the problem described in issue #621

library/init/meta/tactic.lean

@@ -110,6 +110,8 @@ meta_constant defeq_simp    : expr → tactic expr
 /- Change the target of the main goal.
    The input expression must be definitionally equal to the current target. -/
 meta_constant change        : expr → tactic unit
+/- (assert H T), adds a new goal for T, and the hypothesis (H : T := ?M) in the current goal -/
+meta_constant assert        : name → expr → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/tactic/CMakeLists.txt

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

src/library/tactic/assert_tactic.cpp

@@ -0,0 +1,43 @@
+/*
+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/lazy_abstraction.h"
+#include "library/vm/vm_name.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+vm_obj assert_core(name const & n, expr const & e, tactic_state const & s) {
+    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);
+    if (!is_sort(ctx.whnf(ctx.infer(e)))) {
+        format msg("invalid assert tactic, expression is not a type");
+        msg += pp_indented_expr(s, e);
+        return mk_tactic_exception(msg, s);
+    }
+    local_context lctx   = g->get_context();
+    expr new_M_1         = mctx.mk_metavar_decl(lctx, e);
+    expr l               = lctx.mk_local_decl(n, e, new_M_1);
+    expr new_M_2         = mctx.mk_metavar_decl(lctx, g->get_type());
+    expr new_val         = mk_let(n, e, new_M_1, mk_lazy_abstraction(new_M_2, mlocal_name(l)));
+    mctx.assign(head(s.goals()), new_val);
+    list<expr> new_gs    = cons(new_M_1, cons(new_M_2, tail(s.goals())));
+    return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
+}
+
+vm_obj tactic_assert(vm_obj const & n, vm_obj const & e, vm_obj const & s) {
+    return assert_core(to_name(n), to_expr(e), to_tactic_state(s));
+}
+
+void initialize_assert_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "assert"}),   tactic_assert);
+}
+
+void finalize_assert_tactic() {
+}
+}

src/library/tactic/assert_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_assert_tactic();
+void finalize_assert_tactic();
+}

src/library/tactic/init_module.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/tactic/subst_tactic.h"
 #include "library/tactic/exact_tactic.h"
 #include "library/tactic/change_tactic.h"
+#include "library/tactic/assert_tactic.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -26,10 +27,12 @@ void initialize_tactic_module() {
     initialize_subst_tactic();
     initialize_exact_tactic();
     initialize_change_tactic();
+    initialize_assert_tactic();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_assert_tactic();
     finalize_change_tactic();
     finalize_exact_tactic();
     finalize_subst_tactic();

tests/lean/run/assert_tac1.lean

@@ -0,0 +1,10 @@
+open tactic
+
+definition tst1 (a : nat) : a = a :=
+by do
+   assert "x" (expr.const "nat" []),
+   trace_state,
+   a ← get_local "a",
+   exact a,
+   x ← get_local "x",
+   mk_app ("eq" <.> "refl") [x] >>= exact