From 9dcfa03dd2474cb7a9b26087123ab5adfdff868a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Nov 2013 21:00:38 -0800 Subject: [PATCH] feat(library/tactic): add conj_hyp_tactic Signed-off-by: Leonardo de Moura --- src/library/tactic/boolean.cpp | 60 +++++++++++++++++++++++++++++ src/library/tactic/boolean.h | 1 + src/library/tactic/goal.cpp | 2 +- src/tests/library/tactic/tactic.cpp | 9 ++++- 4 files changed, 69 insertions(+), 3 deletions(-) diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 4b35ae65d..7be21c4e4 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "kernel/builtin.h" #include "kernel/abstract.h" +#include "kernel/occurs.h" #include "library/basic_thms.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" @@ -95,4 +96,63 @@ tactic imp_tactic(name const & H_name, bool all) { } }); } +tactic conj_hyp_tactic(bool all) { + return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + expr andfn = mk_and_fn(); + bool found = false; + list>>> proof_info; // goal name, list(hypothesis name, hypothesis prop) + goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { + if (all || !found) { + buffer> new_hyp_buf; + list> proof_info_data; + for (auto const & p : g.get_hypotheses()) { + name const & H_name = p.first; + expr const & H_prop = p.second; + if ((all || !found) && is_app_of(H_prop, andfn)) { + found = true; + proof_info_data.emplace_front(H_name, H_prop); + new_hyp_buf.emplace_back(name(H_name, 1), arg(H_prop, 1)); + new_hyp_buf.emplace_back(name(H_name, 2), arg(H_prop, 2)); + } else { + new_hyp_buf.push_back(p); + } + } + if (proof_info_data) { + proof_info.emplace_front(ng, proof_info_data); + return goal(to_list(new_hyp_buf.begin(), new_hyp_buf.end()), g.get_conclusion()); + } else { + return g; + } + } else { + return g; + } + }); + if (found) { + proof_builder p = s.get_proof_builder(); + proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_map new_m(m); + for (auto const & info : proof_info) { + name const & goal_name = info.first; + auto const & expanded_hyp = info.second; + expr pr = find(m, goal_name); // proof for the new conclusion + for (auto const & H_name_prop : expanded_hyp) { + name const & H_name = H_name_prop.first; + expr const & H_prop = H_name_prop.second; + expr const & H_1 = mk_constant(name(H_name, 1), arg(H_prop, 1)); + expr const & H_2 = mk_constant(name(H_name, 2), arg(H_prop, 2)); + if (occurs(H_1, pr)) + pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); + if (occurs(H_2, pr)) + pr = Let(H_2, Conjunct2(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); + } + new_m.insert(goal_name, pr); + } + return p(new_m, env, a); + }); + return some(proof_state(s, new_goals, new_p)); + } else { + return optional(); + } + }); +} } diff --git a/src/library/tactic/boolean.h b/src/library/tactic/boolean.h index 1e1d5c3cd..1c3daf366 100644 --- a/src/library/tactic/boolean.h +++ b/src/library/tactic/boolean.h @@ -8,5 +8,6 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { tactic conj_tactic(bool all = true); +tactic conj_hyp_tactic(bool all = true); tactic imp_tactic(name const & H_name = name("H"), bool all = true); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 40371759e..078aa64dc 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -47,7 +47,7 @@ name goal::mk_unique_hypothesis_name(name const & suggestion) const { while (true) { bool ok = true; for (auto const & p : m_hypotheses) { - if (n == p.first) { + if (is_prefix_of(n, p.first)) { ok = false; break; } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 78d6d6c24..99223204f 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/interrupt.h" #include "kernel/builtin.h" +#include "kernel/kernel_exception.h" #include "library/all/all.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" @@ -121,8 +122,12 @@ static void tst2() { import_all(env); env.add_var("p", Bool); env.add_var("q", Bool); + env.add_var("r", Bool); + env.add_var("s", Bool); expr p = Const("p"); expr q = Const("q"); + expr r = Const("r"); + expr s = Const("s"); context ctx; ctx = extend(ctx, "H1", p); ctx = extend(ctx, "H2", q); @@ -130,9 +135,9 @@ static void tst2() { << "\n"; std::cout << "-------------\n"; // Theorem to be proved - expr F = Implies(p, Implies(q, And(And(p, q), And(p, p)))); + expr F = Implies(And(p, And(r, s)), Implies(q, And(And(p, q), And(r, p)))); // Tactic - tactic T = repeat(conj_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic(); + tactic T = repeat(conj_tactic() || conj_hyp_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic(); // Generate proof using tactic expr pr = T.solve(env, io, context(), F); // Print proof