fix(frontends/lean): bug when handling identifiers in tactics

This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ

hott/init/tactic.hlean

@@ -52,22 +52,6 @@ definition rotate (k : num) := rotate_left k
 inductive expr : Type :=
 builtin : expr
 
-opaque definition apply      (e : expr)   : tactic := builtin
-opaque definition rapply     (e : expr)   : tactic := builtin
-opaque definition fapply     (e : expr)   : tactic := builtin
-opaque definition rename     (a b : expr) : tactic := builtin
-opaque definition intro      (e : expr)   : tactic := builtin
-opaque definition generalize (e : expr)   : tactic := builtin
-opaque definition clear      (e : expr)   : tactic := builtin
-opaque definition revert     (e : expr)   : tactic := builtin
-opaque definition unfold     (e : expr)   : tactic := builtin
-opaque definition refine     (e : expr)   : tactic := builtin
-opaque definition exact      (e : expr)   : tactic := builtin
--- Relaxed version of exact that does not enforce goal type
-opaque definition rexact     (e : expr)   : tactic := builtin
-opaque definition check_expr (e : expr)   : tactic := builtin
-opaque definition trace      (s : string) : tactic := builtin
-
 inductive expr_list : Type :=
 | nil  : expr_list
 | cons : expr → expr_list → expr_list
@@ -75,23 +59,44 @@ inductive expr_list : Type :=
 -- auxiliary type used to mark optional list of arguments
 definition opt_expr_list := expr_list
 
+-- auxiliary types used to mark that the expression (list) is an identifier (list)
+definition identifier := expr
+definition identifier_list := expr_list
+definition opt_identifier_list := expr_list
+
+opaque definition apply      (e : expr)         : tactic := builtin
+opaque definition rapply     (e : expr)         : tactic := builtin
+opaque definition fapply     (e : expr)         : tactic := builtin
+opaque definition rename     (a b : identifier) : tactic := builtin
+opaque definition intro      (e : identifier)   : tactic := builtin
+opaque definition generalize (e : expr)         : tactic := builtin
+opaque definition clear      (e : identifier)   : tactic := builtin
+opaque definition revert     (e : identifier)   : tactic := builtin
+opaque definition unfold     (e : expr)         : tactic := builtin
+opaque definition refine     (e : expr)         : tactic := builtin
+opaque definition exact      (e : expr)         : tactic := builtin
+-- Relaxed version of exact that does not enforce goal type
+opaque definition rexact     (e : expr)         : tactic := builtin
+opaque definition check_expr (e : expr)         : tactic := builtin
+opaque definition trace      (s : string)       : tactic := builtin
+
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
-opaque definition rewrite_tac (e : expr_list)  : tactic := builtin
+opaque definition rewrite_tac (e : expr_list) : tactic := builtin
 
-opaque definition cases (id : expr) (ids : opt_expr_list) : tactic := builtin
+opaque definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 
-opaque definition intros (ids : opt_expr_list) : tactic := builtin
+opaque definition intros (ids : opt_identifier_list) : tactic := builtin
 
 opaque definition generalizes (es : expr_list) : tactic := builtin
 
-opaque definition clears (ids : expr_list) : tactic := builtin
+opaque definition clears  (ids : identifier_list) : tactic := builtin
 
-opaque definition reverts (ids : expr_list) : tactic := builtin
+opaque definition reverts (ids : identifier_list) : tactic := builtin
 
 opaque definition change (e : expr) : tactic := builtin
 
-opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
+opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
 infixl `;`:15 := and_then
 notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r

library/init/tactic.lean

@@ -52,22 +52,6 @@ definition rotate (k : num) := rotate_left k
 inductive expr : Type :=
 builtin : expr
 
