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

library/init/meta/tactic.lean

@@ -114,6 +114,8 @@ meta_constant assert        : name → expr → tactic unit
 meta_constant rotate_left   : nat → tactic unit
 meta_constant get_goals     : tactic (list expr)
 meta_constant set_goals     : list expr → tactic unit
+meta_constant apply_core    : expr → transparency → tactic unit
+meta_constant fapply_core   : expr → transparency → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=
@@ -223,4 +225,11 @@ do gs ← get_goals,
    | g₁ :: g₂ :: rs := set_goals (g₂ :: g₁ :: rs)
    | _              := skip
    end
+
+meta_definition apply (e : expr) : tactic unit :=
+apply_core e transparency.semireducible
+
+meta_definition fapply (e : expr) : tactic unit :=
+fapply_core e transparency.semireducible
+
 end tactic

src/library/metavar_context.cpp

@@ -115,6 +115,15 @@ expr metavar_context::instantiate_mvars(expr const & e) {
     return ::lean::instantiate_mvars(impl, e);
 }
 
+void metavar_context::instantiate_mvars_at_type_of(expr const & m) {
+    metavar_decl d = *get_metavar_decl(m);
+    expr type      = d.get_type();
+    expr new_type  = instantiate_mvars(type);
+    if (new_type != type) {
+        m_decls.insert(mlocal_name(m), metavar_decl(d.get_context(), new_type));
+    }
+}
+
 template<typename C>
 static bool well_formed_metavar_occs(expr const & e, C const & ds, metavar_context const & ctx) {
     bool ok = true;

src/library/metavar_context.h

@@ -59,6 +59,10 @@ class metavar_context {
     optional<level> get_assignment(level const & l) const;
     optional<expr> get_assignment(expr const & e) const;
 
+    /** \brief Instantiate the assigned meta-variables in the type of \c m
+        \pre get_metavar_decl(m) is not none */
+    void instantiate_mvars_at_type_of(expr const & m);
+
     /** \brief Return true iff \c ctx is well-formed with respect to this metavar context.
         That is, every metavariable ?M occurring in \c ctx is declared here, and
         for every metavariable ?M occurring in a declaration \c d, the context of ?M

src/library/tactic/CMakeLists.txt

@@ -1,4 +1,5 @@
 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 assert_tactic.cpp elaborate.cpp init_module.cpp)
+  change_tactic.cpp assert_tactic.cpp apply_tactic.cpp
+  elaborate.cpp init_module.cpp)

src/library/tactic/apply_tactic.cpp

@@ -0,0 +1,122 @@
+/*
+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 "kernel/instantiate.h"
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+
+namespace lean {
+static unsigned get_expect_num_args(type_context & ctx, expr e) {
+    type_context::tmp_locals locals(ctx);
+    unsigned r = 0;
+    while (true) {
+        e = ctx.relaxed_whnf(e);
+        if (!is_pi(e))
+            return r;
+        // TODO(Leo): try to avoid the following instantiate.
+        expr local = locals.push_local(binding_name(e), binding_domain(e), binding_info(e));
+        e = instantiate(binding_body(e), local);
+        r++;
+    }
+}
+
+vm_obj apply_core(expr e, transparency_mode md, bool /* add_all */, 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, md);
+        local_context lctx   = g->get_context();
+        expr target          = g->get_type();
+        expr e_type          = ctx.infer(e);
+        unsigned num_e_t     = get_expect_num_args(ctx, e_type);
+        unsigned num_t       = get_expect_num_args(ctx, target);
+        if (num_t <= num_e_t)
+            num_e_t -= num_t;
+        else
+            num_e_t = 0;
+        /* Generate meta-variables for arguments */
+        buffer<expr> metas;
+        buffer<bool> is_instance;
+        for (unsigned i = 0; i < num_e_t; i++) {
+            e_type    = ctx.relaxed_whnf(e_type);
+            expr meta = mctx.mk_metavar_decl(lctx, binding_domain(e_type));
+            is_instance.push_back(binding_info(e_type).is_inst_implicit());
+            metas.push_back(meta);
+            e          = mk_app(e, meta);
+            e_type     = instantiate(binding_body(e_type), meta);
+        }
+        /* Unify */
+        lean_assert(metas.size() == is_instance.size());
+        if (!ctx.is_def_eq(target, e_type)) {
+            format msg = format("invalid apply tactic, failed to unify");
+            msg += pp_indented_expr(s, target);
+            msg += line() + format("with");
+            msg += pp_indented_expr(s, e_type);
+            return mk_tactic_exception(msg, s);
+        }
+        /* Synthesize type class instances */
+        unsigned i = is_instance.size();
+        while (i > 0) {
+            --i;
+            if (!is_instance[i]) continue;
+            expr const & meta   = metas[i];
+            if (mctx.is_assigned(meta)) continue;
+            expr meta_type      = ctx.infer(meta);
+            optional<expr> inst = ctx.mk_class_instance(meta_type);
+            if (!inst) {
+                return mk_tactic_exception(sstream() << "invalid apply tactic, failed to synthesize type class instance for #"
+                                           << (i+1) << " argument", s);
+            }
+            if (!ctx.is_def_eq(meta, *inst)) {
+                return mk_tactic_exception(sstream() << "invalid apply tactic, failed to assign type class instance for #"
+                                           << (i+1) << " argument", s);
+            }
+        }
+        /* Collect unassigned meta-variables */
+        buffer<expr> new_goals;
+        for (auto m : metas) {
+            if (!mctx.is_assigned(m)) {
+                mctx.instantiate_mvars_at_type_of(m);
+                new_goals.push_back(m);
+            }
+        }
+        /* TODO(Leo): remove redundant metas */
+
+        /* Assign, and create new tactic_state */
+        e = mctx.instantiate_mvars(e);
+        mctx.assign(head(s.goals()), e);
+        return mk_tactic_success(set_mctx_goals(s, mctx,
+                                                to_list(new_goals.begin(), new_goals.end(), tail(s.goals()))));
+    } catch(exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+vm_obj apply_core(expr const & e, transparency_mode md, tactic_state const & s) {
+    return apply_core(e, md, false, s);
+}
+
+vm_obj fapply_core(expr const & e, transparency_mode md, tactic_state const & s) {
+    return apply_core(e, md, true, s);
+}
+
+vm_obj tactic_apply_core(vm_obj const & e, vm_obj const & md, vm_obj const & s) {
+    return apply_core(to_expr(e), static_cast<transparency_mode>(cidx(md)), to_tactic_state(s));
+}
+
+vm_obj tactic_fapply_core(vm_obj const & e, vm_obj const & md, vm_obj const & s) {
+    return fapply_core(to_expr(e), static_cast<transparency_mode>(cidx(md)), to_tactic_state(s));
+}
+
+void initialize_apply_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "apply_core"}),   tactic_apply_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "fapply_core"}),  tactic_fapply_core);
+}
+
+void finalize_apply_tactic() {
+}
+}

src/library/tactic/apply_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_apply_tactic();
+void finalize_apply_tactic();
+}

src/library/tactic/init_module.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/tactic/exact_tactic.h"
 #include "library/tactic/change_tactic.h"
 #include "library/tactic/assert_tactic.h"
+#include "library/tactic/apply_tactic.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -28,10 +29,12 @@ void initialize_tactic_module() {
     initialize_exact_tactic();
     initialize_change_tactic();
     initialize_assert_tactic();
+    initialize_apply_tactic();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_apply_tactic();
     finalize_assert_tactic();
     finalize_change_tactic();
     finalize_exact_tactic();

tests/lean/run/apply1.lean

@@ -0,0 +1,8 @@
+open tactic
+
+example (p q : Prop) : p → q → p ∧ q :=
+by do
+  intros,
+  apply (expr.const ("and" <.> "intro") []),
+  trace_state,
+  all_goals assumption

tests/lean/run/apply2.lean

@@ -0,0 +1,7 @@
+open tactic
+
+example (p q : Prop) : p → q → p ∧ q ∧ p :=
+by do
+  intros,
+  c₁ ← return (expr.const ("and" <.> "intro") []),
+  repeat_at_most 10 (apply c₁ <|> assumption)