feat(library/tactic): add tactic framework APIs

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

src/CMakeLists.txt

@@ -157,6 +157,8 @@ add_subdirectory(library/rewriter)
 set(LEAN_LIBS ${LEAN_LIBS} rewriter)
 add_subdirectory(library/elaborator)
 set(LEAN_LIBS ${LEAN_LIBS} elaborator)
+add_subdirectory(library/tactic)
+set(LEAN_LIBS ${LEAN_LIBS} tactic)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 add_subdirectory(bindings/lua)
@@ -171,6 +173,7 @@ add_subdirectory(tests/util/interval)
 add_subdirectory(tests/kernel)
 add_subdirectory(tests/library)
 add_subdirectory(tests/library/rewriter)
+add_subdirectory(tests/library/tactic)
 add_subdirectory(tests/library/elaborator)
 add_subdirectory(tests/frontends/lean)
 

src/library/tactic/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(tactic goal.cpp)
+target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/assignment.h

@@ -0,0 +1,20 @@
+/*
+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 "kernel/metavar.h"
+
+namespace lean {
+/**
+   \brief Wrapper for metavar_env that only allows us to access the assignment.
+*/
+class assignment {
+    metavar_env m_menv;
+public:
+    assignment(metavar_env const & menv):m_menv(menv) {}
+    expr operator()(name const & mvar) const { return m_menv.get_subst(mvar); }
+};
+}

src/library/tactic/goal.cpp

