From abf61be8f69c53c9456f9529bdbcd71ee62bfba4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jan 2014 00:57:04 -0800 Subject: [PATCH] chore(library/tactic): remove imp_tac, it is not needed anymore Signed-off-by: Leonardo de Moura --- src/library/tactic/boolean_tactics.cpp | 46 -------------------------- tests/lean/tactic1.lean | 2 +- tests/lean/tactic3.lean | 2 +- tests/lean/tactic4.lean | 2 +- tests/lean/tactic5.lean | 2 +- 5 files changed, 4 insertions(+), 50 deletions(-) diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp index 6ce632848..077f1ae1d 100644 --- a/src/library/tactic/boolean_tactics.cpp +++ b/src/library/tactic/boolean_tactics.cpp @@ -58,46 +58,6 @@ tactic conj_tactic(bool all) { }); } -tactic imp_tactic(name const & H_name, bool all) { - return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { - expr impfn = mk_implies_fn(); - bool found = false; - list> proof_info; - goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> optional { - expr const & c = g.get_conclusion(); - if ((all || !found) && is_implies(c)) { - expr new_h = arg(c, 1); - expr new_c = arg(c, 2); - found = true; - name new_h_name = g.mk_unique_hypothesis_name(H_name); - proof_info.emplace_front(g_name, new_h_name, c); - return optional(goal(add_hypothesis(new_h_name, new_h, g.get_hypotheses()), new_c)); - } else { - return optional(g); - } - }); - if (found) { - proof_builder pr_builder = s.get_proof_builder(); - proof_builder new_pr_builder = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { - proof_map new_m(m); - for (auto const & info : proof_info) { - name const & goal_name = std::get<0>(info); - name const & hyp_name = std::get<1>(info); // new hypothesis name - expr const & old_c = std::get<2>(info); // old conclusion of the form H => C - expr const & h = arg(old_c, 1); // new hypothesis: antencedent of the old conclusion - expr const & c = arg(old_c, 2); // new conclusion: consequent of the old conclusion - expr const & c_pr = find(m, goal_name); // proof for the new conclusion - new_m.insert(goal_name, Discharge(h, c, Fun(hyp_name, h, c_pr))); - } - return pr_builder(new_m, a); - }); - return some_proof_state(s, new_goals, new_pr_builder); - } else { - return none_proof_state(); - } - }); -} - tactic conj_hyp_tactic(bool all) { return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { bool found = false; @@ -357,11 +317,6 @@ static int mk_conj_tactic(lua_State * L) { return push_tactic(L, conj_tactic(nargs == 0 ? true : lua_toboolean(L, 1))); } -static int mk_imp_tactic(lua_State * L) { - int nargs = lua_gettop(L); - return push_tactic(L, imp_tactic(nargs >= 1 ? to_name_ext(L, 1) : name("H"), nargs == 2 ? lua_toboolean(L, 2) : true)); -} - static int mk_conj_hyp_tactic(lua_State * L) { int nargs = lua_gettop(L); return push_tactic(L, conj_hyp_tactic(nargs == 0 ? true : lua_toboolean(L, 1))); @@ -393,7 +348,6 @@ static int mk_absurd_tactic(lua_State * L) { void open_boolean_tactics(lua_State * L) { SET_GLOBAL_FUN(mk_conj_tactic, "conj_tac"); - SET_GLOBAL_FUN(mk_imp_tactic, "imp_tac"); SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tac"); SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tac"); SET_GLOBAL_FUN(mk_disj_tactic, "disj_tac"); diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean index f556e672e..6fc22372a 100644 --- a/tests/lean/tactic1.lean +++ b/tests/lean/tactic1.lean @@ -3,7 +3,7 @@ variables p q r : Bool (* local env = get_environment() local conjecture = parse_lean('p → q → p && q') - local tac = Repeat(conj_tac() ^ imp_tac() ^ assumption_tac()) + local tac = Repeat(conj_tac() ^ assumption_tac()) local proof = tac:solve(env, context(), conjecture) env:add_theorem("T1", conjecture, proof) *) diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean index 94afc0f0d..713fcd092 100644 --- a/tests/lean/tactic3.lean +++ b/tests/lean/tactic3.lean @@ -2,7 +2,7 @@ variables p q r : Bool theorem T1 : p → p /\ q → r → q /\ r /\ p := _. - (* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *) + (* Repeat(OrElse(conj_tac(), conj_hyp_tac(), assumption_tac())) *) done -- Display proof term generated by previous tactic diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean index 7c7cd23d0..1962296fd 100644 --- a/tests/lean/tactic4.lean +++ b/tests/lean/tactic4.lean @@ -1,5 +1,5 @@ (* -simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac() +simple_tac = Repeat(conj_tac()) .. assumption_tac() *) theorem T4 (a b : Bool) : a → b → a /\ b := _. diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean index 5567fdd00..b5c70ff24 100644 --- a/tests/lean/tactic5.lean +++ b/tests/lean/tactic5.lean @@ -1,5 +1,5 @@ (* -simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac() +simple_tac = Repeat(conj_tac()) .. assumption_tac() *) theorem T4 (a b : Bool) : a → b → a /\ b /\ a := _.