From c8c43a866b758ffbd752c7a1fbdf2bd2044c06e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2016 09:06:35 -0700
Subject: [PATCH] feat(library/tactic): implement assumption tactic in Lean

---
 library/init/meta/tactic.lean            |  8 ++++-
 src/library/tactic/CMakeLists.txt        |  2 +-
 src/library/tactic/assumption_tactic.cpp | 40 ------------------------
 src/library/tactic/assumption_tactic.h   | 14 ---------
 src/library/tactic/init_module.cpp       |  3 --
 5 files changed, 8 insertions(+), 59 deletions(-)
 delete mode 100644 src/library/tactic/assumption_tactic.cpp
 delete mode 100644 src/library/tactic/assumption_tactic.h

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index a0402ef4a6..d009fb1110 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -65,7 +65,6 @@ meta_constant format_result : tactic format
 meta_constant target        : tactic expr
 meta_constant intro         : name → tactic unit
 meta_constant intron        : nat → tactic unit
-meta_constant assumption    : tactic unit
 meta_constant rename        : name → name → tactic unit
 meta_constant clear         : name → tactic unit
 meta_constant revert_lst    : list name → tactic unit
@@ -148,4 +147,11 @@ meta_definition find_same_type : expr → list expr → tactic expr
      if b = tt then return H
      else find_same_type e Hs
 
+meta_definition assumption : tactic unit :=
+do { ctx ← local_context,
+     t   ← target,
+     H   ← find_same_type t ctx,
+     exact H }
+<|> fail "assumption tactic failed"
+
 end tactic
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index e4e6da52ee..455a915cee 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
+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
   elaborate.cpp init_module.cpp)
diff --git a/src/library/tactic/assumption_tactic.cpp b/src/library/tactic/assumption_tactic.cpp
deleted file mode 100644
index 7813c2f497..0000000000
--- a/src/library/tactic/assumption_tactic.cpp
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
-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/tactic/tactic_state.h"
-
-namespace lean {
-optional<tactic_state> assumption(tactic_state const & s) {
-    optional<metavar_decl> g   = s.get_main_goal_decl();
-    lean_assert(g);
-    metavar_context mctx       = s.mctx();
-    type_context ctx           = mk_type_context_for(s, mctx, transparency_mode::Reducible);
-    local_context const & lctx = g->get_context();
-    expr const & type          = g->get_type();
-    optional<local_decl> d = lctx.back_find_if([&](local_decl const & d) {
-            return ctx.is_def_eq(type, d.get_type());
-        });
-    if (!d) return none_tactic_state();
-    mctx.assign(head(s.goals()), d->mk_ref());
-    return some_tactic_state(set_mctx_goals(s, mctx, tail(s.goals())));
-}
-
-vm_obj tactic_assumption(vm_obj const & s) {
-    optional<metavar_decl> g = to_tactic_state(s).get_main_goal_decl();
-    if (!g) return mk_no_goals_exception(to_tactic_state(s));
-    if (auto r = assumption(to_tactic_state(s)))
-        return mk_tactic_success(*r);
-    else
-        return mk_tactic_exception("assumption tactic failed", to_tactic_state(s));
-}
-
-void initialize_assumption_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "assumption"}), tactic_assumption);
-}
-
-void finalize_assumption_tactic() {
-}
-}
diff --git a/src/library/tactic/assumption_tactic.h b/src/library/tactic/assumption_tactic.h
deleted file mode 100644
index a86557d4bd..0000000000
--- a/src/library/tactic/assumption_tactic.h
+++ /dev/null
@@ -1,14 +0,0 @@
-/*
-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
-#include "library/tactic/tactic_state.h"
-
-namespace lean {
-optional<tactic_state> assumption(tactic_state const & s);
-void initialize_assumption_tactic();
-void finalize_assumption_tactic();
-}
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index edb100fe24..9f97dd172f 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/intro_tactic.h"
-#include "library/tactic/assumption_tactic.h"
 #include "library/tactic/revert_tactic.h"
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/clear_tactic.h"
@@ -19,7 +18,6 @@ namespace lean {
 void initialize_tactic_module() {
     initialize_tactic_state();
     initialize_intro_tactic();
-    initialize_assumption_tactic();
     initialize_revert_tactic();
     initialize_rename_tactic();
     initialize_clear_tactic();
@@ -36,7 +34,6 @@ void finalize_tactic_module() {
     finalize_clear_tactic();
     finalize_rename_tactic();
     finalize_revert_tactic();
-    finalize_assumption_tactic();
     finalize_intro_tactic();
     finalize_tactic_state();
 }