From 0ff145e59b75a565ea1f26914b3994147319c3d3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Jul 2014 09:20:01 -0700
Subject: [PATCH] feat(library/tactic): add apply tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/tactic.lean          |  1 +
 src/library/tactic/expr_to_tactic.cpp |  1 +
 src/library/tactic/tactic.cpp         | 13 +++++++++++++
 src/library/tactic/tactic.h           |  8 +++++++-
 tests/lean/run/tactic16.lean          | 11 +++++++++++
 5 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/tactic16.lean

diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean
index 60583a5b1..bf753b59a 100644
--- a/library/standard/tactic.lean
+++ b/library/standard/tactic.lean
@@ -24,6 +24,7 @@ definition interleave (t1 t2 : tactic) : tactic := builtin_tactic
 definition par        (t1 t2 : tactic) : tactic := builtin_tactic
 definition repeat     (t : tactic) : tactic := builtin_tactic
 definition at_most    (t : tactic) (k : num)  : tactic := builtin_tactic
+definition discard    (t : tactic) (k : num)  : tactic := builtin_tactic
 definition focus_at   (t : tactic) (i : num)  : tactic := builtin_tactic
 definition try_for    (t : tactic) (ms : num) : tactic := builtin_tactic
 definition now        : tactic := builtin_tactic
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index d71946a3d..692055fef 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -185,6 +185,7 @@ static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr co
             return unfold_tactic(const_name(id));
     });
 static register_unary_num_tac reg_at_most(name(g_tac, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); });
+static register_unary_num_tac reg_discard(name(g_tac, "discard"), [](tactic const & t, unsigned k) { return discard(t, k); });
 static register_unary_num_tac reg_focus_at(name(g_tac, "focus_at"), [](tactic const & t, unsigned k) { return focus(t, k); });
 static register_unary_num_tac reg_try_for(name(g_tac, "try_for"), [](tactic const & t, unsigned k) { return try_for(t, k); });
 
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 5ad74634b..414720828 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -190,6 +190,19 @@ tactic take(tactic const & t, unsigned k) {
         });
 }
 
+tactic discard(tactic const & t, unsigned k) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+            auto r = t(env, ios, s);
+            for (unsigned i = 0; i < k; i++) {
+                auto m = r.pull();
+                if (!m)
+                    return proof_state_seq();
+                r = m->second;
+            }
+            return r;
+        });
+}
+
 tactic assumption_tactic() {
     return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             substitution subst = s.get_subst();
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 909efcf8e..2872174f5 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -112,9 +112,15 @@ tactic repeat(tactic const & t);
 tactic repeat_at_most(tactic const & t, unsigned k);
 /**
    \brief Return a tactic that applies \c t, but takes at most \c
-   k elements from the sequence produced by \c t.
+   \c k elements from the sequence produced by \c t.
 */
 tactic take(tactic const & t, unsigned k);
+/**
+   \brief Return a tactic that applies \c t, but discards the first
+   \c k elements from the sequence produced by \c t.
+*/
+tactic discard(tactic const & t, unsigned k);
+
 typedef std::function<bool(environment const & env, io_state const & ios, proof_state const & s)> proof_state_pred; // NOLINT
 /**
     \brief Return a tactic that applies the predicate \c p to the input state.
diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean
new file mode 100644
index 000000000..9afd25103
--- /dev/null
+++ b/tests/lean/run/tactic16.lean
@@ -0,0 +1,11 @@
+import standard
+using tactic
+
+variable A : Type.{1}
+variable f : A → A → A
+
+theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c)
+:= by discard (apply (subst H1)) 3;  -- discard the first 3 solutions produced by apply
+      trace "after subst H1";
+      apply (subst H2);
+      apply refl