refactor(library/tactic/goal): use local names for hypotheses

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

src/frontends/lua/register_modules.cpp

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -8,9 +8,8 @@ Author: Leonardo de Moura
 #include "util/numerics/register_module.h"
 #include "util/sexpr/register_module.h"
 #include "library/register_module.h"
-// #include "library/io_state_stream.h"
 // #include "library/simplifier/register_module.h"
-// #include "library/tactic/register_module.h"
+#include "library/tactic/register_module.h"
 #include "frontends/lean/register_module.h"
 
 namespace lean {
@@ -19,7 +18,7 @@ void register_modules() {
     register_sexpr_module();
     register_core_module();
     // register_simplifier_module();
-    // register_tactic_module();
+    register_tactic_module();
     register_frontend_lean_module();
 }
 }

src/kernel/formatter.h

@@ -11,6 +11,8 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
+/** \brief Return true iff \c t contains a constant named \c n or a local constant with named (pp or not) \c n */
+bool is_used_name(expr const & t, name const & n);
 /**
     \brief Return the body of the binding \c b, where variable #0 is replaced by a local constant with a "fresh" name.
     The name is considered fresh if it is not used by a constant or local constant occuring in the body of \c b.

src/library/tactic/goal.cpp

@@ -6,47 +6,164 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include "util/buffer.h"
+#include "util/sstream.h"
+#include "kernel/replace_fn.h"
+#include "kernel/for_each_fn.h"
+#include "kernel/abstract.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/goal.h"
 
 namespace lean {
 goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {}
 
+static bool is_used_pp_name(hypothesis const * begin, hypothesis const * end, name const & n) {
+    return std::any_of(begin, end, [&](hypothesis const & h) { return local_pp_name(h.first) == n; });
+}
+
+static expr pick_unused_pp_name(hypothesis const * begin, hypothesis const * end, expr const & l) {
+    expr r = l;
+    unsigned i = 1;
+    while (is_used_pp_name(begin, end, local_pp_name(r))) {
+        name new_pp_name = local_pp_name(l);
+        new_pp_name = new_pp_name.append_after(i);
+        r = mk_local(new_pp_name, mlocal_type(l));
+        i++;
+    }
+    return r;
+}
+
+static void update_local(expr & t, expr const & old_local, expr const & new_local) {
+    t = replace(t, [&](expr const & e, unsigned) {
+            if (!has_local(e))
+                return some_expr(e);
+            if (e == old_local)
+                return some_expr(new_local);
+            return none_expr();
+        });
+}
+
+static void update_local(hypothesis * begin, hypothesis * end, expr & conclusion,
+                         expr const & old_local, expr const & new_local) {
+    for (auto it = begin; it != end; ++it)
+        update_local(it->first, old_local, new_local);
+    update_local(conclusion, old_local, new_local);
+}
+
 format goal::pp(environment const & env, formatter const & fmt, options const & opts) const {
     unsigned indent  = get_pp_indent(opts);
     bool unicode     = get_pp_unicode(opts);
     format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
+    expr conclusion  = m_conclusion;
     buffer<hypothesis> tmp;
     to_buffer(m_hypotheses, tmp);
+    std::reverse(tmp.begin(), tmp.end());
     bool first = true;
     format r;
-    for (auto const & p : tmp) {
+    auto end = tmp.end();
-        if (first) {
+    for (auto it = tmp.begin(); it != end; ++it) {
-            first = false;
+        if (first) first = false; else r += compose(comma(), line());
-        } else {
+        expr l     = it->first;
-            r += compose(comma(), line());
+        expr new_l = pick_unused_pp_name(tmp.begin(), it, l);
-        }
+        if (!is_eqp(l, new_l))
-        r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(env, p.second, opts)))};
+            update_local(it+1, end, conclusion, l, new_l);
+        r += format{format(local_pp_name(new_l)), space(), colon(), nest(indent, compose(line(), fmt(env, mlocal_type(new_l), opts)))};
     }
-
     r = group(r);
-    r += format{line(), turnstile, space(), nest(indent, fmt(env, m_conclusion, opts))};
+    r += format{line(), turnstile, space(), nest(indent, fmt(env, conclusion, opts))};
     return group(r);
 }
 
+expr goal::mk_meta(name const & n, expr const & type) const {
+    if (has_local(type)) {
+        bool failed = false;
+        name missing;
+        for_each(type, [&](expr const & e, unsigned) {
+                if (!has_local(e) || failed) return false;
+                if (is_local(e)) {
+                    bool found = false;
+                    for (hypothesis const & h : m_hypotheses) {
+                        if (h.second && h.first == e) {
+                            found = true;
+                            break;
+                        }
+                    }
+                    if (!found) {
+                        failed  = true;
+                        missing = local_pp_name(e);
+                        return false;
+                    }
+                }
+                return true;
+            });
+        if (failed) {
+            throw exception(sstream() << "invalid metavariable for goal, metavariable type contains local constant '"
+                            << missing << "' which is not a hypothesis for this goal");
+        }
+    }
+    expr t = type;
+    buffer<expr> args;
+    for (hypothesis const & h : m_hypotheses) {
+        if (h.second) {
+            t = Pi(h.first, t);
+            args.push_back(h.first);
+        }
+    }
+    std::reverse(args.begin(), args.end());
+    return mk_app(mk_metavar(n, t), args);
+}
+
+static bool validate(expr const & r, hypotheses const & hs) {
+    bool failed = false;
+    for_each(r, [&](expr const & e, unsigned) {
+            if (!has_local(e) || failed) return false;
+            if (is_local(e) &&
+                !std::any_of(hs.begin(), hs.end(), [&](hypothesis const & h) { return h.first == e; })) {
+                failed = true;
+                return false;
+            }
+            return true;
+        });
+    return !failed;
+}
+
+bool goal::validate() const {
+    if (!::lean::validate(m_conclusion, m_hypotheses))
+        return false;
+    hypotheses const * h = &m_hypotheses;
+    while (!is_nil(*h)) {
+        if (!::lean::validate(mlocal_type(head(*h).first), tail(*h)))
+            return false;
+        h = &tail(*h);
+    }
+    return true;
+}
+
 DECL_UDATA(hypotheses)
 
 static int mk_hypotheses(lua_State * L) {
-    int nargs = lua_gettop(L);
+    int i = lua_gettop(L);
-    if (nargs == 0) {
+    hypotheses r;
-        return push_hypotheses(L, hypotheses());
+    if (i > 0 && is_hypotheses(L, i)) {
-    } else if (nargs == 2) {
+        r = to_hypotheses(L, i);
-        return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses()));
+        i--;
-    } else if (nargs == 3) {
-        return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3)));
-    } else {
-        throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments");
     }
+    while (i > 0) {
+        if (is_expr(L, i)) {
+            expr const & l = to_expr(L, i);
+            if (!is_local(l))
+                throw exception(sstream() << "arg #" << i << " must be a local constant or a pair");
+            r = hypotheses(hypothesis(l, true), r);
+        } else {
+            lua_rawgeti(L, i, 1);
+            lua_rawgeti(L, i, 2);
+            if (!is_expr(L, -2) || !is_local(to_expr(L, -2)) || !lua_isboolean(L, -1))
+                throw exception(sstream() << "arg #" << i << " must be a pair: local constant, Boolean");
+            r = hypotheses(hypothesis(to_expr(L, -2), lua_toboolean(L, -1)), r);
+            lua_pop(L, 2);
+        }
+        i--;
+    }
+    return push_hypotheses(L, r);
 }
 
 static int hypotheses_is_nil(lua_State * L) {
@@ -58,8 +175,8 @@ static int hypotheses_head(lua_State * L) {
     hypotheses const & hs = to_hypotheses(L, 1);
     if (!hs)
         throw exception("head method expects a non-empty hypotheses list");
-    push_name(L, head(hs).first);
+    push_expr(L, head(hs).first);
-    push_expr(L, head(hs).second);
+    push_boolean(L, head(hs).second);
     return 2;
 }
 
@@ -76,8 +193,8 @@ static int hypotheses_next(lua_State * L) {
     if (hs) {
         push_hypotheses(L, tail(hs));
         lua_replace(L, lua_upvalueindex(1));
-        push_name(L, head(hs).first);
+        push_expr(L, head(hs).first);
-        push_expr(L, head(hs).second);
+        push_boolean(L, head(hs).second);
         return 2;
     } else {
         lua_pushnil(L);
@@ -124,7 +241,7 @@ static int goal_tostring(lua_State * L) {
     lua_pushstring(L, out.str().c_str());
     return 1;
 }
-
+static int goal_mk_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3))); }
 static int goal_pp(lua_State * L) {
     int nargs = lua_gettop(L);
     goal & g = to_goal(L, 1);
@@ -138,6 +255,7 @@ static int goal_pp(lua_State * L) {
         return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4)));
     }
 }
+static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate()); }
 
 static const struct luaL_Reg goal_m[] = {
     {"__gc",            goal_gc}, // never throws
@@ -145,7 +263,9 @@ static const struct luaL_Reg goal_m[] = {
     {"hypotheses",      safe_function<goal_hypotheses>},
     {"hyps",            safe_function<goal_hypotheses>},
     {"conclusion",      safe_function<goal_conclusion>},
+    {"mk_meta",         safe_function<goal_mk_meta>},
     {"pp",              safe_function<goal_pp>},
+    {"validate",        safe_function<goal_validate>},
     {0, 0}
 };
 

src/library/tactic/goal.h

@@ -14,7 +14,11 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 
 namespace lean {
-typedef std::pair<name, expr> hypothesis;
+/**
+    \brief A hypothesis is a local variable + a flag indicating whether it is "contextual" or not.
+    Only contextual ones are used to build the context of new metavariables.
+*/
+typedef std::pair<expr, bool> hypothesis;
 typedef list<hypothesis>      hypotheses;
 class goal {
     hypotheses m_hypotheses;
@@ -24,14 +28,27 @@ public:
     goal(hypotheses const & hs, expr const & c);
     hypotheses const & get_hypotheses() const { return m_hypotheses; }
     expr const & get_conclusion() const { return m_conclusion; }
+    /**
+        \brief Create a metavarible application <tt>(m l_1 ... l_n)</tt> with type \c type,
+        where \c l_1 ... \c l_n are the contextual hypotheses of this goal, and
+        \c m is a metavariable with name \c n.
+    */
+    expr mk_meta(name const & n, expr const & type) const;
+    /**
+        brief Return true iff this is a valid goal.
+        We say a goal is valid when the conclusion only contains local constants that are in hypotheses,
+        and each hypothesis only contains local constants that occur in the previous hypotheses.
+    */
+    bool validate() const;
     format pp(environment const & env, formatter const & fmt, options const & opts) const;
 };
 
 inline goal update(goal const & g, expr const & c) { return goal(g.get_hypotheses(), c); }
 inline goal update(goal const & g, hypotheses const & hs) { return goal(hs, g.get_conclusion()); }
 inline goal update(goal const & g, buffer<hypothesis> const & hs) { return goal(to_list(hs.begin(), hs.end()), g.get_conclusion()); }
