From 727a4f5a3ad6961c4471d7aafc80b67db777e4f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Dec 2015 16:47:31 -0800
Subject: [PATCH] feat(library/tactic/intros_tactic): use '_' to say that some
 names are irrelevant in the intro tactic

See #695
---
 src/frontends/lean/parser.cpp        | 25 +++++++++++++++++++------
 src/library/tactic/intros_tactic.cpp |  2 ++
 tests/lean/run/intro_under.lean      |  5 +++++
 3 files changed, 26 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/intro_under.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9bb81b26c..c329d31ab 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1902,16 +1902,29 @@ expr parser::parse_tactic_expr_list() {
 expr parser::parse_tactic_id_list() {
     auto p = pos();
     buffer<expr> args;
-    if (curr_is_identifier()) {
-        while (curr_is_identifier()) {
-            name id = get_name_val();
+    if (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
+        while (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
+            name id;
+            if (curr_is_identifier())
+                id = get_name_val();
+            else
+                id = name("_");
             args.push_back(mk_local(id, mk_expr_placeholder()));
             next();
         }
     } else {
-        check_token_next(get_lbracket_tk(), "invalid tactic, '[' or identifier expected");
+        check_token_next(get_lbracket_tk(), "invalid tactic, '[', identifier or '_' expected");
         while (true) {
-            args.push_back(mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder()));
+            auto id_pos = pos();
+            name id;
+            if (curr_is_identifier())
+                id = get_name_val();
+            else if (curr_is_token(get_placeholder_tk()))
+                id = name("_");
+            else
+                throw parser_error("invalid tactic, identifier or '_' expected", id_pos);
+            next();
+            args.push_back(mk_local(id, mk_expr_placeholder()));
             if (!curr_is_token(get_comma_tk()))
                 break;
             next();
@@ -1933,7 +1946,7 @@ expr parser::parse_tactic_opt_expr_list() {
 }
 
 expr parser::parse_tactic_opt_id_list() {
-    if (curr_is_token(get_lbracket_tk()) || curr_is_identifier()) {
+    if (curr_is_token(get_lbracket_tk()) || curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
         return parse_tactic_id_list();
     } else if (curr_is_token(get_with_tk())) {
         next();
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index a102b1f4e..508be684a 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -44,6 +44,8 @@ static tactic intro_intros_tactic(list<name> _ns, bool is_intros) {
                 name new_name;
                 if (!is_nil(ns)) {
                     new_name = head(ns);
+                    if (new_name == "_")
+                        new_name = get_unused_name(binding_name(t), m);
                     ns       = tail(ns);
                 } else {
                     new_name = get_unused_name(binding_name(t), m);
diff --git a/tests/lean/run/intro_under.lean b/tests/lean/run/intro_under.lean
new file mode 100644
index 000000000..d863da66a
--- /dev/null
+++ b/tests/lean/run/intro_under.lean
@@ -0,0 +1,5 @@
+example (p q r : Prop) : p → q → r → r :=
+begin
+  intro _ _ Hr,
+  assumption
+end