From c22f86311494a8a21b7975a8b64c6585d426e3a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Nov 2013 13:04:09 -0800 Subject: [PATCH] refactor(library/tactic): improve solve method Now, it produces the following outcomes: 1- A proof 2- A counterexample 3- A list of (unsolved) final states Remark: the solve method does not check whether the proof or counterexample is correct. Signed-off-by: Leonardo de Moura --- src/library/tactic/proof_state.cpp | 16 ++++++++- src/library/tactic/proof_state.h | 12 ++++++- src/library/tactic/tactic.cpp | 56 ++++++++++++++++++++++------- src/library/tactic/tactic.h | 28 +++++++++++++-- src/tests/library/tactic/tactic.cpp | 37 +++++++++---------- 5 files changed, 113 insertions(+), 36 deletions(-) diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index f5789f487..8084767d7 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "kernel/builtin.h" #include "library/tactic/proof_state.h" namespace lean { @@ -15,7 +16,7 @@ precision mk_union(precision p1, precision p2) { else return precision::UnderOver; } -bool trust_proofs(precision p) { +bool trust_proof(precision p) { return p == precision::Precise || p == precision::Over; } @@ -36,6 +37,19 @@ format proof_state::pp(formatter const & fmt, options const & opts) const { return r; } +bool proof_state::is_proof_final_state() const { + return empty(get_goals()) && trust_proof(get_precision()); +} + +bool proof_state::is_cex_final_state() const { + if (length(get_goals()) == 1 && trust_cex(get_precision())) { + goal const & g = head(get_goals()).second; + return is_false(g.get_conclusion()) && empty(g.get_hypotheses()); + } else { + return false; + } +} + static name g_main("main"); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index e20e16af9..34af333a0 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -25,7 +25,7 @@ enum class precision { }; precision mk_union(precision p1, precision p2); -bool trust_proofs(precision p); +bool trust_proof(precision p); bool trust_cex(precision p); class proof_state { @@ -61,6 +61,16 @@ public: metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; } proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; } cex_builder const & get_cex_builder() const { lean_assert(m_ptr); return m_ptr->m_cex_builder; } + /** + \brief Return true iff this state does not have any goals left, and + the precision is \c Precise or \c Over + */ + bool is_proof_final_state() const; + /** + \brief Return true iff this state has only one goal of the form |- false, + and the precision is \c Precise or \c Under + */ + bool is_cex_final_state() const; format pp(formatter const & fmt, options const & opts) const; }; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index a3e1292bc..f0dcf544c 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -13,6 +13,24 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { +solve_result::solve_result(expr const & pr):m_kind(solve_result_kind::Proof) { new (&m_proof) expr(pr); } +solve_result::solve_result(counterexample const & cex):m_kind(solve_result_kind::Counterexample) { new (&m_cex) counterexample(cex); } +solve_result::solve_result(list const & fs):m_kind(solve_result_kind::Failure) { new (&m_failures) list(fs); } +solve_result::solve_result(solve_result const & r):m_kind(r.m_kind) { + switch (m_kind) { + case solve_result_kind::Proof: new (&m_proof) expr(r.m_proof); break; + case solve_result_kind::Counterexample: new (&m_cex) counterexample(r.m_cex); break; + case solve_result_kind::Failure: new (&m_failures) list(r.m_failures); break; + } +} +solve_result::~solve_result() { + switch (m_kind) { + case solve_result_kind::Proof: m_proof.~expr(); break; + case solve_result_kind::Counterexample: m_cex.~counterexample(); break; + case solve_result_kind::Failure: m_failures.~list(); break; + } +} + tactic & tactic::operator=(tactic const & s) { LEAN_COPY_REF(tactic, s); } @@ -21,20 +39,34 @@ tactic & tactic::operator=(tactic && s) { LEAN_MOVE_REF(tactic, s); } -expr tactic::solve(environment const & env, io_state const & io, proof_state const & s) { - proof_state_seq r = operator()(env, io, s); - auto p = r.pull(); - if (!p) - throw exception("tactic failed to solve input"); - proof_state final = p->first; - if (!trust_proofs(final.get_precision())) - throw exception("tactic failed to solve input, final state is not precise"); - assignment a(final.get_menv()); - proof_map m; - return final.get_proof_builder()(m, a); +solve_result tactic::solve(environment const & env, io_state const & io, proof_state const & s1) { + proof_state_seq r = operator()(env, io, s1); + list failures; + while (true) { + check_interrupted(); + auto p = r.pull(); + if (!p) { + return solve_result(failures); + } else { + proof_state s2 = p->first; + r = p->second; + try { + if (s2.is_proof_final_state()) { + assignment a(s2.get_menv()); + proof_map m; + return solve_result(s2.get_proof_builder()(m, a)); + } else if (s2.is_cex_final_state()) { + assignment a(s2.get_menv()); + name goal_name(head(s2.get_goals()).first); + return solve_result(s2.get_cex_builder()(goal_name, optional(), a)); + } + } catch (exception & ex) {} + failures = cons(s2, failures); + } + } } -expr tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) { +solve_result tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) { proof_state s = to_proof_state(env, ctx, t); return solve(env, io, s); } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index bac0ac10f..027c73aa3 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -36,6 +36,30 @@ public: } }; +enum class solve_result_kind { Proof, Counterexample, Failure }; +/** + \brief Result for the solve method in the tactic class. + The result may be a proof, a counterexample, or a list of unsolved proof_states. +*/ +class solve_result { + solve_result_kind m_kind; + union { + expr m_proof; + counterexample m_cex; + list m_failures; + }; +public: + solve_result(expr const & pr); + solve_result(counterexample const & cex); + solve_result(list const & fs); + solve_result(solve_result const & r); + ~solve_result(); + solve_result_kind kind() const { return m_kind; } + expr get_proof() const { lean_assert(kind() == solve_result_kind::Proof); return m_proof; } + counterexample get_cex() const { lean_assert(kind() == solve_result_kind::Counterexample); return m_cex; } + list get_failures() const { lean_assert(kind() == solve_result_kind::Failure); return m_failures; } +}; + class tactic { protected: tactic_cell * m_ptr; @@ -50,8 +74,8 @@ public: proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const { return m_ptr->operator()(env, io, s); } - expr solve(environment const & env, io_state const & io, proof_state const & s); - expr solve(environment const & env, io_state const & io, context const & ctx, expr const & t); + solve_result solve(environment const & env, io_state const & io, proof_state const & s); + solve_result solve(environment const & env, io_state const & io, context const & ctx, expr const & t); }; /** diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 99223204f..7f00f6ac8 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -42,12 +42,8 @@ tactic show_opts_tactic() { } 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); - lean_unreachable(); - } catch (exception & ex) { - std::cout << "expected error: " << ex.what() << "\n"; - } + solve_result r(t.solve(env, io, ctx, ty)); + lean_assert(r.kind() == solve_result_kind::Failure); } static void tst1() { @@ -64,14 +60,14 @@ static void tst1() { proof_state s = to_proof_state(env, ctx, p); std::cout << s.pp(mk_simple_formatter(), options()) << "\n"; tactic t = then(assumption_tactic(), now_tactic()); - std::cout << "proof 1: " << t.solve(env, io, s) << "\n"; - std::cout << "proof 2: " << t.solve(env, io, ctx, q) << "\n"; + std::cout << "proof 1: " << t.solve(env, io, s).get_proof() << "\n"; + std::cout << "proof 2: " << t.solve(env, io, ctx, q).get_proof() << "\n"; check_failure(now_tactic(), env, io, ctx, q); - std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q) << "\n"; + std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q).get_proof() << "\n"; #ifndef __APPLE__ check_failure(try_for(loop_tactic(), 100), env, io, ctx, q); - std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s) << "\n"; + std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s).get_proof() << "\n"; check_failure(try_for(orelse(try_for(loop_tactic(), 10000), trace_tactic(std::string("hello world"))), 100), @@ -88,31 +84,31 @@ static void tst1() { env, io, ctx, q); lean_assert(flag1); std::cout << "Before parallel 3 parallel tactics...\n"; - std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q) << "\n"; + std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q).get_proof() << "\n"; #endif std::cout << "Before hello1 and 2...\n"; std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()), - t).solve(env, io, ctx, q) << "\n"; + t).solve(env, io, ctx, q).get_proof() << "\n"; std::cout << "------------------\n"; std::cout << "proof 2: " << ((trace_tactic("hello1.1") + trace_tactic("hello1.2") + trace_tactic("hello1.3") + trace_tactic("hello1.4")) << (trace_tactic("hello2.1") + trace_tactic("hello2.2")) << (trace_tactic("hello3.1") || trace_tactic("hello3.2")) << - assumption_tactic()).solve(env, io, ctx, q) << "\n"; + assumption_tactic()).solve(env, io, ctx, q).get_proof() << "\n"; std::cout << "------------------\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")), - t).solve(env, io, ctx, q) << "\n"; + t).solve(env, io, ctx, q).get_proof() << "\n"; 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"; + t).solve(env, io, ctx, q).get_proof() << "\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"; + trace_tactic("msg3") << t).solve(env, io, ctx, q).get_proof() << "\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"; + show_opts_tactic() << t).solve(env, io, ctx, q).get_proof() << "\n"; std::cout << "done\n"; } @@ -131,15 +127,16 @@ static void tst2() { 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))) + std::cout << "proof: " << (repeat(conj_tactic()) << assumption_tactic()).solve(env, io, ctx, And(And(p, q), And(p, p))).get_proof() << "\n"; std::cout << "-------------\n"; // Theorem to be proved expr F = Implies(And(p, And(r, s)), Implies(q, And(And(p, q), And(r, p)))); // Tactic - tactic T = repeat(conj_tactic() || conj_hyp_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic(); + tactic T = append(id_tactic() << assumption_tactic(), + 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); + expr pr = T.solve(env, io, context(), F).get_proof(); // Print proof std::cout << pr << "\n"; // Check whether the proof is correct or not.