From 15e52b06dfd710d14749aa8e1608bcc25868be37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 20:18:24 -0700 Subject: [PATCH] fix(library/tactic/constructor_tactic): bug in constructor tactic see example (constr_tac2.lean) in comment at issue #500 --- src/library/tactic/apply_tactic.cpp | 8 +++-- src/library/tactic/apply_tactic.h | 1 + src/library/tactic/constructor_tactic.cpp | 42 +++++++++-------------- tests/lean/run/constr_tac2.lean | 7 ++++ 4 files changed, 31 insertions(+), 27 deletions(-) create mode 100644 tests/lean/run/constr_tac2.lean diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 2f41e4aac7..a13465e05e 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -67,8 +67,6 @@ static void remove_redundant_metas(buffer & metas) { enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals, AddAllSubgoals }; - - static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e, buffer & cs, bool add_meta, subgoals_action_kind subgoals_action) { @@ -178,6 +176,12 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action); } +proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) { + buffer tmp_cs; + cs.linearize(tmp_cs); + return apply_tactic_core(env, ios, s, e, tmp_cs, true, AddAllSubgoals); +} + tactic eassumption_tactic() { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 6da148b6e9..41815b7b14 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/lua.h" #include "library/tactic/elaborate.h" namespace lean { +proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs); tactic apply_tactic(elaborate_fn const & fn, expr const & e); tactic fapply_tactic(elaborate_fn const & fn, expr const & e); tactic eassumption_tactic(); diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp index 0f78b92f54..4c59a2c357 100644 --- a/src/library/tactic/constructor_tactic.cpp +++ b/src/library/tactic/constructor_tactic.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/reducible.h" #include "library/tactic/expr_to_tactic.h" +#include "library/tactic/apply_tactic.h" namespace lean { /** @@ -25,78 +26,69 @@ tactic constructor_tactic(elaborate_fn const & elab, unsigned _i, optional(); + return proof_state_seq(); } if (_i == 0) { throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero"); - return optional(); + return proof_state_seq(); } + constraint_seq cs; unsigned i = _i - 1; name_generator ngen = s.get_ngen(); auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); goal const & g = head(gs); - expr t = tc->whnf(g.get_type()).first; + expr t = tc->whnf(g.get_type(), cs); buffer I_args; expr I = get_app_args(t, I_args); if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) { throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, goal is not an inductive datatype"); - return none_proof_state(); + return proof_state_seq(); } buffer c_names; get_intro_rule_names(env, const_name(I), c_names); if (num_constructors && c_names.size() != *num_constructors) { throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " << "but it does not have " << *num_constructors << " constructor(s)"); - return none_proof_state(); + return proof_state_seq(); } if (i >= c_names.size()) { throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " << "but it has only " << c_names.size() << " constructor(s)"); - return none_proof_state(); + return proof_state_seq(); } expr C = mk_constant(c_names[i], const_levels(I)); unsigned num_params = *inductive::get_num_params(env, const_name(I)); if (I_args.size() < num_params) - return none_proof_state(); + return proof_state_seq(); proof_state new_s(s, ngen); C = mk_app(C, num_params, I_args.data()); - expr C_type = tc->whnf(tc->infer(C).first).first; + expr C_type = tc->whnf(tc->infer(C, cs), cs); bool report_unassigned = true; bool enforce_type = true; for (expr const & arg : given_args) { if (!is_pi(C_type)) { throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, " << "too many arguments have been provided"); - return none_proof_state(); + return proof_state_seq(); } try { if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)), report_unassigned, enforce_type)) { C = mk_app(C, *new_arg); - C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg)).first; + C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs); } else { - return none_proof_state(); + return proof_state_seq(); } } catch (exception &) { if (new_s.report_failure()) throw; - return none_proof_state(); + return proof_state_seq(); } } - buffer new_goals; - while (is_pi(C_type)) { - expr new_type = binding_domain(C_type); - expr new_meta = g.mk_meta(tc->mk_fresh_name(), new_type); - goal new_goal(new_meta, new_type); - new_goals.push_back(new_goal); - C = mk_app(C, new_meta); - C_type = tc->whnf(instantiate(binding_body(C_type), new_meta)).first; - } - substitution new_subst = new_s.get_subst(); - assign(new_subst, g, C); - return some_proof_state(proof_state(new_s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), new_subst)); + + return apply_tactic_core(env, ios, new_s, C, cs); }; - return tactic01(fn); + return tactic(fn); } void initialize_constructor_tactic() { diff --git a/tests/lean/run/constr_tac2.lean b/tests/lean/run/constr_tac2.lean new file mode 100644 index 0000000000..20beb9118c --- /dev/null +++ b/tests/lean/run/constr_tac2.lean @@ -0,0 +1,7 @@ +open nat + +example (n m : ℕ) (H : n < m) : n < succ m := +begin + constructor 2, + exact H +end