diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 658d481ecc..53c9e95640 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp) +add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp boolean.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp new file mode 100644 index 0000000000..4b35ae65d9 --- /dev/null +++ b/src/library/tactic/boolean.cpp @@ -0,0 +1,98 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/interrupt.h" +#include "kernel/builtin.h" +#include "kernel/abstract.h" +#include "library/basic_thms.h" +#include "library/tactic/goal.h" +#include "library/tactic/proof_builder.h" +#include "library/tactic/proof_state.h" +#include "library/tactic/tactic.h" + +namespace lean { +bool is_app_of(expr const & e, expr const & f) { + return is_app(e) && arg(e, 0) == f; +} +tactic conj_tactic(bool all) { + return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + expr andfn = mk_and_fn(); + bool found = false; + buffer> new_goals_buf; + list> proof_info; + for (auto const & p : s.get_goals()) { + check_interrupted(); + goal const & g = p.second; + expr const & c = g.get_conclusion(); + if ((all || !found) && is_app_of(c, andfn)) { + found = true; + name const & n = p.first; + proof_info.emplace_front(n, c); + new_goals_buf.emplace_back(name(n, 1), goal(g.get_hypotheses(), arg(c, 1))); + new_goals_buf.emplace_back(name(n, 2), goal(g.get_hypotheses(), arg(c, 2))); + } else { + new_goals_buf.push_back(p); + } + } + 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 nc : proof_info) { + name const & n = nc.first; + expr const & c = nc.second; + new_m.insert(n, Conj(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2)))); + } + return p(new_m, env, a); + }); + goals new_goals = to_list(new_goals_buf.begin(), new_goals_buf.end()); + return some(proof_state(s, new_goals, new_p)); + } else { + return optional(); + } + }); +} +tactic imp_tactic(name const & H_name, bool all) { + return mk_tactic01([=](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 & ng, goal const & g) -> goal { + expr const & c = g.get_conclusion(); + if ((all || !found) && is_app_of(c, impfn)) { + found = true; + name new_hn = g.mk_unique_hypothesis_name(H_name); + proof_info.emplace_front(ng, new_hn, c); + expr new_h = arg(c, 1); + expr new_c = arg(c, 2); + return goal(cons(mk_pair(new_hn, new_h), g.get_hypotheses()), new_c); + } 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 info : proof_info) { + name const & gn = std::get<0>(info); // goal name + name const & hn = 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, gn); // proof for the new conclusion + new_m.insert(gn, Discharge(h, c, Fun(hn, h, c_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 new file mode 100644 index 0000000000..1e1d5c3cd2 --- /dev/null +++ b/src/library/tactic/boolean.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/tactic/tactic.h" +namespace lean { +tactic conj_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 0d690d1369..40371759ea 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -41,6 +41,26 @@ format goal::pp(formatter const & fmt, options const & opts) const { return group(r); } +name goal::mk_unique_hypothesis_name(name const & suggestion) const { + name n = suggestion; + unsigned i = 0; + while (true) { + bool ok = true; + for (auto const & p : m_hypotheses) { + if (n == p.first) { + ok = false; + break; + } + } + if (ok) { + return n; + } else { + i++; + n = name(suggestion, i); + } + } +} + goal_proof_fn::goal_proof_fn(std::vector && consts): m_constants(consts) { } diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 1cad7bebc1..72cd7148aa 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -25,6 +25,7 @@ public: expr const & get_conclusion() const { return m_conclusion; } operator bool() const { return m_conclusion; } format pp(formatter const & fmt, options const & opts) const; + name mk_unique_hypothesis_name(name const & suggestion) const; }; /** diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 9d5508229d..142dba0d6f 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -39,7 +39,7 @@ expr tactic::solve(environment const & env, io_state const & io, context const & } tactic id_tactic() { - return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); } @@ -60,7 +60,7 @@ tactic now_tactic() { } tactic trace_tactic(std::string const & msg) { - return mk_simple_tactic([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { + return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { io.get_diagnostic_channel() << msg << "\n"; io.get_diagnostic_channel().get_stream().flush(); return s; @@ -75,8 +75,17 @@ tactic trace_tactic(char const * msg) { return trace_tactic(std::string(msg)); } +tactic suppress_trace(tactic const & t) { + return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + io_state new_io(io); + std::shared_ptr out(new string_output_channel()); + new_io.set_diagnostic_channel(out); + return t(env, new_io, s); + }); +} + tactic assumption_tactic() { - return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state { list> proofs; goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { expr const & c = g.get_conclusion(); @@ -84,7 +93,7 @@ tactic assumption_tactic() { for (auto const & p : g.get_hypotheses()) { check_interrupted(); if (p.second == c) { - pr = mk_constant(p.first); + pr = mk_constant(p.first, p.second); break; } } @@ -122,6 +131,14 @@ tactic orelse(tactic const & t1, tactic const & t2) { }); } +tactic using_params(tactic const & t, options const & opts) { + return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + io_state new_io(io); + new_io.set_options(join(opts, io.get_options())); + return t(env, new_io, s); + }); +} + tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return timeout(t(env, io, s), ms, check_ms); @@ -167,16 +184,4 @@ tactic take(tactic const & t, unsigned k) { return take(k, t(env, io, s)); }); } - -tactic force(tactic const & t) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { - proof_state_seq r = t(env, io, s); - buffer buf; - for_each(r, [&](proof_state const & s2) { - buf.push_back(s2); - check_interrupted(); - }); - return to_lazy(to_list(buf.begin(), buf.end())); - }); -} } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 796d2bfb05..14bf1dcf5a 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -71,8 +71,9 @@ inline proof_state_seq mk_proof_state_seq(F && f) { } /** - \brief Create a tactic using the given functor. + \brief Create a tactic that produces exactly one output state. + The functor f must contain the method: proof_state operator()(environment const & env, io_state const & io, proof_state const & s) @@ -80,13 +81,37 @@ inline proof_state_seq mk_proof_state_seq(F && f) { \remark The functor is invoked on demand. */ template -tactic mk_simple_tactic(F && f) { +tactic mk_tactic1(F && f) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) { return mk_proof_state_seq([=]() { return some(mk_pair(f(env, io, s), proof_state_seq())); }); }); } +/** + \brief Create a tactic that produces at most one output state. + + The functor f must contain the method: + + optional operator()(environment const & env, io_state const & io, proof_state const & s) + + + \remark The functor is invoked on demand. +*/ +template +tactic mk_tactic01(F && f) { + return + mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) { + return mk_proof_state_seq([=]() { + auto r = f(env, io, s); + if (r) + return some(mk_pair(*r, proof_state_seq())); + else + return proof_state_seq::maybe_pair(); + }); + }); +} + inline proof_state_seq to_proof_state_seq(proof_state const & s) { return mk_proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); }); } @@ -123,6 +148,10 @@ tactic trace_tactic(char const * msg); class sstream; tactic trace_tactic(sstream const & msg); tactic trace_tactic(std::string const & msg); +/** + \brief Create a tactic that applies \c t, but suppressing diagnostic messages. +*/ +tactic suppress_trace(tactic const & t); /** \brief Return a tactic that performs \c t1 followed by \c t2. @@ -135,6 +164,11 @@ inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, */ tactic orelse(tactic const & t1, tactic const & t2); inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); } +/** + \brief Return a tactic that appies \c t, but using the additional set of options + \c opts. +*/ +tactic using_params(tactic const & t, options const & opts); /** \brief Return a tactic that tries the tactic \c t for at most \c ms milliseconds. If the tactic does not terminate in \c ms milliseconds, then the empty @@ -194,19 +228,6 @@ tactic take(tactic const & t, unsigned k); \brief Syntax sugar for take(t, 1) */ inline tactic determ(tactic const & t) { return take(t, 1); } -/** - \brief Return a tactic that forces \c t to produce all - the elements in the resultant sequence. - - \remark proof_state_seq is a lazy-list, that is, their - elements are produced on demand. This tactic forces - all the elements in the sequence to be computed eagerly. - - \remark The sequence may be infinite. So, consider - combining this tactical with \c take if the sequence - may be infinite or too big. -*/ -tactic force(tactic const & t); /** \brief Return a tactic that applies the predicate \c p to the input state. If \c p returns true, then applies \c t1. Otherwise, applies \c t2. diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index c250f093a2..511394a338 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -13,11 +13,11 @@ Author: Leonardo de Moura #include "library/tactic/proof_builder.h" #include "library/tactic/proof_state.h" #include "library/tactic/tactic.h" -#include "library/tactic/tactic_exception.h" +#include "library/tactic/boolean.h" using namespace lean; tactic loop_tactic() { - return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { while (true) { check_interrupted(); } @@ -26,12 +26,20 @@ tactic loop_tactic() { } tactic set_tactic(std::atomic * flag) { - return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { *flag = true; return s; }); } +tactic show_opts_tactic() { + return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { + io.get_diagnostic_channel() << "options: " << io.get_options() << "\n"; + io.get_diagnostic_channel().get_stream().flush(); + return s; + }); +} + static void check_failure(tactic t, environment const & env, io_state const & io, context const & ctx, expr const & ty) { try { t.solve(env, io, ctx, ty); @@ -90,9 +98,6 @@ static void tst1() { (trace_tactic("hello3.1") || trace_tactic("hello3.2")) << assumption_tactic()).solve(env, io, ctx, q) << "\n"; std::cout << "------------------\n"; - std::cout << "proof 2: " << force(take(repeat_at_most(interleave(id_tactic(), id_tactic()), 100) << trace_tactic("foo") << t, - 5)).solve(env, io, ctx, q) << "\n"; - std::cout << "proof 2: " << then(cond([](environment const &, io_state const &, proof_state const &) { return true; }, trace_tactic("then branch.1") + trace_tactic("then branch.2"), trace_tactic("else branch")), @@ -101,11 +106,42 @@ static void tst1() { std::cout << "proof 2: " << then(when([](environment const &, io_state const &, proof_state const &) { return true; }, trace_tactic("when branch.1") + trace_tactic("when branch.2")), t).solve(env, io, ctx, q) << "\n"; - + std::cout << "------------------\n"; + std::cout << "proof 2: " << (suppress_trace(trace_tactic("msg1") << trace_tactic("msg2")) << + trace_tactic("msg3") << t).solve(env, io, ctx, q) << "\n"; + std::cout << "------------------\n"; + std::cout << "proof 2: " << (show_opts_tactic() << using_params(show_opts_tactic(), options(name({"pp", "colors"}), true)) << + show_opts_tactic() << t).solve(env, io, ctx, q) << "\n"; std::cout << "done\n"; } +static void tst2() { + environment env; + io_state io(options(), mk_simple_formatter()); + import_all(env); + env.add_var("p", Bool); + env.add_var("q", Bool); + expr p = Const("p"); + expr q = Const("q"); + context ctx; + ctx = extend(ctx, "H1", p); + ctx = extend(ctx, "H2", q); + std::cout << "proof: " << (repeat(conj_tactic()) << assumption_tactic()).solve(env, io, ctx, And(And(p, q), And(p, p))) + << "\n"; + // Theorem to be proved + expr F = Implies(p, Implies(q, And(And(p, q), And(p, p)))); + // Tactic + tactic T = repeat(conj_tactic() || imp_tactic()) << assumption_tactic(); + // Generate proof using tactic + expr pr = T.solve(env, io, context(), F); + // Print proof + std::cout << pr << "\n"; + // Check whether the proof is correct or not. + std::cout << env.infer_type(pr) << "\n"; +} + int main() { tst1(); + tst2(); return has_violations() ? 1 : 0; }