@@ -0,0 +1,115 @@
+/*
+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 <utility>
+#include <vector>
+#include "util/name_set.h"
+#include "util/buffer.h"
+#include "kernel/for_each_fn.h"
+#include "kernel/replace.h"
+#include "kernel/abstract.h"
+#include "library/type_inferer.h"
+#include "library/tactic/goal.h"
+
+namespace lean {
+
+goal::goal(list<std::pair<name, expr>> const & h, expr const & c):m_hypotheses(h), m_conclusion(c) {}
+
+goal_proof_fn::goal_proof_fn(std::vector<expr> && consts):
+    m_constants(consts) {
+}
+
+expr goal_proof_fn::operator()(expr const & pr) {
+    return abstract(pr, m_constants.size(), m_constants.data());
+}
+
+static name_set collect_used_names(context const & ctx, expr const & t) {
+    name_set r;
+    auto f = [&r](expr const & e, unsigned) { if (is_constant(e)) r.insert(const_name(e)); return true; };
+    for_each_fn<decltype(f)> visitor(f);
+    for (auto const & e : ctx) {
+        if (expr const & d = e.get_domain())
+            visitor(d);
+        if (expr const & b = e.get_body())
+            visitor(b);
+    }
+    visitor(t);
+    return r;
+}
+
+static name mk_unique_name(name_set & s, name const & suggestion) {
+    unsigned i = 1;
+    name n = suggestion;
+    while (true) {
+        if (s.find(n) == s.end()) {
+            s.insert(n);
+            return n;
+        } else {
+            n = name(suggestion, i);
+            i++;
+        }
+    }
+}
+
+std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const & ctx, expr const & t) {
+    type_inferer inferer(env);
+    if (!inferer.is_proposition(t))
+        throw exception("to goal failed, type is not a proposition");
+    name_set used_names = collect_used_names(ctx, t);
+    buffer<context_entry> entries;
+    for (auto const & e : ctx)
+        entries.push_back(e);
+    buffer<std::pair<name, expr>> hypotheses;  // normalized names and types of the entries processed so far
+    buffer<expr> bodies;                       // normalized bodies of the entries processed so far
+    std::vector<expr> consts;                  // cached consts[i] == mk_constant(names[i], hypotheses[i])
+    auto replace_vars = [&](expr const & e, unsigned offset) {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx >= offset) {
+                unsigned nvidx = vidx - offset;
+                unsigned nfv   = consts.size();
+                if (nvidx >= nfv)
+                    throw exception("to_goal failed, unknown free variable");
+                unsigned lvl   = nfv - nvidx - 1;
+                if (bodies[lvl])
+                    return bodies[lvl];
+                else
+                    return consts[lvl];
+            }
+        }
+        return e;
+    };
+    replace_fn<decltype(replace_vars)> replacer(replace_vars);
+    auto it    = entries.end();
+    auto begin = entries.begin();
+    while (it != begin) {
+        --it;
+        auto const & e = *it;
+        name n = mk_unique_name(used_names, e.get_name());
+        expr d = replacer(e.get_domain());
+        expr b = replacer(e.get_body());
+        replacer.clear();
+        if (b && (!d || !inferer.is_proposition(d))) {
+            hypotheses.emplace_back(n, expr());
+            bodies.push_back(b);
+            consts.push_back(expr());
+        } else {
+            hypotheses.emplace_back(n, d);
+            bodies.push_back(expr());
+            consts.push_back(mk_constant(n, d));
+        }
+    }
+    expr conclusion = replacer(t);
+    return mk_pair(goal(reverse_to_list(hypotheses.begin(), hypotheses.end()), conclusion),
+                   goal_proof_fn(std::move(consts)));
+}
+
+#if 0
+
+
+
+#endif
+}

src/library/tactic/goal.h

@@ -0,0 +1,50 @@
+/*
+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 <utility>
+#include <vector>
+#include "util/list.h"
+#include "util/name.h"
+#include "kernel/expr.h"
+#include "kernel/context.h"
+#include "kernel/environment.h"
+
+namespace lean {
+class goal {
+    list<std::pair<name, expr>> m_hypotheses;
+    expr                        m_conclusion;
+public:
+    goal(list<std::pair<name, expr>> const & h, expr const & c);
+    list<std::pair<name, expr>> const & get_hypotheses() const { return m_hypotheses; }
+    expr const & get_conclusion() const { return m_conclusion; }
+};
+
+/**
+   \brief Functor for converting a proof for a goal \c g produced using <tt>to_goal(env, ctx, T)</tt>
+   into a term of type \c t.
+
+   That is, the goal was created to synthesize a proof term for a proposition/type \c T in a
+   context \c ctx. This functor allows us to convert a proof for \c g into a term/expression \c p
+   s.t. <tt>ctx |- p : T</t>
+*/
+class goal_proof_fn {
+    friend std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const & ctx, expr const & t);
+    std::vector<expr> m_constants;
+    goal_proof_fn(std::vector<expr> && constants);
+public:
+    expr operator()(expr const & pr);
+};
+
+/**
+   \brief Convert the synthesis problem <tt>ctx |- ?p : T</tt> into a goal,
+   where \c T is a proposition (i.e., has type Boolean), and \c ?p is a proof we want to synthesize.
+
+   We can use tactics for solving the resultant goal, and the functor \c goal_proof_fn
+   to convert the proof for the goal into the proof term \c ?p.
+*/
+std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const & ctx, expr const & t);
+}

src/library/tactic/justification_builder.h

