From 2613e7c4443e4c38c177260a2e4be5fa2e4c86ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Apr 2015 16:03:22 -0700 Subject: [PATCH] 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 | 49 ++++++++++-------- library/init/tactic.lean | 47 +++++++++-------- src/frontends/lean/elaborator.cpp | 10 ++-- src/frontends/lean/parser.cpp | 59 +++++++++++++++++++--- src/frontends/lean/parser.h | 3 ++ src/library/constants.cpp | 12 +++++ src/library/constants.h | 3 ++ src/library/constants.txt | 3 ++ src/library/tactic/expr_to_tactic.cpp | 14 +++-- src/library/tactic/expr_to_tactic.h | 1 + tests/lean/tactic_id_bug.lean | 32 ++++++++++++ tests/lean/tactic_id_bug.lean.expected.out | 11 ++++ 12 files changed, 187 insertions(+), 57 deletions(-) create mode 100644 tests/lean/tactic_id_bug.lean create mode 100644 tests/lean/tactic_id_bug.lean.expected.out diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 39d2b5af6..cc4644f35 100644 --- a/hott/init/tactic.hlean +++ b/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 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 41fe83932..5f3334576 100644 --- a/library/init/tactic.lean +++ b/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 diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7b7c5647e..e858e8527 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7b8bd76a0..b1fcea993 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 parser::is_tactic_command(name & id) { return some_expr(type); } +expr parser::mk_tactic_expr_list(buffer 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(); - 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 mk_tactic_expr_list(args, p); +} + +expr parser::parse_tactic_id_list() { + auto p = pos(); + check_token_next(get_lbracket_tk(), "invalid tactic, '[' expected"); + buffer 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); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index cc2e31b47..f87fa3257 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -221,8 +221,11 @@ class parser { optional is_tactic_command(name & id); expr parse_tactic_led(expr left); expr parse_tactic_nud(); + expr mk_tactic_expr_list(buffer 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, diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 0d91a3591..778c32fc7 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index c97049f28..de0888819 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index b22594a04..01d53f76e 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 8f33bfb70..64c735b65 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/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_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_opcode = new std::string("TACE"); - g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); + 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_list_type = new expr(mk_constant(get_tactic_expr_list_name())); + g_tactic_identifier_type = new expr(mk_constant(get_tactic_identifier_name())); + 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; diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index c36778c2c..1b5c479af 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/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); diff --git a/tests/lean/tactic_id_bug.lean b/tests/lean/tactic_id_bug.lean new file mode 100644 index 000000000..a32786a22 --- /dev/null +++ b/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 diff --git a/tests/lean/tactic_id_bug.lean.expected.out b/tests/lean/tactic_id_bug.lean.expected.out new file mode 100644 index 000000000..9b6c574d8 --- /dev/null +++ b/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