michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic): add support for Pi's at to_proof_state

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-22 16:37:38 -08:00
parent 104bd990e1
commit 3e32d9bef2
8 changed files with 58 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/frontends/lean/parser.cpp
View file

@ -1806,22 +1806,24 @@ class parser::imp {
if (has_metavar(mvar_type))
throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type,
"failed to synthesize metavar, its type contains metavariables");
if (!is_proposition(mvar_type, m_env, mvar_ctx))
throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
if (hint_and_pos.first) {
// metavariable has an associated tactic hint
s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
} else {
if (curr_is_period()) {
display_proof_state_if_interactive(s);
show_tactic_prompt();
next();
try {
proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
if (hint_and_pos.first) {
// metavariable has an associated tactic hint
s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
} else {
if (curr_is_period()) {
display_proof_state_if_interactive(s);
show_tactic_prompt();
next();
}
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
menv->assign(mvar, mvar_val);
}
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
menv->assign(mvar, mvar_val);
} catch (type_is_not_proposition_exception &) {
throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
}
}
return menv->instantiate_metavars(val);

1
src/kernel/expr.h
View file

@ -426,6 +426,7 @@ inline expr mk_eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r
inline expr Eq(expr const & l, expr const & r) { return mk_eq(l, r); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); }
inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }

4
src/library/tactic/goal.cpp
View file

@ -102,7 +102,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) {
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 exception("to_goal failed, type is not a proposition");
throw type_is_not_proposition_exception();
name_set used_names = collect_used_names(ctx, t);
buffer<context_entry> entries;
for (auto const & e : ctx)
@ -118,7 +118,7 @@ std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const
unsigned nvidx = vidx - offset;
unsigned nfv = consts.size();
if (nvidx >= nfv)
throw exception("to_goal failed, unknown free variable");
throw exception("failed to create goal, unknown free variable");
unsigned lvl = nfv - nvidx - 1;
if (bodies[lvl])
return *(bodies[lvl]);

10
src/library/tactic/goal.h
View file

@ -10,12 +10,22 @@ Author: Leonardo de Moura
#include "util/lua.h"
#include "util/list.h"
#include "util/name.h"
#include "util/exception.h"
#include "kernel/formatter.h"
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/environment.h"
namespace lean {
class type_is_not_proposition_exception : public exception {
public:
type_is_not_proposition_exception() {}
virtual ~type_is_not_proposition_exception() noexcept {}
virtual char const * what() const noexcept { return "type is not a propostion"; }
virtual exception * clone() const { return new type_is_not_proposition_exception(); }
virtual void rethrow() const { throw *this; }
};
typedef std::pair<name, expr> hypothesis;
typedef list<hypothesis> hypotheses;
class goal {

20
src/library/tactic/proof_state.cpp
View file

@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/sstream.h"
#include "kernel/builtin.h"
#include "kernel/type_checker.h"
#include "library/kernel_bindings.h"
#include "library/tactic/proof_state.h"
@ -88,13 +90,27 @@ void proof_state::get_goal_names(name_set & r) const {
static name g_main("main");
proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t) {
proof_state to_proof_state(ro_environment const & env, context ctx, expr t) {
list<std::pair<name, expr>> extra_binders;
while (is_pi(t)) {
name vname;
if (is_default_arrow_var_name(abst_name(t)) && is_proposition(abst_domain(t), env, ctx))
vname = name("H");
else
vname = abst_name(t);
extra_binders.emplace_front(vname, abst_domain(t));
ctx = extend(ctx, vname, abst_domain(t));
t = abst_body(t);
}
auto gfn = to_goal(env, ctx, t);
goal g = gfn.first;
goal_proof_fn fn = gfn.second;
proof_builder pr_builder = mk_proof_builder(
[=](proof_map const & m, assignment const &) -> expr {
return fn(find(m, g_main));
expr pr = fn(find(m, g_main));
for (auto p : extra_binders)
pr = mk_lambda(p.first, p.second, pr);
return pr;
});
cex_builder cex_builder = mk_cex_builder_for(g_main);
return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);

2
src/library/tactic/proof_state.h
View file

@ -96,7 +96,7 @@ public:
format pp(formatter const & fmt, options const & opts) const;
};
proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t);
proof_state to_proof_state(ro_environment const & env, context ctx, expr t);
inline optional<proof_state> some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) {
return some(proof_state(s, gs, p));

5
tests/lean/pr1.lean Normal file
View file

@ -0,0 +1,5 @@
Theorem T (C A B : Bool) : C -> A -> B -> A.
assumption.
done.
Show Environment 1.

4
tests/lean/pr1.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
Set: pp::colors
Set: pp::unicode
Proved: T
Theorem T (C A B : Bool) (H : C) (H : A) (H::1 : B) : A := H