feat(library/tactic): add precision and counterexample builder to proof state

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/cex_builder.h

@@ -0,0 +1,68 @@
+/*
+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 <algorithm>
+#include "util/debug.h"
+#include "util/name.h"
+#include "util/rc.h"
+#include "kernel/expr.h"
+#include "kernel/environment.h"
+#include "library/tactic/assignment.h"
+
+namespace lean {
+/**
+   \brief In Lean, a counter-example is encoded using an environment object.
+*/
+typedef environment counterexample;
+
+/**
+   \brief Base class for functors that build a counterexample for the main goal based on
+   a counterexample for a subgoal.
+*/
+class cex_builder_cell {
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
+public:
+    cex_builder_cell():m_rc(0) {}
+    virtual ~cex_builder_cell() {}
+    virtual counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const = 0;
+};
+
+template<typename F>
+class cex_builder_tpl : public cex_builder_cell {
+    F m_f;
+public:
+    cex_builder_tpl(F && f):m_f(f) {}
+    virtual counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const {
+        return m_f(n, cex, a);
+    }
+};
+
+/**
+   \brief Smart pointer for a counterexample builder functor.
+*/
+class cex_builder {
+protected:
+    cex_builder_cell * m_ptr;
+public:
+    cex_builder():m_ptr(nullptr) {}
+    explicit cex_builder(cex_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
+    cex_builder(cex_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    cex_builder(cex_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~cex_builder() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(cex_builder & a, cex_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
+    cex_builder & operator=(cex_builder const & s) { LEAN_COPY_REF(cex_builder, s); }
+    cex_builder & operator=(cex_builder && s) { LEAN_MOVE_REF(cex_builder, s); }
+
+    counterexample operator()(name const & n, optional<counterexample> const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); }
+};
+
+template<typename F>
+cex_builder mk_cex_builder(F && f) {
+    return cex_builder(new cex_builder_tpl<F>(std::forward<F>(f)));
+}
+}

src/library/tactic/proof_state.cpp

@@ -8,6 +8,21 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+precision mk_union(precision p1, precision p2) {
+    if (p1 == p2) return p1;
+    else if (p1 == precision::Precise) return p2;
+    else if (p2 == precision::Precise) return p1;
+    else return precision::UnderOver;
+}
+
+bool trust_proofs(precision p) {
+    return p == precision::Precise || p == precision::Over;
+}
+
+bool trust_cex(precision p) {
+    return p == precision::Precise || p == precision::Under;
+}
+
 format proof_state::pp(formatter const & fmt, options const & opts) const {
     format r;
     bool first = true;
@@ -29,11 +44,14 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co
     goal_proof_fn fn         = gfn.second;
     proof_builder pr_builder = mk_proof_builder(
         [=](proof_map const & m, assignment const &) -> expr {
-            expr p = find(m, g_main);
-            if (!p)
-                throw exception(sstream() << "failed to find proof for '" << g_main << "' goal");
-            return fn(p);
+            return fn(find(m, g_main));
         });
-    return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder);
+    cex_builder cex_builder = mk_cex_builder(
+        [](name const & n, optional<counterexample> const & cex, assignment const &) -> counterexample {
+            if (n != g_main || !cex)
+                throw exception(sstream() << "failed to build counterexample for '" << g_main << "' goal");
+            return *cex;
+        });
+    return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);
 }
 }

src/library/tactic/proof_state.h

@@ -12,34 +12,55 @@ Author: Leonardo de Moura
 #include "util/optional.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
+#include "library/tactic/cex_builder.h"
 
 namespace lean {
 typedef list<std::pair<name, goal>> goals;
+
+enum class precision {
+    Precise,
+    Under,   // counter-examples can be trusted
+    Over,    // proofs can be trusted
+    UnderOver // proof_state is garbage: it was produced using under and over approximation steps.
+};
+
+precision mk_union(precision p1, precision p2);
+bool trust_proofs(precision p);
+bool trust_cex(precision p);
+
 class proof_state {
     struct cell {
         MK_LEAN_RC();
+        precision                   m_precision;
         goals                       m_goals;
         metavar_env                 m_menv;
         proof_builder               m_proof_builder;
+        cex_builder                 m_cex_builder;
         void dealloc() { delete this; }
         cell():m_rc(1) {}
-        cell(goals const & gs, metavar_env const & menv, proof_builder const & p):
-            m_rc(1), m_goals(gs), m_menv(menv), m_proof_builder(p) {}
+        cell(precision prec, goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c):
+            m_rc(1), m_precision(prec), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {}
+        cell(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c):
+            m_rc(1), m_precision(precision::Precise), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {}
     };
     cell * m_ptr;
 public:
     proof_state():m_ptr(new cell()) {}
     proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
-    proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p):m_ptr(new cell(gs, menv, p)) {}
-    proof_state(proof_state const & s, goals const & gs, proof_builder const & p):m_ptr(new cell(gs, s.m_ptr->m_menv, p)) {}
+    proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c):
+        m_ptr(new cell(gs, menv, p, c)) {}
+    proof_state(proof_state const & s, goals const & gs, proof_builder const & p):
+        m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, s.get_cex_builder())) {}
     ~proof_state() { if (m_ptr) m_ptr->dec_ref(); }
     friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); }
     proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(proof_state, s); }
     proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(proof_state, s); }
+    precision get_precision() const { lean_assert(m_ptr); return m_ptr->m_precision; }
     goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; }
     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; }
     format pp(formatter const & fmt, options const & opts) const;
 };
 

src/library/tactic/tactic.cpp

@@ -27,6 +27,8 @@ expr tactic::solve(environment const & env, io_state const & io, proof_state con
     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);