-opaque definition apply      (e : expr)   : tactic := builtin
-opaque definition rapply     (e : expr)   : tactic := builtin
-opaque definition fapply     (e : expr)   : tactic := builtin
-opaque definition rename     (a b : expr) : tactic := builtin
-opaque definition intro      (e : expr)   : tactic := builtin
-opaque definition generalize (e : expr)   : tactic := builtin
-opaque definition clear      (e : expr)   : tactic := builtin
-opaque definition revert     (e : expr)   : tactic := builtin
-opaque definition unfold     (e : expr)   : tactic := builtin
-opaque definition refine     (e : expr)   : tactic := builtin
-opaque definition exact      (e : expr)   : tactic := builtin
--- Relaxed version of exact that does not enforce goal type
-opaque definition rexact     (e : expr)   : tactic := builtin
-opaque definition check_expr (e : expr)   : tactic := builtin
-opaque definition trace      (s : string) : tactic := builtin
-
 inductive expr_list : Type :=
 | nil  : expr_list
 | cons : expr → expr_list → expr_list
@@ -75,23 +59,44 @@ inductive expr_list : Type :=
 -- auxiliary type used to mark optional list of arguments
 definition opt_expr_list := expr_list
 
+-- auxiliary types used to mark that the expression (list) is an identifier (list)
+definition identifier := expr
+definition identifier_list := expr_list
+definition opt_identifier_list := expr_list
+
+opaque definition apply      (e : expr)         : tactic := builtin
+opaque definition rapply     (e : expr)         : tactic := builtin
+opaque definition fapply     (e : expr)         : tactic := builtin
+opaque definition rename     (a b : identifier) : tactic := builtin
+opaque definition intro      (e : identifier)   : tactic := builtin
+opaque definition generalize (e : expr)         : tactic := builtin
+opaque definition clear      (e : identifier)   : tactic := builtin
+opaque definition revert     (e : identifier)   : tactic := builtin
+opaque definition unfold     (e : expr)         : tactic := builtin
+opaque definition refine     (e : expr)         : tactic := builtin
+opaque definition exact      (e : expr)         : tactic := builtin
+-- Relaxed version of exact that does not enforce goal type
+opaque definition rexact     (e : expr)         : tactic := builtin
+opaque definition check_expr (e : expr)         : tactic := builtin
+opaque definition trace      (s : string)       : tactic := builtin
+
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
 opaque definition rewrite_tac (e : expr_list) : tactic := builtin
 
-opaque definition cases (id : expr) (ids : opt_expr_list) : tactic := builtin
+opaque definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 
-opaque definition intros (ids : opt_expr_list) : tactic := builtin
+opaque definition intros (ids : opt_identifier_list) : tactic := builtin
 
 opaque definition generalizes (es : expr_list) : tactic := builtin
 
-opaque definition clears  (ids : expr_list) : tactic := builtin
+opaque definition clears  (ids : identifier_list) : tactic := builtin
 
-opaque definition reverts (ids : expr_list) : tactic := builtin
+opaque definition reverts (ids : identifier_list) : tactic := builtin
 
 opaque definition change (e : expr) : tactic := builtin
 
-opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
+opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
 infixl `;`:15 := and_then
 notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r

src/frontends/lean/elaborator.cpp

@@ -607,13 +607,17 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
     }
     constraint_seq a_cs;
     expr d_type = binding_domain(f_type);
