From abbd054b51ab6556fc9a84551acee2eb478fbb1f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Jul 2014 12:59:48 -0700 Subject: [PATCH] feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic Signed-off-by: Leonardo de Moura --- library/standard/tactic.lean | 49 +++++----- src/library/tactic/apply_tactic.cpp | 136 +++++++++++++++++++------- src/library/tactic/apply_tactic.h | 1 + src/library/tactic/expr_to_tactic.cpp | 1 + tests/lean/run/tactic20.lean | 12 +++ tests/lean/run/tactic21.lean | 17 ++++ 6 files changed, 156 insertions(+), 60 deletions(-) create mode 100644 tests/lean/run/tactic20.lean create mode 100644 tests/lean/run/tactic21.lean diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean index bf753b59a..9ebd4d3ca 100644 --- a/library/standard/tactic.lean +++ b/library/standard/tactic.lean @@ -17,33 +17,34 @@ inductive tactic : Type := -- uses them when converting Lean expressions into actual tactic objects. -- The bultin 'by' construct triggers the process of converting a -- a term of type 'tactic' into a tactic that sythesizes a term -definition and_then (t1 t2 : tactic) : tactic := builtin_tactic -definition or_else (t1 t2 : tactic) : tactic := builtin_tactic -definition append (t1 t2 : tactic) : tactic := builtin_tactic -definition interleave (t1 t2 : tactic) : tactic := builtin_tactic -definition par (t1 t2 : tactic) : tactic := builtin_tactic -definition repeat (t : tactic) : tactic := builtin_tactic -definition at_most (t : tactic) (k : num) : tactic := builtin_tactic -definition discard (t : tactic) (k : num) : tactic := builtin_tactic -definition focus_at (t : tactic) (i : num) : tactic := builtin_tactic -definition try_for (t : tactic) (ms : num) : tactic := builtin_tactic -definition now : tactic := builtin_tactic -definition assumption : tactic := builtin_tactic -definition state : tactic := builtin_tactic -definition fail : tactic := builtin_tactic -definition id : tactic := builtin_tactic -definition beta : tactic := builtin_tactic -definition apply {B : Type} (b : B) : tactic := builtin_tactic -definition unfold {B : Type} (b : B) : tactic := builtin_tactic -definition exact {B : Type} (b : B) : tactic := builtin_tactic -definition trace (s : string) : tactic := builtin_tactic +definition and_then (t1 t2 : tactic) : tactic := builtin_tactic +definition or_else (t1 t2 : tactic) : tactic := builtin_tactic +definition append (t1 t2 : tactic) : tactic := builtin_tactic +definition interleave (t1 t2 : tactic) : tactic := builtin_tactic +definition par (t1 t2 : tactic) : tactic := builtin_tactic +definition repeat (t : tactic) : tactic := builtin_tactic +definition at_most (t : tactic) (k : num) : tactic := builtin_tactic +definition discard (t : tactic) (k : num) : tactic := builtin_tactic +definition focus_at (t : tactic) (i : num) : tactic := builtin_tactic +definition try_for (t : tactic) (ms : num) : tactic := builtin_tactic +definition now : tactic := builtin_tactic +definition assumption : tactic := builtin_tactic +definition eassumption : tactic := builtin_tactic +definition state : tactic := builtin_tactic +definition fail : tactic := builtin_tactic +definition id : tactic := builtin_tactic +definition beta : tactic := builtin_tactic +definition apply {B : Type} (b : B) : tactic := builtin_tactic +definition unfold {B : Type} (b : B) : tactic := builtin_tactic +definition exact {B : Type} (b : B) : tactic := builtin_tactic +definition trace (s : string) : tactic := builtin_tactic infixl `;`:200 := and_then infixl `|`:100 := or_else notation `!` t:max := repeat t notation `⟦` t `⟧` := apply t -definition try (t : tactic) : tactic := t | id +definition try (t : tactic) : tactic := t | id notation `?` t:max := try t -definition repeat1 (t : tactic) : tactic := t ; !t -definition focus (t : tactic) : tactic := focus_at t 0 -definition determ (t : tactic) : tactic := at_most t 1 +definition repeat1 (t : tactic) : tactic := t ; !t +definition focus (t : tactic) : tactic := focus_at t 0 +definition determ (t : tactic) : tactic := at_most t 1 end diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index ddc5d2ca6..d1d430db3 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/kernel_bindings.h" #include "library/unifier.h" +#include "library/occurs.h" #include "library/tactic/apply_tactic.h" namespace lean { @@ -60,51 +61,114 @@ void collect_simple_meta(expr const & e, buffer & metas) { }); } -tactic apply_tactic(expr const & _e) { +/** + \brief Given a sequence metas: (?m_1 ...) (?m_2 ... ) ... (?m_k ...), + we say ?m_i is "redundant" if it occurs in the type of some ?m_j. + This procedure removes from metas any redundant element. +*/ +static void remove_redundant_metas(buffer & metas) { + buffer mvars; + for (expr const & m : metas) + mvars.push_back(get_app_fn(m)); + unsigned k = 0; + for (unsigned i = 0; i < metas.size(); i++) { + bool found = false; + for (unsigned j = 0; j < metas.size(); j++) { + if (j != i) { + if (occurs(mvars[i], mlocal_type(mvars[j]))) { + found = true; + break; + } + } + } + if (!found) { + metas[k] = metas[i]; + k++; + } + } + metas.shrink(k); +} + +proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e, + bool add_meta, bool add_subgoals) { + goals const & gs = s.get_goals(); + if (empty(gs)) + return proof_state_seq(); + name_generator ngen = s.get_ngen(); + type_checker tc(env, ngen.mk_child()); + goal g = head(gs); + goals tail_gs = tail(gs); + expr t = g.get_type(); + expr e = _e; + expr e_t = tc.infer(e); + buffer metas; + collect_simple_meta(e, metas); + if (add_meta) { + unsigned num_t = get_expect_num_args(tc, t); + unsigned num_e_t = get_expect_num_args(tc, e_t); + if (num_t > num_e_t) + return proof_state_seq(); // no hope to unify then + for (unsigned i = 0; i < num_e_t - num_t; i++) { + e_t = tc.whnf(e_t); + expr meta = g.mk_meta(ngen.next(), binding_domain(e_t)); + e = mk_app(e, meta); + e_t = instantiate(binding_body(e_t), meta); + metas.push_back(meta); + } + } + list meta_lst = to_list(metas.begin(), metas.end()); + lazy_list substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options()); + return map2(substs, [=](substitution const & subst) -> proof_state { + name_generator new_ngen(ngen); + type_checker tc(env, new_ngen.mk_child()); + expr new_e = subst.instantiate(e); + expr new_p = g.abstract(new_e); + check_has_no_local(new_p, _e, "apply"); + substitution new_subst = subst.assign(g.get_name(), new_p); + goals new_gs = tail_gs; + if (add_subgoals) { + buffer metas; + for (auto m : meta_lst) { + if (!new_subst.is_assigned(get_app_fn(m))) + metas.push_back(m); + } + remove_redundant_metas(metas); + unsigned i = metas.size(); + while (i > 0) { + --i; + new_gs = cons(goal(metas[i], subst.instantiate(tc.infer(metas[i]))), new_gs); + } + } + return proof_state(new_gs, new_subst, new_ngen); + }); +} + +tactic apply_tactic(expr const & e) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + return apply_tactic_core(env, ios, s, e, true, true); + }); +} + +tactic eassumption_tactic() { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) return proof_state_seq(); - name_generator ngen = s.get_ngen(); - type_checker tc(env, ngen.mk_child()); - goal g = head(gs); - goals tail_gs = tail(gs); - expr t = g.get_type(); - expr e = _e; - expr e_t = tc.infer(e); - unsigned num_t = get_expect_num_args(tc, t); - unsigned num_e_t = get_expect_num_args(tc, e_t); - if (num_t > num_e_t) - return proof_state_seq(); // no hope to unify then - for (unsigned i = 0; i < num_e_t - num_t; i++) { - e_t = tc.whnf(e_t); - expr meta = g.mk_meta(ngen.next(), binding_domain(e_t)); - e = mk_app(e, meta); - e_t = instantiate(binding_body(e_t), meta); + proof_state_seq r; + goal g = head(gs); + buffer hs; + get_app_args(g.get_meta(), hs); + for (expr const & h : hs) { + r = append(r, apply_tactic_core(env, ios, s, h, false, false)); } - lazy_list substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options()); - return map2(substs, [=](substitution const & subst) -> proof_state { - name_generator new_ngen(ngen); - type_checker tc(env, new_ngen.mk_child()); - expr new_e = subst.instantiate(e); - expr new_p = g.abstract(new_e); - check_has_no_local(new_p, _e, "apply"); - substitution new_subst = subst.assign(g.get_name(), new_p); - buffer metas; - collect_simple_meta(new_e, metas); - goals new_gs = tail_gs; - unsigned i = metas.size(); - while (i > 0) { - --i; - new_gs = cons(goal(metas[i], subst.instantiate(tc.infer(metas[i]))), new_gs); - } - return proof_state(new_gs, new_subst, new_ngen); - }); + return r; }); } int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); } +int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); } void open_apply_tactic(lua_State * L) { - SET_GLOBAL_FUN(mk_apply_tactic, "apply_tac"); + SET_GLOBAL_FUN(mk_apply_tactic, "apply_tac"); + SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac"); } } diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index a9abc95e6..b343ce152 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -9,5 +9,6 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { tactic apply_tactic(expr const & e); +tactic eassumption_tactic(); void open_apply_tactic(lua_State * L); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 692055fef..8828d0cd4 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -145,6 +145,7 @@ register_unary_num_tac::register_unary_num_tac(name const & n, std::function