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 <leonardo@microsoft.com>

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) {

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 <tt> |- false</tt>,
+       and the precision is \c Precise or \c Under
+    */
+    bool is_cex_final_state() const;
     format pp(formatter const & fmt, options const & opts) const;
 };
 

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<proof_state> const & fs):m_kind(solve_result_kind::Failure) { new (&m_failures) list<proof_state>(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<proof_state>(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<proof_state>(); 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) {
+solve_result tactic::solve(environment const & env, io_state const & io, proof_state const & s1) {
-    proof_state_seq r   = operator()(env, io, s);
+    proof_state_seq r   = operator()(env, io, s1);
-    auto p = r.pull();
+    list<proof_state> failures;
-    if (!p)
+    while (true) {
-        throw exception("tactic failed to solve input");
+        check_interrupted();
-    proof_state final = p->first;
+        auto p = r.pull();
-    if (!trust_proofs(final.get_precision()))
+        if (!p) {
-        throw exception("tactic failed to solve input, final state is not precise");
+            return solve_result(failures);
-    assignment a(final.get_menv());
+        } else {
-    proof_map  m;
+            proof_state s2 = p->first;
-    return final.get_proof_builder()(m, a);
+            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<counterexample>(), 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);
 }

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<proof_state> m_failures;
+    };
+public:
+    solve_result(expr const & pr);
+    solve_result(counterexample const & cex);
+    solve_result(list<proof_state> 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<proof_state> 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);
+    solve_result 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, context const & ctx, expr const & t);
 };
 
 /**

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 {
+    solve_result r(t.solve(env, io, ctx, ty));
-        t.solve(env, io, ctx, ty);
+    lean_assert(r.kind() == solve_result_kind::Failure);
-        lean_unreachable();
-    } catch (exception & ex) {
-        std::cout << "expected error: " << ex.what() << "\n";
-    }
 }
 
 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 1: " << t.solve(env, io, s).get_proof() << "\n";
-    std::cout << "proof 2: " << t.solve(env, io, ctx, q) << "\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.