From 1490bdad4980e59dfa35369de691957636bb2b1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Mar 2015 16:48:48 -0800 Subject: [PATCH] feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration --- hott/init/tactic.hlean | 2 ++ library/init/tactic.lean | 2 ++ src/frontends/lean/builtin_exprs.cpp | 10 +++++++--- src/frontends/lean/elaborator.cpp | 14 ++++++++++---- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/info_tactic.cpp | 2 +- src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/elaborate.cpp | 16 +++++++++++----- src/library/tactic/elaborate.h | 11 +++++++---- src/library/tactic/exact_tactic.cpp | 18 ++++++++++++++---- src/library/tactic/exact_tactic.h | 2 +- src/library/tactic/rewrite_tactic.cpp | 10 +++++----- tests/lean/run/match_tac2.lean | 12 ++++++++++++ tests/lean/run/match_tac3.lean | 13 +++++++++++++ 17 files changed, 93 insertions(+), 29 deletions(-) create mode 100644 tests/lean/run/match_tac2.lean create mode 100644 tests/lean/run/match_tac3.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 3313e5af2..7fd2d9c91 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -62,6 +62,8 @@ opaque definition clear (e : expr) : tactic := builtin opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin +-- rexact is similar to exact, but the goal type is enforced during elaboration +opaque definition sexact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin inductive expr_list : Type := diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 19e70190b..e30ed5fc5 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -61,6 +61,8 @@ opaque definition clear (e : expr) : tactic := builtin opaque definition revert (e : expr) : tactic := builtin opaque definition unfold (e : expr) : tactic := builtin opaque definition exact (e : expr) : tactic := builtin +-- rexact is similar to exact, but the goal type is enforced during elaboration +opaque definition sexact (e : expr) : tactic := builtin opaque definition trace (s : string) : tactic := builtin inductive expr_list : Type := diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 0b67083d0..7e3e71db9 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -213,13 +213,17 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & } else { throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos()); } - } else if (p.curr_is_token(get_show_tk()) || p.curr_is_token(get_match_tk()) || - p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) || - p.curr_is_token(get_fun_tk())) { + } else if (p.curr_is_token(get_show_tk())) { auto pos = p.pos(); expr t = p.parse_expr(); t = p.mk_app(get_exact_tac_fn(), t, pos); add_tac(t, pos); + } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) || + p.curr_is_token(get_take_tk()) || p.curr_is_token(get_fun_tk())) { + auto pos = p.pos(); + expr t = p.parse_expr(); + t = p.mk_app(get_sexact_tac_fn(), t, pos); + add_tac(t, pos); } else { auto pos = p.pos(); expr t = p.parse_tactic(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 29d81fa30..fc22b1928 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1464,12 +1464,14 @@ optional elaborator::get_pre_tactic_for(expr const & mvar) { optional elaborator::pre_tactic_to_tactic(expr const & pre_tac) { try { bool relax = m_relax_main_opaque; - auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, bool report_unassigned) { + auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional const & expected_type, + bool report_unassigned) { elaborator aux_elaborator(m_ctx, ngen); // Disable tactic hints when processing expressions nested in tactics. // We must do it otherwise, it is easy to make the system loop. bool use_tactic_hints = false; - return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints, report_unassigned); + return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e, + relax, use_tactic_hints, report_unassigned); }; return optional(expr_to_tactic(env(), fn, pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { @@ -1870,14 +1872,18 @@ static expr translate(environment const & env, list const & ctx, expr cons } /** \brief Elaborate expression \c e in context \c ctx. */ -pair elaborator::elaborate_nested(list const & ctx, expr const & n, - bool relax, bool use_tactic_hints, bool report_unassigned) { +pair elaborator::elaborate_nested(list const & ctx, optional const & expected_type, + expr const & n, bool relax, bool use_tactic_hints, + bool report_unassigned) { if (infom()) { if (auto ps = get_info_tactic_proof_state()) { save_proof_state_info(*ps, n); } } expr e = translate(env(), ctx, n); + if (expected_type) + e = copy_tag(e, mk_typed_expr(mk_as_is(*expected_type), e)); + m_context.set_ctx(ctx); m_context.set_ctx(ctx); m_full_context.set_ctx(ctx); flet set_relax(m_relax_main_opaque, relax); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 4437f434d..4c9653d07 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -157,7 +157,7 @@ class elaborator : public coercion_info_manager { void check_sort_assignments(substitution const & s); expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params); std::tuple apply(substitution & s, expr const & e); - pair elaborate_nested(list const & g, expr const & e, + pair elaborate_nested(list const & ctx, optional const & expected_type, expr const & e, bool relax, bool use_tactic_hints, bool report_unassigned); expr const & get_equation_fn(expr const & eq) const; diff --git a/src/frontends/lean/info_tactic.cpp b/src/frontends/lean/info_tactic.cpp index 28b76e844..fd5bae7d5 100644 --- a/src/frontends/lean/info_tactic.cpp +++ b/src/frontends/lean/info_tactic.cpp @@ -36,7 +36,7 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) { // create dummy variable just to communicate position to the elaborator expr dummy = mk_sort(mk_level_zero(), e.get_tag()); scoped_info_tactic_proof_state scope(ps); - fn(goal(), name_generator("dummy"), dummy, false); + fn(goal(), name_generator("dummy"), dummy, none_expr(), false); return ps; }); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d1e4395ca..f177ae7fa 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -94,6 +94,7 @@ name const * g_tactic_now = nullptr; name const * g_tactic_opt_expr_list = nullptr; name const * g_tactic_or_else = nullptr; name const * g_tactic_par = nullptr; +name const * g_tactic_sexact = nullptr; name const * g_tactic_state = nullptr; name const * g_tactic_rename = nullptr; name const * g_tactic_repeat = nullptr; @@ -204,6 +205,7 @@ void initialize_constants() { g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; g_tactic_or_else = new name{"tactic", "or_else"}; g_tactic_par = new name{"tactic", "par"}; + g_tactic_sexact = new name{"tactic", "sexact"}; g_tactic_state = new name{"tactic", "state"}; g_tactic_rename = new name{"tactic", "rename"}; g_tactic_repeat = new name{"tactic", "repeat"}; @@ -315,6 +317,7 @@ void finalize_constants() { delete g_tactic_opt_expr_list; delete g_tactic_or_else; delete g_tactic_par; + delete g_tactic_sexact; delete g_tactic_state; delete g_tactic_rename; delete g_tactic_repeat; @@ -425,6 +428,7 @@ name const & get_tactic_now_name() { return *g_tactic_now; } name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } name const & get_tactic_or_else_name() { return *g_tactic_or_else; } name const & get_tactic_par_name() { return *g_tactic_par; } +name const & get_tactic_sexact_name() { return *g_tactic_sexact; } name const & get_tactic_state_name() { return *g_tactic_state; } name const & get_tactic_rename_name() { return *g_tactic_rename; } name const & get_tactic_repeat_name() { return *g_tactic_repeat; } diff --git a/src/library/constants.h b/src/library/constants.h index 6ec469c09..2e31f5ddc 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -96,6 +96,7 @@ name const & get_tactic_now_name(); name const & get_tactic_opt_expr_list_name(); name const & get_tactic_or_else_name(); name const & get_tactic_par_name(); +name const & get_tactic_sexact_name(); name const & get_tactic_state_name(); name const & get_tactic_rename_name(); name const & get_tactic_repeat_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 348406140..c60daae77 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -89,6 +89,7 @@ tactic.now tactic.opt_expr_list tactic.or_else tactic.par +tactic.sexact tactic.state tactic.rename tactic.repeat diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 8db063b53..5a92c1c6f 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -210,7 +210,7 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, subgoals_act name_generator ngen = s.get_ngen(); expr new_e; buffer cs; - auto ecs = elab(g, ngen.mk_child(), e, false); + auto ecs = elab(g, ngen.mk_child(), e, none_expr(), false); new_e = ecs.first; to_buffer(ecs.second, cs); to_buffer(s.get_postponed(), cs); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index b5d1cd113..212bd373f 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -31,18 +31,24 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat } optional elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab, - proof_state & s, expr const & e, optional const & expected_type, - bool report_unassigned) { + proof_state & s, expr const & e, optional const & _expected_type, + bool report_unassigned, bool enforce_type_during_elaboration) { name_generator ngen = s.get_ngen(); substitution subst = s.get_subst(); goals const & gs = s.get_goals(); + optional expected_type = _expected_type; + if (expected_type) + expected_type = subst.instantiate(*expected_type); if (empty(gs)) return none_expr(); - auto ecs = elab(head(gs), ngen.mk_child(), e, report_unassigned); + optional elab_expected_type; + if (enforce_type_during_elaboration) + elab_expected_type = expected_type; + auto ecs = elab(head(gs), ngen.mk_child(), e, elab_expected_type, report_unassigned); expr new_e = ecs.first; buffer cs; to_buffer(ecs.second, cs); - if (cs.empty() && !expected_type) { + if (cs.empty() && (!expected_type || enforce_type_during_elaboration)) { // easy case: no constraints to be solved s = proof_state(s, ngen); return some_expr(new_e); @@ -51,7 +57,7 @@ optional elaborate_with_respect_to(environment const & env, io_state const if (expected_type) { auto tc = mk_type_checker(env, ngen.mk_child()); auto e_t_cs = tc->infer(new_e); - expr t = subst.instantiate(*expected_type); + expr t = *expected_type; e_t_cs.second.linearize(cs); auto d_cs = tc->is_def_eq(e_t_cs.first, t); if (!d_cs.first) { diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index cb49bb808..9de211678 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -16,9 +16,11 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat 1- goal that will provide the context where the expression will be elaborated 2- name generator 3- expression to be elaborated - 4- a flag indicating whether the elaborator should report unassigned/unsolved placeholders + 4- expected type + 5- a flag indicating whether the elaborator should report unassigned/unsolved placeholders */ -typedef std::function(goal const &, name_generator const &, expr const &, bool)> elaborate_fn; +typedef std::function(goal const &, name_generator const &, expr const &, + optional const &, bool)> elaborate_fn; /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed with respect to (local context of) the first goal in \c s. The constraints generated during elaboration @@ -31,6 +33,7 @@ typedef std::function(goal const &, name_generator const is not modified. */ optional elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab, - proof_state & s, expr const & e, optional const & expected_type = optional(), - bool report_unassigned = false); + proof_state & s, expr const & e, + optional const & expected_type = optional(), + bool report_unassigned = false, bool enforce_type_during_elaboration = false); } diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 0760b526a..4e80d43b6 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -tactic exact_tactic(elaborate_fn const & elab, expr const & e) { +tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration) { return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { proof_state new_s = s; goals const & gs = new_s.get_goals(); @@ -21,7 +21,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) { } expr t = head(gs).get_type(); bool report_unassigned = false; - if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) { + if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), + report_unassigned, enforce_type_during_elaboration)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs); expr new_p = g.abstract(*new_e); @@ -35,14 +36,23 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) { } static expr * g_exact_tac_fn = nullptr; -expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } +static expr * g_sexact_tac_fn = nullptr; +expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } +expr const & get_sexact_tac_fn() { return *g_sexact_tac_fn; } void initialize_exact_tactic() { name const & exact_tac_name = get_tactic_exact_name(); + name const & sexact_tac_name = get_tactic_sexact_name(); g_exact_tac_fn = new expr(Const(exact_tac_name)); + g_sexact_tac_fn = new expr(Const(sexact_tac_name)); register_tac(exact_tac_name, [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); - return exact_tactic(fn, get_tactic_expr_expr(app_arg(e))); + return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false); + }); + register_tac(sexact_tac_name, + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); + return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true); }); } void finalize_exact_tactic() { diff --git a/src/library/tactic/exact_tactic.h b/src/library/tactic/exact_tactic.h index c229033a8..6c87c4e8b 100644 --- a/src/library/tactic/exact_tactic.h +++ b/src/library/tactic/exact_tactic.h @@ -9,8 +9,8 @@ Author: Leonardo de Moura namespace lean { expr const & get_exact_tac_fn(); +expr const & get_sexact_tac_fn(); /** \brief Solve first goal iff it is definitionally equal to type of \c e */ -tactic exact_tactic(expr const & e); void initialize_exact_tactic(); void finalize_exact_tactic(); } diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 3f724214f..ecb517d39 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -579,7 +579,7 @@ class rewrite_fn { } optional fold(expr const & type, expr const & e, occurrence const & occ) { - auto ecs = m_elab(m_g, m_ngen.mk_child(), e, false); + auto ecs = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false); expr new_e = ecs.first; if (ecs.second) return none_expr(); // contain constraints... @@ -651,7 +651,7 @@ class rewrite_fn { } optional unify_with(expr const & t, expr const & e) { - auto ecs = m_elab(m_g, m_ngen.mk_child(), e, false); + auto ecs = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), false); expr new_e = ecs.first; buffer cs; to_buffer(ecs.second, cs); @@ -832,7 +832,7 @@ class rewrite_fn { unify_result unify_target(expr const & t, expr const & orig_elem, bool is_goal) { try { expr rule = get_rewrite_rule(orig_elem); - auto rcs = m_elab(m_g, m_ngen.mk_child(), rule, false); + auto rcs = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false); rule = rcs.first; buffer cs; to_buffer(rcs.second, cs); @@ -1096,11 +1096,11 @@ class rewrite_fn { expr rule = get_rewrite_rule(elem); expr new_elem; if (has_rewrite_pattern(elem)) { - expr pattern = m_elab(m_g, m_ngen.mk_child(), get_rewrite_pattern(elem), false).first; + expr pattern = m_elab(m_g, m_ngen.mk_child(), get_rewrite_pattern(elem), none_expr(), false).first; expr new_args[2] = { rule, pattern }; new_elem = mk_macro(macro_def(elem), 2, new_args); } else { - rule = m_elab(m_g, m_ngen.mk_child(), rule, false).first; + rule = m_elab(m_g, m_ngen.mk_child(), rule, none_expr(), false).first; new_elem = mk_macro(macro_def(elem), 1, &rule); } return process_rewrite_step(new_elem, elem); diff --git a/tests/lean/run/match_tac2.lean b/tests/lean/run/match_tac2.lean new file mode 100644 index 000000000..06d2b3f9b --- /dev/null +++ b/tests/lean/run/match_tac2.lean @@ -0,0 +1,12 @@ +example (a b c : Prop) : a ∧ b ↔ b ∧ a := +begin + apply iff.intro, + {intro H, + match H with + | and.intro H₁ H₂ := by apply and.intro; assumption + end}, + {intro H, + match H with + | and.intro H₁ H₂ := by apply and.intro; assumption + end}, +end diff --git a/tests/lean/run/match_tac3.lean b/tests/lean/run/match_tac3.lean new file mode 100644 index 000000000..38844920d --- /dev/null +++ b/tests/lean/run/match_tac3.lean @@ -0,0 +1,13 @@ +import data.nat +open nat + +theorem tst (a b : nat) (H : a = 0) : a + b = b := +begin + revert H, + match a with + | zero := λ H, by rewrite zero_add + | (n+1) := λ H, nat.no_confusion H + end +end + +print definition tst