-inline hypotheses add_hypothesis(name const & h_name, expr const & h, hypotheses const & hs) {
+inline hypotheses add_hypothesis(expr const & l, hypotheses const & hs) {
-    return cons(mk_pair(h_name, h), hs);
+    lean_assert(is_local(l));
+    return cons(hypothesis(l, true), hs);
 }
 inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) {
     return cons(h, hs);

src/library/tactic/register_module.h

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -7,24 +7,22 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/script_state.h"
 #include "library/tactic/goal.h"
-#include "library/tactic/proof_builder.h"
+// #include "library/tactic/proof_builder.h"
-#include "library/tactic/cex_builder.h"
+// #include "library/tactic/cex_builder.h"
-#include "library/tactic/proof_state.h"
+// #include "library/tactic/proof_state.h"
-#include "library/tactic/tactic.h"
+// #include "library/tactic/tactic.h"
-#include "library/tactic/boolean_tactics.h"
+// #include "library/tactic/apply_tactic.h"
-#include "library/tactic/apply_tactic.h"
+// #include "library/tactic/simplify_tactic.h"
-#include "library/tactic/simplify_tactic.h"
 
 namespace lean {
 inline void open_tactic_module(lua_State * L) {
     open_goal(L);
-    open_proof_builder(L);
+    // open_proof_builder(L);
-    open_cex_builder(L);
+    // open_cex_builder(L);
-    open_proof_state(L);
+    // open_proof_state(L);
-    open_tactic(L);
+    // open_tactic(L);
-    open_boolean_tactics(L);
+    // open_apply_tactic(L);
-    open_apply_tactic(L);
+    // open_simplify_tactic(L);
-    open_simplify_tactic(L);
 }
 inline void register_tactic_module() {
     script_state::register_module(open_tactic_module);

tests/lua/goal1.lua

@@ -0,0 +1,16 @@
+local env = environment()
+local A = Local("A", Type)
+env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool))))
+local eq = Const("eq")
+local a  = Local("a", A)
+local b  = mk_local("b", "a", A)
+local H  = Local("H", eq(A, a, b))
+local hs = hypotheses(H, a, b, A)
+local g = goal(hs, eq(A, b, a))
+print(g)
+assert(g:validate())
+local m1 = g:mk_meta("m1", Bool)
+print(tostring(m1))
+print(env:type_check(m1))
+
+assert(not goal(hypotheses(H, A, a, b), eq(A, b, a)):validate())