-    if (d_type == get_tactic_expr_type()) {
+    if (d_type == get_tactic_expr_type() || d_type == get_tactic_identifier_type()) {
         expr const & a = app_arg(e);
         expr r;
-        if (is_local(a) && (mlocal_type(a) == get_tactic_expr_type() || m_in_equation_lhs))
+        if (is_local(a) &&
+            (mlocal_type(a) == get_tactic_expr_type()
+             || mlocal_type(a) == get_tactic_identifier_type()
+             || m_in_equation_lhs)) {
             r = mk_app(f, a, e.get_tag());
-        else
+        } else {
             r = mk_app(f, mk_tactic_expr(a), e.get_tag());
+        }
         cs += f_cs + a_cs;
         return r;
     } else {

src/frontends/lean/parser.cpp

@@ -1352,6 +1352,18 @@ static bool is_tactic_opt_expr_list_type(expr const & e) {
     return is_constant(e) && const_name(e) == get_tactic_opt_expr_list_name();
 }
 
+static bool is_tactic_identifier_type(expr const & e) {
+    return is_constant(e) && const_name(e) == get_tactic_identifier_name();
+}
+
+static bool is_tactic_identifier_list_type(expr const & e) {
+    return is_constant(e) && const_name(e) == get_tactic_identifier_list_name();
+}
+
+static bool is_tactic_opt_identifier_list_type(expr const & e) {
+    return is_constant(e) && const_name(e) == get_tactic_opt_identifier_list_name();
+}
+
 static bool is_tactic_command_type(expr e) {
     while (is_pi(e))
         e = binding_body(e);
@@ -1370,6 +1382,16 @@ optional<expr> parser::is_tactic_command(name & id) {
     return some_expr(type);
 }
 
+expr parser::mk_tactic_expr_list(buffer<expr> const & args, pos_info const & p) {
+    unsigned i = args.size();
+    expr r = save_pos(mk_constant(get_tactic_expr_list_nil_name()), p);
+    while (i > 0) {
+        i--;
+        r = mk_app({save_pos(mk_constant(get_tactic_expr_list_cons_name()), p), args[i], r}, p);
+    }
+    return r;
+}
+
 expr parser::parse_tactic_expr_list() {
     auto p = pos();
     check_token_next(get_lbracket_tk(), "invalid tactic, '[' expected");
@@ -1381,13 +1403,21 @@ expr parser::parse_tactic_expr_list() {
         next();
     }
     check_token_next(get_rbracket_tk(), "invalid tactic, ',' or ']' expected");
-    unsigned i = args.size();
+    return mk_tactic_expr_list(args, p);
-    expr r = save_pos(mk_constant(get_tactic_expr_list_nil_name()), p);
+}
-    while (i > 0) {
+
-        i--;
+expr parser::parse_tactic_id_list() {
-        r = mk_app({save_pos(mk_constant(get_tactic_expr_list_cons_name()), p), args[i], r}, p);
+    auto p = pos();
+    check_token_next(get_lbracket_tk(), "invalid tactic, '[' expected");
+    buffer<expr> args;
+    while (true) {
+        args.push_back(mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder()));
+        if (!curr_is_token(get_comma_tk()))
+            break;
+        next();
     }
-    return r;
+    check_token_next(get_rbracket_tk(), "invalid tactic, ',' or ']' expected");
+    return mk_tactic_expr_list(args, p);
 }
 
 expr parser::parse_tactic_opt_expr_list() {
@@ -1401,6 +1431,17 @@ expr parser::parse_tactic_opt_expr_list() {
     }
 }
 
+expr parser::parse_tactic_opt_id_list() {
+    if (curr_is_token(get_lbracket_tk())) {
+        return parse_tactic_id_list();
+    } else if (curr_is_token(get_with_tk())) {
+        next();
+        return parse_tactic_id_list();
+    } else {
+        return save_pos(mk_constant(get_tactic_expr_list_nil_name()), pos());
+    }
+}
+
 expr parser::parse_tactic_nud() {
     if (curr_is_identifier()) {
         auto id_pos = pos();
@@ -1417,6 +1458,12 @@ expr parser::parse_tactic_nud() {
                     r = mk_app(r, parse_tactic_expr_list(), id_pos);
                 } else if (is_tactic_opt_expr_list_type(d)) {
                     r = mk_app(r, parse_tactic_opt_expr_list(), id_pos);
+                } else if (is_tactic_identifier_type(d)) {
+                    r = mk_app(r, mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder()), id_pos);
+                } else if (is_tactic_identifier_list_type(d)) {
+                    r = mk_app(r, parse_tactic_id_list(), id_pos);
+                } else if (is_tactic_opt_identifier_list_type(d)) {
+                    r = mk_app(r, parse_tactic_opt_id_list(), id_pos);
                 } else {
                     r = mk_app(r, parse_expr(get_max_prec()), id_pos);
                 }

src/frontends/lean/parser.h

@@ -221,8 +221,11 @@ class parser {
     optional<expr> is_tactic_command(name & id);
     expr parse_tactic_led(expr left);
     expr parse_tactic_nud();
+    expr mk_tactic_expr_list(buffer<expr> const & args, pos_info const & p);
     expr parse_tactic_expr_list();
     expr parse_tactic_opt_expr_list();
+    expr parse_tactic_id_list();
+    expr parse_tactic_opt_id_list();
 
 public:
     parser(environment const & env, io_state const & ios,

src/library/constants.cpp

@@ -86,6 +86,9 @@ name const * g_tactic_expr_builtin = nullptr;
 name const * g_tactic_expr_list = nullptr;
 name const * g_tactic_expr_list_cons = nullptr;
 name const * g_tactic_expr_list_nil = nullptr;
+name const * g_tactic_identifier = nullptr;
+name const * g_tactic_identifier_list = nullptr;
+name const * g_tactic_opt_identifier_list = nullptr;
 name const * g_tactic_fail = nullptr;
 name const * g_tactic_fixpoint = nullptr;
 name const * g_tactic_focus_at = nullptr;
@@ -203,6 +206,9 @@ void initialize_constants() {
     g_tactic_expr_list = new name{"tactic", "expr_list"};
     g_tactic_expr_list_cons = new name{"tactic", "expr_list", "cons"};
     g_tactic_expr_list_nil = new name{"tactic", "expr_list", "nil"};
+    g_tactic_identifier = new name{"tactic", "identifier"};
+    g_tactic_identifier_list = new name{"tactic", "identifier_list"};
+    g_tactic_opt_identifier_list = new name{"tactic", "opt_identifier_list"};
     g_tactic_fail = new name{"tactic", "fail"};
     g_tactic_fixpoint = new name{"tactic", "fixpoint"};
     g_tactic_focus_at = new name{"tactic", "focus_at"};
@@ -321,6 +327,9 @@ void finalize_constants() {
     delete g_tactic_expr_list;
     delete g_tactic_expr_list_cons;
     delete g_tactic_expr_list_nil;
+    delete g_tactic_identifier;
+    delete g_tactic_identifier_list;
+    delete g_tactic_opt_identifier_list;
     delete g_tactic_fail;
     delete g_tactic_fixpoint;
     delete g_tactic_focus_at;
@@ -438,6 +447,9 @@ name const & get_tactic_expr_builtin_name() { return *g_tactic_expr_builtin; }
 name const & get_tactic_expr_list_name() { return *g_tactic_expr_list; }
 name const & get_tactic_expr_list_cons_name() { return *g_tactic_expr_list_cons; }
 name const & get_tactic_expr_list_nil_name() { return *g_tactic_expr_list_nil; }
+name const & get_tactic_identifier_name() { return *g_tactic_identifier; }
+name const & get_tactic_identifier_list_name() { return *g_tactic_identifier_list; }
+name const & get_tactic_opt_identifier_list_name() { return *g_tactic_opt_identifier_list; }
 name const & get_tactic_fail_name() { return *g_tactic_fail; }
 name const & get_tactic_fixpoint_name() { return *g_tactic_fixpoint; }
 name const & get_tactic_focus_at_name() { return *g_tactic_focus_at; }

src/library/constants.h

@@ -88,6 +88,9 @@ name const & get_tactic_expr_builtin_name();
 name const & get_tactic_expr_list_name();
 name const & get_tactic_expr_list_cons_name();
 name const & get_tactic_expr_list_nil_name();
+name const & get_tactic_identifier_name();
+name const & get_tactic_identifier_list_name();
+name const & get_tactic_opt_identifier_list_name();
 name const & get_tactic_fail_name();
 name const & get_tactic_fixpoint_name();
 name const & get_tactic_focus_at_name();

src/library/constants.txt

@@ -81,6 +81,9 @@ tactic.expr.builtin
 tactic.expr_list
 tactic.expr_list.cons
 tactic.expr_list.nil
+tactic.identifier
+tactic.identifier_list
+tactic.opt_identifier_list
 tactic.fail
 tactic.fixpoint
 tactic.focus_at

src/library/tactic/expr_to_tactic.cpp

@@ -62,10 +62,12 @@ bool has_tactic_decls(environment const & env) {
 static expr * g_tactic_expr_type = nullptr;
 static expr * g_tactic_expr_builtin = nullptr;
 static expr * g_tactic_expr_list_type = nullptr;
+static expr * g_tactic_identifier_type = nullptr;
 
 expr const & get_tactic_expr_type() { return *g_tactic_expr_type; }
 expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; }
 expr const & get_tactic_expr_list_type() { return *g_tactic_expr_list_type; }
+expr const & get_tactic_identifier_type() { return *g_tactic_identifier_type; }
 
 static std::string * g_tactic_expr_opcode = nullptr;
 static std::string * g_tactic_opcode = nullptr;
@@ -321,11 +323,12 @@ void initialize_expr_to_tactic() {
 
     g_map               = new expr_to_tactic_map();
 
-    g_tactic_expr_type      = new expr(mk_constant(get_tactic_expr_name()));
+    g_tactic_expr_type       = new expr(mk_constant(get_tactic_expr_name()));
-    g_tactic_expr_builtin   = new expr(mk_constant(get_tactic_expr_builtin_name()));
+    g_tactic_expr_builtin    = new expr(mk_constant(get_tactic_expr_builtin_name()));
-    g_tactic_expr_list_type = new expr(mk_constant(get_tactic_expr_list_name()));
+    g_tactic_expr_list_type  = new expr(mk_constant(get_tactic_expr_list_name()));
-    g_tactic_expr_opcode    = new std::string("TACE");
+    g_tactic_identifier_type = new expr(mk_constant(get_tactic_identifier_name()));
-    g_tactic_expr_macro     = new macro_definition(new tactic_expr_macro_definition_cell());
+    g_tactic_expr_opcode     = new std::string("TACE");
+    g_tactic_expr_macro      = new macro_definition(new tactic_expr_macro_definition_cell());
 
     register_macro_deserializer(*g_tactic_expr_opcode,
                                 [](deserializer &, unsigned num, expr const * args) {
@@ -396,6 +399,7 @@ void finalize_expr_to_tactic() {
     delete g_tactic_expr_type;
     delete g_tactic_expr_builtin;
     delete g_tactic_expr_list_type;
+    delete g_tactic_identifier_type;
     delete g_tactic_expr_opcode;
     delete g_tactic_expr_macro;
     delete g_fixpoint_tac;

src/library/tactic/expr_to_tactic.h

@@ -30,6 +30,7 @@ tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr con
 name const & get_tactic_name();
 
 expr const & get_tactic_expr_type();
+expr const & get_tactic_identifier_type();
 expr mk_tactic_expr(expr const & e);
 bool is_tactic_expr(expr const & e);
 expr const & get_tactic_expr_expr(expr const & e);

tests/lean/tactic_id_bug.lean

@@ -0,0 +1,32 @@
+import algebra.function
+import logic.funext
+
+open function
+
+structure bijection (A : Type) :=
+(func finv : A → A)
+(linv : finv ∘ func = id)
+(rinv : func ∘ finv = id)
+
+attribute bijection.func [coercion]
+
+namespace bijection
+  variable {A : Type}
+
+  protected theorem eq {f g : bijection A}
+    (func_eq : func f = func g) (finv_eq : finv f = finv g) : f = g :=
+  begin
+    revert finv_eq,
+    revert func_eq,
+    cases g with [gfunc, gfinv, glinv, grinv],
+    cases f with [func, finv, linv, rinv],
+    state,
+    esimp,
+    intros [func_eq, finv_eq],
+    revert grinv, revert glinv, revert rinv, revert linv,
+    rewrite [func_eq, finv_eq],
+    intros [H1, H2, H3, H4],
+    apply rfl
+  end
+
+end bijection

tests/lean/tactic_id_bug.lean.expected.out

@@ -0,0 +1,11 @@
+tactic_id_bug.lean:23:4: proof state
+A : Type,
+gfunc gfinv : A → A,
+glinv : gfinv ∘ gfunc = id,
+grinv : gfunc ∘ gfinv = id,
+func finv : A → A,
+linv : finv ∘ func = id,
+rinv : func ∘ finv = id
+⊢ func (mk func finv linv rinv) = func (mk gfunc gfinv glinv grinv) →
+  finv (mk func finv linv rinv) = finv (mk gfunc gfinv glinv grinv) →
+  mk func finv linv rinv = mk gfunc gfinv glinv grinv