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

feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-03 21:51:21 -08:00
parent a22346e411
commit ba392f504f
6 changed files with 72 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/builtin_exprs.cpp
View file

@ -227,7 +227,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos);
tacs.push_back(mk_begin_end_element_annotation(assert_tac));
if (p.curr_is_token(get_bar_tk())) {
expr local = p.save_pos(mk_local(id, A), id_pos);
expr local = p.save_pos(mk_local(id, A, mk_rec_info(true)), id_pos);
expr t = parse_local_equations(p, local);
t = p.mk_app(get_rexact_tac_fn(), t, pos);
t = p.save_pos(mk_begin_end_element_annotation(t), pos);
@ -438,7 +438,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
}
expr proof;
if (p.curr_is_token(get_bar_tk()) && !prev_local) {
expr fn = p.save_pos(mk_local(id, prop), id_pos);
expr fn = p.save_pos(mk_local(id, prop, mk_rec_info(true)), id_pos);
proof = parse_local_equations(p, fn);
} else {
p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
@ -521,7 +521,7 @@ static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & p
static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
expr prop = p.parse_expr();
if (p.curr_is_token(get_bar_tk())) {
expr fn = p.save_pos(mk_local(get_this_tk(), prop), pos);
expr fn = p.save_pos(mk_local(get_this_tk(), prop, mk_rec_info(true)), pos);
return parse_local_equations(p, fn);
} else {
p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected");

4
src/frontends/lean/decl_cmds.cpp
View file

@ -604,7 +604,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
for (expr const & param : ps)
p.add_local(param);
lean_assert(is_curr_with_or_comma_or_bar(p));
fns.push_back(mk_local(n, type));
fns.push_back(mk_local(n, type, mk_rec_info(true)));
if (p.curr_is_token(get_with_tk())) {
while (p.curr_is_token(get_with_tk())) {
p.next();
@ -612,7 +612,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
name g_name = p.check_decl_id_next("invalid declaration, identifier expected");
p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
expr g_type = p.parse_expr();
expr g = p.save_pos(mk_local(g_name, g_type), pos);
expr g = p.save_pos(mk_local(g_name, g_type, mk_rec_info(true)), pos);
auxs.push_back(g_name);
fns.push_back(g);
}

11
src/kernel/expr.h
View file

@ -217,22 +217,27 @@ class binder_info {
/** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be
inferred by class-instance resolution. */
unsigned m_inst_implicit:1;
/** \brief Auxiliary internal attribute used to mark local constants represeting recursive functions
in recursive equations */
unsigned m_rec:1;
public:
binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false):
binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false, bool rec = false):
m_implicit(implicit), m_contextual(contextual), m_strict_implicit(strict_implicit),
m_inst_implicit(inst_implicit) {}
m_inst_implicit(inst_implicit), m_rec(rec) {}
bool is_implicit() const { return m_implicit; }
bool is_contextual() const { return m_contextual; }
bool is_strict_implicit() const { return m_strict_implicit; }
bool is_inst_implicit() const { return m_inst_implicit; }
bool is_rec() const { return m_rec; }
unsigned hash() const;
binder_info update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit); }
binder_info update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit, m_rec); }
};
inline binder_info mk_implicit_binder_info() { return binder_info(true); }
inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true, true); }
inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, true, false, true); }
inline binder_info mk_contextual_info(bool f) { return binder_info(false, f); }
inline binder_info mk_rec_info(bool f) { return binder_info(false, true, false, false, f); }
inline bool is_explicit(binder_info const & bi) {
return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();

43
src/library/blast/blast.cpp
View file

@ -451,9 +451,46 @@ class blastenv {
g.get_hyps(hs);
for (expr const & h : hs) {
lean_assert(is_local(h));
expr new_type = normalize(to_blast_expr(mlocal_type(h)));
expr href = s.mk_hypothesis(local_pp_name(h), new_type, h);
local2href.insert(mlocal_name(h), href);
if (!local_info(h).is_rec()) {
/*
We do not add auxiliary locals used to compile recursive equations.
The problem is that blast doesn't know when it is safe to use this kind of hypothesis.
For example: suppose we are defining the following function using recursive equations and blast.
lemma comm : ∀ a b : nat, a + b = b + a
| a 0 := by simp
| a (succ n) := by simp
Both goals will contain the (rec) hypothesis
comm : ∀ a b : nat, a + b = b + a
If we the recursive equation is being compiled using structural recursion, then we can only apply
'comm' to strucuturall smaller terms. If we are using well-founded recursion, then we need the well-founded relation.
Blast does not have access to this information. We address this issue by simply ignoring this kind of
auxiliary rec hypothesis.
Of course, this workaround forces the user to provide a valid induction hypothesis.
Example:
lemma comm : ∀ a b : nat, a + b = b + a
| a 0 := by simp
| a (succ n) :=
assert a + n = n + a, from !comm,
by simp
In this simple example, we can simply ask blast to apply the recursor automatically for use.
lemma comm : ∀ a b : nat, a + b = b + a :=
by rec_simp
However, this is not always possible. Sometimes, we will be defining a complex function using recursive equations.
The definition may contain nested proofs that we may want to discharge using blast.
*/
expr new_type = normalize(to_blast_expr(mlocal_type(h)));
expr href = s.mk_hypothesis(local_pp_name(h), new_type, h);
local2href.insert(mlocal_name(h), href);
}
}
expr new_target = normalize(to_blast_expr(g.get_type()));
s.set_target(new_target);

12
src/library/kernel_serializer.cpp
View file

@ -118,6 +118,7 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
serializer & operator<<(serializer & s, binder_info const & i) {
unsigned w =
(i.is_rec() ? 16 : 0) +
(i.is_implicit() ? 8 : 0) +
(i.is_contextual() ? 4 : 0) +
(i.is_strict_implicit() ? 2 : 0) +
@ -128,11 +129,12 @@ serializer & operator<<(serializer & s, binder_info const & i) {
static binder_info read_binder_info(deserializer & d) {
unsigned w = d.read_char();
bool imp = (w & 8) != 0;
bool ctx = (w & 4) != 0;
bool s_imp = (w & 2) != 0;
bool i_imp = (w & 1) != 0;
return binder_info(imp, ctx, s_imp, i_imp);
bool rec = (w & 16) != 0;
bool imp = (w & 8) != 0;
bool ctx = (w & 4) != 0;
bool s_imp = (w & 2) != 0;
bool i_imp = (w & 1) != 0;
return binder_info(imp, ctx, s_imp, i_imp, rec);
}
static name * g_binder_name = nullptr;

12
tests/lean/run/blast_rec_eq.lean Normal file
View file

@ -0,0 +1,12 @@
open nat
lemma addz [simp] : ∀ a : nat, a + 0 = a := sorry
lemma zadd [simp] : ∀ a : nat, 0 + a = a := sorry
lemma adds [simp] : ∀ a b : nat, a + succ b = succ (a + b) := sorry
lemma sadd [simp] : ∀ a b : nat, succ a + b = succ (a + b) := sorry
definition comm : ∀ a b : nat, a + b = b + a
| a 0 := by simp
| a (succ n) :=
assert a + n = n + a, from !comm,
by simp