From 2510d5722a707135f16ac8bdb6eee113d581f85f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Jun 2014 12:05:45 -0700
Subject: [PATCH] feat(frontends/lean): add unfold tactic command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_tactic_cmds.cpp | 9 +++++++++
 tests/lean/run/tactic4.lean                | 6 ++++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/lean/run/tactic4.lean

diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp
index add8c1653..4099e0cbc 100644
--- a/src/frontends/lean/builtin_tactic_cmds.cpp
+++ b/src/frontends/lean/builtin_tactic_cmds.cpp
@@ -17,6 +17,14 @@ tactic parse_id_tactic(parser &) { return id_tactic(); }
 tactic parse_now_tactic(parser &) { return now_tactic(); }
 tactic parse_show_tactic(parser &) { return trace_state_tactic(); }
 tactic parse_assumption_tactic(parser &) { return assumption_tactic(); }
+tactic parse_unfold_tactic(parser & p) {
+    auto pos = p.pos();
+    expr id  = p.parse_expr();
+    if (!is_constant(id))
+        throw parser_error("invalid 'unfold' tactic, constant expected", pos);
+    return unfold_tactic(const_name(id));
+}
+
 tactic parse_echo_tactic(parser & p) {
     if (!p.curr_is_string())
         throw parser_error("invalid 'echo' tactic, string expected", p.pos());
@@ -60,6 +68,7 @@ tactic_cmd_table get_builtin_tactic_cmds() {
     add_tactic(t, tactic_cmd_info("show", "show goals tactic", parse_show_tactic));
     add_tactic(t, tactic_cmd_info("now",  "succeeds only if all goals have been solved", parse_now_tactic));
     add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic));
+    add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic));
     add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic));
     add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion",
                                   parse_assumption_tactic));
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
new file mode 100644
index 000000000..28fee62b1
--- /dev/null
+++ b/tests/lean/run/tactic4.lean
@@ -0,0 +1,6 @@
+import logic
+
+definition id {A : Type} (a : A) := a
+
+theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
+:= by [unfold id, show, exact]