From ca110012d8ad80c52a8032485ce2e7dbb30ad76b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 May 2015 21:57:28 -0700 Subject: [PATCH] feat(library/tactic): automate "generalize-intro-induction/cases" idiom closes #645 --- hott/init/tactic.hlean | 4 +- library/init/tactic.lean | 4 +- src/frontends/lean/parser.cpp | 3 +- src/library/tactic/generalize_tactic.cpp | 108 ++++++++++++++--------- src/library/tactic/generalize_tactic.h | 3 + src/library/tactic/induction_tactic.cpp | 31 ++++++- src/library/tactic/inversion_tactic.cpp | 26 +++++- tests/lean/errors.lean.expected.out | 2 +- tests/lean/run/645a.lean | 22 +++++ 9 files changed, 148 insertions(+), 55 deletions(-) create mode 100644 tests/lean/run/645a.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index d1b43860e9..d51e75e81a 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -91,9 +91,9 @@ definition rewrite_tac (e : expr_list) : tactic := builtin definition xrewrite_tac (e : expr_list) : tactic := builtin definition krewrite_tac (e : expr_list) : tactic := builtin -definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin +definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin -definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin +definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin definition intros (ids : opt_identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 72dd1a8520..895d0714c2 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -91,9 +91,9 @@ definition rewrite_tac (e : expr_list) : tactic := builtin definition xrewrite_tac (e : expr_list) : tactic := builtin definition krewrite_tac (e : expr_list) : tactic := builtin -definition cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin +definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin -definition induction (h : identifier) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin +definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin definition intros (ids : opt_identifier_list) : tactic := builtin diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8afffcaa89..ec353f5257 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1588,7 +1588,8 @@ expr parser::parse_tactic_nud() { r = mk_app(r, parse_tactic_option_num(), id_pos); } else { unsigned rbp; - if (arity == 1 || (arity == 2 && i == 0 && is_tactic_opt_identifier_list_type(ds[1]))) + if ((arity == 1) || + (arity >= 2 && i == 0 && (is_tactic_opt_identifier_list_type(ds[1]) || is_tactic_using_expr(ds[1])))) rbp = 0; else rbp = get_max_prec(); diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 7c028d6f58..8a354f0b42 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "library/constants.h" #include "kernel/abstract.h" +#include "kernel/instantiate.h" #include "kernel/kernel_exception.h" #include "library/reducible.h" #include "library/util.h" @@ -18,50 +19,73 @@ expr mk_generalize_tactic_expr(expr const & e, name const & id) { e, mk_constant(id)); } +optional generalize_core(environment const & env, io_state const & ios, elaborate_fn const & elab, + expr const & e, name const & x, proof_state const & s, name const & tac_name, + bool intro) { + proof_state new_s = s; + if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) { + name_generator ngen = new_s.get_ngen(); + substitution subst = new_s.get_subst(); + goals const & gs = new_s.get_goals(); + goal const & g = head(gs); + auto tc = mk_type_checker(env, ngen.mk_child()); + auto e_t_cs = tc->infer(*new_e); + if (e_t_cs.second) { + throw_tactic_exception_if_enabled(s, sstream() << "invalid '" << tac_name << "' tactic, unification constraints " + "have been generated when inferring type"); + return none_proof_state(); // constraints were generated + } + expr e_t = e_t_cs.first; + expr t = subst.instantiate(g.get_type()); + name n; + if (is_constant(e)) + n = const_name(e); + else if (is_local(e)) + n = local_pp_name(e); + else + n = x; + expr new_t, new_m, new_val; + if (intro) { + buffer hyps; + g.get_hyps(hyps); + expr new_h = mk_local(ngen.next(), get_unused_name(x, hyps), e_t, binder_info()); + new_t = instantiate(abstract(t, *new_e), new_h); + new_m = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t))); + new_m = mk_app(new_m, hyps); + new_val = mk_app(new_m, *new_e); + new_m = mk_app(new_m, new_h); + } else { + new_t = mk_pi(n, e_t, abstract(t, *new_e)); + new_m = g.mk_meta(ngen.next(), new_t); + new_val = mk_app(new_m, *new_e); + } + try { + check_term(*tc, g.abstract(new_t)); + } catch (kernel_exception const & ex) { + std::shared_ptr ex_ptr(static_cast(ex.clone())); + throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) { + format r = format("invalid '") + format(tac_name) + format("' tactic, type error"); + r += line(); + r += ex_ptr->pp(fmt); + return r; + }); + return none_proof_state(); + } + assign(subst, g, new_val); + goal new_g(new_m, new_t); + return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen)); + } + return none_proof_state(); +} + +optional generalize(environment const & env, io_state const & ios, elaborate_fn const & elab, + expr const & e, name const & x, proof_state const & s) { + return generalize_core(env, ios, elab, e, x, s, "generalize", false); +} + tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const & x) { return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { - proof_state new_s = s; - if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) { - name_generator ngen = new_s.get_ngen(); - substitution subst = new_s.get_subst(); - goals const & gs = new_s.get_goals(); - goal const & g = head(gs); - auto tc = mk_type_checker(env, ngen.mk_child()); - auto e_t_cs = tc->infer(*new_e); - if (e_t_cs.second) { - throw_tactic_exception_if_enabled(s, "invalid 'generalize' tactic, unification constraints " - "have been generated when inferring type"); - return none_proof_state(); // constraints were generated - } - expr e_t = e_t_cs.first; - expr t = subst.instantiate(g.get_type()); - name n; - if (is_constant(e)) - n = const_name(e); - else if (is_local(e)) - n = local_pp_name(e); - else - n = x; - expr new_t = mk_pi(n, e_t, abstract(t, *new_e)); - expr new_m = g.mk_meta(ngen.next(), new_t); - try { - check_term(*tc, g.abstract(new_t)); - } catch (kernel_exception const & ex) { - std::shared_ptr ex_ptr(static_cast(ex.clone())); - throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) { - format r = format("invalid 'generalize' tactic, type error"); - r += line(); - r += ex_ptr->pp(fmt); - return r; - }); - return none_proof_state(); - } - - assign(subst, g, mk_app(new_m, *new_e)); - goal new_g(new_m, new_t); - return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen)); - } - return none_proof_state(); + return generalize(env, ios, elab, e, x, s); }); } diff --git a/src/library/tactic/generalize_tactic.h b/src/library/tactic/generalize_tactic.h index 03daddf41e..6915ed21cf 100644 --- a/src/library/tactic/generalize_tactic.h +++ b/src/library/tactic/generalize_tactic.h @@ -9,6 +9,9 @@ Author: Leonardo de Moura namespace lean { expr mk_generalize_tactic_expr(expr const & e, name const & id); +optional generalize_core(environment const & env, io_state const & ios, elaborate_fn const & elab, + expr const & e, name const & x, proof_state const & s, name const & tac_name, + bool intro); void initialize_generalize_tactic(); void finalize_generalize_tactic(); } diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index dd8d9efa51..57fa2f22ef 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" +#include "library/tactic/generalize_tactic.h" #include "library/tactic/class_instance_synth.h" namespace lean { @@ -386,14 +387,30 @@ tactic induction_tactic(name const & H, optional rec, list const & i return tactic01(fn); } +tactic induction_tactic(elaborate_fn const & elab, expr const & H, optional rec, list const & ids, expr const & ref) { + auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) { + name Haux{"H", "ind"}; + auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "induction", true); + if (!new_ps) + return proof_state_seq(); + goal g = head(new_ps->get_goals()); + expr new_H = app_arg(g.get_meta()); + lean_assert(is_local(new_H)); + name H_name = local_pp_name(new_H); + return induction_tactic(H_name, rec, ids, ref)(env, ios, *new_ps); + }; + return tactic(fn); +} + void initialize_induction_tactic() { register_tac(name{"tactic", "induction"}, - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { buffer args; get_app_args(e, args); if (args.size() != 3) throw expr_to_tactic_exception(e, "invalid 'induction' tactic, insufficient number of arguments"); - name H = tactic_expr_to_id(args[0], "invalid 'induction' tactic, argument must be an identifier"); + check_tactic_expr(args[0], "invalid 'induction' tactic, argument must be an expression"); + expr H = get_tactic_expr_expr(args[0]); buffer ids; get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected"); check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument"); @@ -403,9 +420,15 @@ void initialize_induction_tactic() { } name const & cname = const_name(rec); if (cname == get_tactic_none_expr_name()) { - return induction_tactic(H, optional(), to_list(ids.begin(), ids.end()), e); + if (is_local(H)) + return induction_tactic(local_pp_name(H), optional(), to_list(ids.begin(), ids.end()), e); + else + return induction_tactic(elab, H, optional(), to_list(ids.begin(), ids.end()), e); } else { - return induction_tactic(H, optional(cname), to_list(ids.begin(), ids.end()), e); + if (is_local(H)) + return induction_tactic(local_pp_name(H), optional(cname), to_list(ids.begin(), ids.end()), e); + else + return induction_tactic(elab, H, optional(), to_list(ids.begin(), ids.end()), e); } }); } diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index dcab3b7c43..0fdb2db129 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" #include "library/tactic/class_instance_synth.h" #include "library/tactic/inversion_tactic.h" +#include "library/tactic/generalize_tactic.h" #include "library/tactic/clear_tactic.h" namespace lean { @@ -1112,13 +1113,32 @@ tactic inversion_tactic(name const & n, list const & ids) { return tactic01(fn); } +tactic inversion_tactic(elaborate_fn const & elab, expr const & H, list const & ids) { + auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) { + name Haux{"H", "cases"}; + auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "cases", true); + if (!new_ps) + return proof_state_seq(); + goal g = head(new_ps->get_goals()); + expr new_H = app_arg(g.get_meta()); + lean_assert(is_local(new_H)); + name H_name = local_pp_name(new_H); + return inversion_tactic(H_name, ids)(env, ios, *new_ps); + }; + return tactic(fn); +} + void initialize_inversion_tactic() { register_tac(get_tactic_cases_name(), - [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an identifier"); + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(app_fn(e)), "invalid 'cases' tactic, argument must be an expression"); + expr H = get_tactic_expr_expr(app_arg(app_fn(e))); buffer ids; get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases' tactic, list of identifiers expected"); - return inversion_tactic(n, to_list(ids.begin(), ids.end())); + if (is_local(H)) + return inversion_tactic(local_pp_name(H), to_list(ids.begin(), ids.end())); + else + return inversion_tactic(elab, H, to_list(ids.begin(), ids.end())); }); } void finalize_inversion_tactic() {} diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out index b5e731f474..9703f27271 100644 --- a/tests/lean/errors.lean.expected.out +++ b/tests/lean/errors.lean.expected.out @@ -1,6 +1,6 @@ errors.lean:4:0: error: unknown identifier 'a' tst1 : nat → nat → nat -errors.lean:12:16: error: invalid 'begin-end' expression, ',' expected +errors.lean:12:8: error: unknown identifier 'add' errors.lean:22:12: error: unknown identifier 'b' tst3 : A → A → A foo.tst1 : ℕ → ℕ → ℕ diff --git a/tests/lean/run/645a.lean b/tests/lean/run/645a.lean new file mode 100644 index 0000000000..d218fbd1ad --- /dev/null +++ b/tests/lean/run/645a.lean @@ -0,0 +1,22 @@ +open bool + +definition to_pred {A : Type} (p : A → bool) : A → Prop := +λ a, p a = tt + +definition to_pred_dec₁ [instance] {A : Type} (p : A → bool) + : decidable_pred (to_pred p) := +begin + intro a, unfold to_pred, + induction p a, + right, contradiction, + left, reflexivity +end + +definition to_pred_dec₂ [instance] {A : Type} (p : A → bool) + : decidable_pred (to_pred p) := +begin + intro a, unfold to_pred, + cases p a, + right, contradiction, + left, reflexivity +end