@@ -0,0 +1,38 @@
+/*
+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/name.h"
+#include "util/rc.h"
+#include "kernel/expr.h"
+#include "kernel/justification.h"
+#include "library/tactic/assignment.h"
+
+namespace lean {
+class justification_builder_cell {
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
+public:
+    virtual ~justification_builder_cell() {}
+    virtual justification operator()(name const & n, justification const & j, assignment const & a) const = 0;
+};
+
+class justification_builder {
+protected:
+    justification_builder_cell * m_ptr;
+public:
+    explicit justification_builder(justification_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
+    justification_builder(justification_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    justification_builder(justification_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~justification_builder() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(justification_builder & a, justification_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
+    justification_builder & operator=(justification_builder const & s) { LEAN_COPY_REF(justification_builder, s); }
+    justification_builder & operator=(justification_builder && s) { LEAN_MOVE_REF(justification_builder, s); }
+
+    justification operator()(name const & n, justification const & j, assignment const & a) const { return m_ptr->operator()(n, j, a); }
+};
+}

src/library/tactic/proof_builder.h

@@ -0,0 +1,41 @@
+/*
+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/splay_map.h"
+#include "util/rc.h"
+#include "kernel/expr.h"
+#include "library/tactic/assignment.h"
+
+namespace lean {
+typedef splay_map<name, expr, name_quick_cmp> proof_map;
+
+class proof_builder_cell {
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
+public:
+    virtual ~proof_builder_cell() {}
+    virtual expr operator()(proof_map const & p, assignment const & a) const = 0;
+};
+
+class proof_builder {
+protected:
+    proof_builder_cell * m_ptr;
+public:
+    explicit proof_builder(proof_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
+    proof_builder(proof_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    proof_builder(proof_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~proof_builder() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(proof_builder & a, proof_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
+    proof_builder & operator=(proof_builder const & s) { LEAN_COPY_REF(proof_builder, s); }
+    proof_builder & operator=(proof_builder && s) { LEAN_MOVE_REF(proof_builder, s); }
+
+    expr operator()(proof_map const & p, assignment const & a) const { return m_ptr->operator()(p, a); }
+};
+}

src/library/tactic/proof_state.h

@@ -0,0 +1,21 @@
+/*
+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 <utility>
+#include "library/tactic/goal.h"
+#include "library/tactic/proof_builder.h"
+#include "library/tactic/justification_builder.h"
+
+namespace lean {
+class proof_state {
+    list<std::pair<name, goal>> m_goals;
+    metavar_env                 m_menv;
+    proof_builder               m_proof_builder;
+    justification_builder       m_justification_builder;
+public:
+};
+}

src/library/tactic/tactic.h

@@ -0,0 +1,36 @@
+/*
+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/lazy_list.h"
+#include "library/tactic/proof_state.h"
+
+namespace lean {
+class tactic_cell {
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
+public:
+    virtual ~tactic_cell() {}
+    virtual lazy_list<proof_state> operator()(proof_state const & p) const = 0;
+};
+
+class tactic {
+protected:
+    tactic_cell * m_ptr;
+public:
+    explicit tactic(tactic_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    tactic(tactic const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    tactic(tactic && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~tactic() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(tactic & a, tactic & b) { std::swap(a.m_ptr, b.m_ptr); }
+    tactic & operator=(tactic const & s) { LEAN_COPY_REF(tactic, s); }
+    tactic & operator=(tactic && s) { LEAN_MOVE_REF(tactic, s); }
+
+    lazy_list<proof_state> operator()(proof_state const & p) const { return m_ptr->operator()(p); }
+};
+}
+

src/library/type_inferer.cpp

@@ -247,5 +247,10 @@ expr type_inferer::operator()(expr const & e, context const & ctx) {
     buffer<unification_constraint> uc;
     return operator()(e, ctx, nullptr, uc);
 }
+bool type_inferer::is_proposition(expr const & e, context const & ctx) {
+    expr t = operator()(e, ctx);
+    // TODO(Leo): consider replacing the following test with is_convertible(t, Bool);
+    return t == Bool;
+}
 void type_inferer::clear() { m_ptr->clear(); }
 }

src/library/type_inferer.h

@@ -33,7 +33,7 @@ public:
 
     expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc);
     expr operator()(expr const & e, context const & ctx = context());
-
+    bool is_proposition(expr const & e, context const & ctx = context());
     void clear();
 };
 }

src/tests/library/tactic/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_executable(tactic_tst tactic.cpp)
+target_link_libraries(tactic_tst ${EXTRA_LIBS})
+add_test(tactic ${CMAKE_CURRENT_BINARY_DIR}/tactic_tst)

src/tests/library/tactic/tactic.cpp

@@ -0,0 +1,17 @@
+/*
+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 "util/test.h"
+#include "library/tactic/goal.h"
+#include "library/tactic/proof_builder.h"
+#include "library/tactic/justification_builder.h"
+#include "library/tactic/proof_state.h"
+#include "library/tactic/tactic.h"
+using namespace lean;
+
+int main() {
+    return has_violations() ? 1 : 0;
+}