lean2/src/library/tactic/goal.cpp

327 lines
10 KiB
C++
Raw Normal View History

/*
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 <algorithm>
#include "util/name_set.h"
#include "util/buffer.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "library/kernel_bindings.h"
#include "library/tactic/goal.h"
namespace lean {
name mk_unique_hypothesis_name(hypotheses const & hs, name const & suggestion) {
name n = suggestion;
unsigned i = 0;
// TODO(Leo): investigate if this method is a performance bottleneck
while (true) {
bool ok = true;
for (auto const & p : hs) {
if (is_prefix_of(n, p.first)) {
ok = false;
break;
}
}
if (ok) {
return n;
} else {
i++;
n = name(suggestion, i);
}
}
}
name update_hypotheses_fn::operator()(name const & suggestion, expr const & t) {
name n = mk_unique_hypothesis_name(m_hypotheses, suggestion);
m_hypotheses.emplace_front(n, t);
return n;
}
goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {}
format goal::pp(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("|-");
buffer<hypothesis> tmp;
to_buffer(m_hypotheses, tmp);
bool first = true;
format r;
for (auto const & p : tmp) {
if (first) {
first = false;
} else {
r += compose(comma(), line());
}
r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(p.second, opts)))};
}
r = group(r);
r += format{line(), turnstile, space(), nest(indent, fmt(m_conclusion, opts))};
return group(r);
}
name goal::mk_unique_hypothesis_name(name const & suggestion) const {
return ::lean::mk_unique_hypothesis_name(m_hypotheses, suggestion);
}
goal_proof_fn::goal_proof_fn(std::vector<expr> && consts):
m_constants(consts) {
}
expr goal_proof_fn::operator()(expr const & pr) const {
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 (optional<expr> const & d = e.get_domain())
visitor(*d);
if (optional<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(ro_environment const & env, context const & ctx, expr const & t) {
type_inferer inferer(env);
if (!inferer.is_proposition(t, ctx))
throw type_is_not_proposition_exception();
name_set used_names = collect_used_names(ctx, t);
buffer<context_entry> entries;
for (auto const & e : ctx)
entries.push_back(e);
std::reverse(entries.begin(), entries.end());
buffer<hypothesis> hypotheses; // normalized names and types of the entries processed so far
buffer<optional<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) -> expr {
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("failed to create goal, 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.begin();
auto end = entries.end();
for (; it != end; ++it) {
auto const & e = *it;
name n = mk_unique_name(used_names, e.get_name());
optional<expr> d = e.get_domain();
optional<expr> b = e.get_body();
if (d) d = some_expr(replacer(*d));
if (b) b = some_expr(replacer(*b));
fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term This commit fixes a problem exposed by t13.lean. It has a theorem of the form: Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type). Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions. Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created A : Bool, B : Bool, assumption : A /\ B |- B /\ A That is, the lemmas are not available when solving B /\ A. Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used. Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj (Conjunct2 assumption) (Conjunct1 assumption) This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A After this commit, the proof for theorem T1 is Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 as expected. Finally, this example suggests that the encoding Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) is more efficient than Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 00:14:15 +00:00
if (b && !d) {
d = some_expr(inferer(*b));
fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term This commit fixes a problem exposed by t13.lean. It has a theorem of the form: Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type). Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions. Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created A : Bool, B : Bool, assumption : A /\ B |- B /\ A That is, the lemmas are not available when solving B /\ A. Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used. Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj (Conjunct2 assumption) (Conjunct1 assumption) This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A After this commit, the proof for theorem T1 is Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 as expected. Finally, this example suggests that the encoding Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) is more efficient than Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 00:14:15 +00:00
}
replacer.clear();
if (b && !inferer.is_proposition(*d)) {
bodies.push_back(b);
consts.push_back(expr());
} else {
lean_assert(d);
hypotheses.emplace_back(n, *d);
bodies.push_back(none_expr());
consts.push_back(mk_constant(n, *d));
}
}
expr conclusion = replacer(t);
return mk_pair(goal(to_list(hypotheses.begin(), hypotheses.end()), conclusion),
goal_proof_fn(std::move(consts)));
}
DECL_UDATA(hypotheses)
static int mk_hypotheses(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 0) {
return push_hypotheses(L, hypotheses());
} else if (nargs == 2) {
return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses()));
} 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");
}
}
static int hypotheses_is_nil(lua_State * L) {
lua_pushboolean(L, !to_hypotheses(L, 1));
return 1;
}
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).second);
return 2;
}
static int hypotheses_tail(lua_State * L) {
hypotheses const & hs = to_hypotheses(L, 1);
if (!hs)
throw exception("tail method expects a non-empty hypotheses list");
push_hypotheses(L, tail(hs));
return 1;
}
static int hypotheses_next(lua_State * L) {
hypotheses & hs = to_hypotheses(L, lua_upvalueindex(1));
if (hs) {
push_hypotheses(L, tail(hs));
lua_replace(L, lua_upvalueindex(1));
push_name(L, head(hs).first);
push_expr(L, head(hs).second);
return 2;
} else {
lua_pushnil(L);
return 1;
}
}
static int hypotheses_items(lua_State * L) {
hypotheses & hs = to_hypotheses(L, 1);
push_hypotheses(L, hs); // upvalue(1): hypotheses
lua_pushcclosure(L, &safe_function<hypotheses_next>, 1); // create closure with 1 upvalue
return 1;
}
static int hypotheses_len(lua_State * L) {
lua_pushinteger(L, length(to_hypotheses(L, 1)));
return 1;
}
static const struct luaL_Reg hypotheses_m[] = {
{"__gc", hypotheses_gc}, // never throws
{"__len", safe_function<hypotheses_len>},
{"size", safe_function<hypotheses_len>},
{"pairs", safe_function<hypotheses_items>},
{"is_nil", safe_function<hypotheses_is_nil>},
{"empty", safe_function<hypotheses_is_nil>},
{"head", safe_function<hypotheses_head>},
{"tail", safe_function<hypotheses_tail>},
{0, 0}
};
DECL_UDATA(goal)
static int mk_goal(lua_State * L) {
return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2)));
}
static int goal_hypotheses(lua_State * L) {
return push_hypotheses(L, to_goal(L, 1).get_hypotheses());
}
static int goal_conclusion(lua_State * L) {
return push_expr(L, to_goal(L, 1).get_conclusion());
}
static int goal_unique_name(lua_State * L) {
return push_name(L, to_goal(L, 1).mk_unique_hypothesis_name(to_name_ext(L, 2)));
}
static int goal_tostring(lua_State * L) {
std::ostringstream out;
goal & g = to_goal(L, 1);
formatter fmt = get_global_formatter(L);
options opts = get_global_options(L);
out << mk_pair(g.pp(fmt, opts), opts);
lua_pushstring(L, out.str().c_str());
return 1;
}
static int goal_pp(lua_State * L) {
int nargs = lua_gettop(L);
goal & g = to_goal(L, 1);
if (nargs == 1) {
return push_format(L, g.pp(get_global_formatter(L), get_global_options(L)));
} else if (nargs == 2) {
if (is_formatter(L, 2))
return push_format(L, g.pp(to_formatter(L, 2), get_global_options(L)));
else
return push_format(L, g.pp(get_global_formatter(L), to_options(L, 2)));
} else {
return push_format(L, g.pp(to_formatter(L, 2), to_options(L, 3)));
}
}
static const struct luaL_Reg goal_m[] = {
{"__gc", goal_gc}, // never throws
{"__tostring", safe_function<goal_tostring>},
{"hypotheses", safe_function<goal_hypotheses>},
{"hyps", safe_function<goal_hypotheses>},
{"conclusion", safe_function<goal_conclusion>},
{"unique_name", safe_function<goal_unique_name>},
{"pp", safe_function<goal_pp>},
{0, 0}
};
static void hypotheses_migrate(lua_State * src, int i, lua_State * tgt) {
push_hypotheses(tgt, to_hypotheses(src, i));
}
static void goal_migrate(lua_State * src, int i, lua_State * tgt) {
push_goal(tgt, to_goal(src, i));
}
void open_goal(lua_State * L) {
luaL_newmetatable(L, hypotheses_mt);
set_migrate_fn_field(L, -1, hypotheses_migrate);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, hypotheses_m, 0);
SET_GLOBAL_FUN(hypotheses_pred, "is_hypotheses");
SET_GLOBAL_FUN(mk_hypotheses, "hypotheses");
luaL_newmetatable(L, goal_mt);
set_migrate_fn_field(L, -1, goal_migrate);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, goal_m, 0);
SET_GLOBAL_FUN(goal_pred, "is_goal");
SET_GLOBAL_FUN(mk_goal, "goal");
}
}