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

feat(library/blast): major reorg and basic backward chaining action

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-10 16:57:57 -08:00
parent 5be1893d98
commit f8f3f9402e
10 changed files with 335 additions and 100 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
init_module.cpp simplifier.cpp assumption.cpp intros.cpp proof_expr.cpp
options.cpp choice_point.cpp simple_strategy.cpp)
options.cpp choice_point.cpp simple_strategy.cpp backward.cpp)

148
src/library/blast/backward.cpp Normal file
View file

@ -0,0 +1,148 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/blast/blast.h"
#include "library/blast/proof_expr.h"
#include "library/blast/choice_point.h"
namespace lean {
namespace blast {
struct backward_proof_step_cell : public proof_step_cell {
branch m_branch;
expr m_proof;
list<expr> m_mvars;
backward_proof_step_cell(branch const & b, expr const & pr, list<expr> const & mvars):
m_branch(b), m_proof(pr), m_mvars(mvars) {
lean_assert(!empty(m_mvars));
}
virtual ~backward_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const {
state & s = curr_state();
s.set_branch(m_branch);
expr mvar = head(m_mvars);
if (!is_def_eq(mvar, pr))
return action_result::failed();
list<expr> new_mvars = tail(m_mvars);
if (empty(new_mvars)) {
// solved all branches
expr r = to_proof_expr(s.instantiate_urefs_mrefs(m_proof));
r = unfold_hypotheses_ge(s, r);
return action_result::solved(r);
} else {
s.pop_proof_step();
auto bcell = new backward_proof_step_cell(m_branch, m_proof, new_mvars);
s.push_proof_step(bcell);
expr new_target = s.instantiate_urefs_mrefs(infer_type(head(new_mvars)));
s.set_target(new_target);
return action_result::new_branch();
}
}
};
static action_result try_lemma(name const & fname, bool prop_only_branches) {
state & s = curr_state();
declaration const & fdecl = env().get(fname);
buffer<level> ls_buffer;
unsigned num_univ_ps = fdecl.get_num_univ_params();
for (unsigned i = 0; i < num_univ_ps; i++)
ls_buffer.push_back(mk_fresh_uref());
levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
expr f = mk_constant(fname, ls);
expr type = instantiate_type_univ_params(fdecl, ls);
expr pr = f;
buffer<expr> mvars;
while (true) {
type = whnf(type);
if (!is_pi(type))
break;
expr mvar = s.mk_metavar(binding_domain(type));
mvars.push_back(mvar);
pr = mk_app(pr, mvar);
type = instantiate(binding_body(type), mvar);
}
expr target = s.get_target();
if (!is_def_eq(target, type))
return action_result::failed();
bool has_unassigned = false;
buffer<expr> branches;
unsigned i = mvars.size();
while (i > 0) {
--i;
if (!s.is_mref_assigned(mvars[i])) {
has_unassigned = true;
if (!prop_only_branches || is_prop(infer_type(mvars[i]))) {
branches.push_back(mvars[i]);
}
}
}
if (!has_unassigned) {
// all meta-variables have been assigned
return action_result::solved(to_proof_expr(s.instantiate_urefs_mrefs(pr)));
}
if (branches.empty()) {
// some meta-variables were not assigned, but they are not propositions,
// and since prop_only_branches == true, we only create branches for propositions
return action_result::failed();
}
auto bcell = new backward_proof_step_cell(s.get_branch(), pr, to_list(branches));
s.push_proof_step(bcell);
expr new_target = s.instantiate_urefs_mrefs(infer_type(branches[0]));
s.set_target(new_target);
return action_result::new_branch();
}
class backward_choice_point_cell : public choice_point_cell {
state m_state;
list<name> m_fnames;
bool m_prop_only;
public:
backward_choice_point_cell(state const & s, list<name> const & fnames, bool prop_only):
m_state(s), m_fnames(fnames), m_prop_only(prop_only) {}
virtual action_result next() {
while (!empty(m_fnames)) {
curr_state() = m_state;
name fname = head(m_fnames);
m_fnames = tail(m_fnames);
action_result r = try_lemma(fname, m_prop_only);
if (!failed(r))
return r;
}
return action_result::failed();
}
};
action_result backward_action(list<name> const & fnames, bool prop_only_branches) {
state s = curr_state();
auto it = fnames;
while (!empty(it)) {
action_result r = try_lemma(head(it), prop_only_branches);
it = tail(it);
if (!failed(r)) {
// create choice point
if (!empty(it))
push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches)));
return r;
}
curr_state() = s;
}
return action_result::failed();
}
action_result constructor_action(bool prop_only_branches) {
state s = curr_state();
expr I = get_app_fn(s.get_target());
if (!is_constant(I) || !inductive::is_inductive_decl(env(), const_name(I)))
return action_result::failed();
buffer<name> c_names;
get_intro_rule_names(env(), const_name(I), c_names);
return backward_action(to_list(c_names), prop_only_branches);
}
}}

14
src/library/blast/backward.h Normal file
View file

@ -0,0 +1,14 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/blast/action_result.h"
namespace lean {
namespace blast {
action_result backward_action(list<name> const & fnames, bool prop_only_branches = true);
action_result constructor_action(bool prop_only_branches = true);
}}

11
src/library/blast/choice_point.cpp
View file

@ -20,15 +20,14 @@ void push_choice_point(choice_point const & c) {
get_choice_points().push_back(c);
}
bool next_choice_point() {
action_result next_choice_point() {
auto & cs = get_choice_points();
while (true) {
if (cs.empty())
return false;
if (auto r = cs.back().next()) {
curr_state() = *r;
return true;
}
return action_result::failed();
action_result r = cs.back().next();
if (!failed(r))
return r;
cs.pop_back();
}
}

16
src/library/blast/choice_point.h
View file

@ -20,11 +20,11 @@ class choice_point_cell {
MK_LEAN_RC(); // Declare m_rc counter
void dealloc() { delete this; }
public:
virtual ~choice_point_cell();
/** \brief Return the next proof state. This method may
virtual ~choice_point_cell() {}
/** \brief Update next proof state. This method may
perform destructive updates, choice points are not shared
objects. */
virtual optional<state> next() = 0;
virtual action_result next() = 0;
};
/** \brief Smart pointer for choice points */
@ -39,7 +39,7 @@ public:
choice_point & operator=(choice_point const & s) { LEAN_COPY_REF(s); }
choice_point & operator=(choice_point && s) { LEAN_MOVE_REF(s); }
optional<state> next() {
action_result next() {
lean_assert(m_ptr);
return m_ptr->next();
}
@ -49,9 +49,11 @@ public:
void init_choice_points();
/** \brief Add choice point to the top of the stack */
void push_choice_point(choice_point const & c);
/** \brief If there is another choice point, then update the current state and return true.
Otherwise, return false. */
bool next_choice_point();
inline void push_choice_point(choice_point_cell * cell) {
push_choice_point(choice_point(cell));
}
/** \brief Keep executing choice points until one of them doesn't fail. */
action_result next_choice_point();
/** \brief Return size of the choice point stack */
unsigned get_num_choice_points();
/** \brief Shrink the size of the choice point stack.

8
src/library/blast/intros.cpp
View file

@ -14,9 +14,9 @@ namespace blast {
struct intros_proof_step_cell : public proof_step_cell {
list<expr> m_new_hs;
virtual ~intros_proof_step_cell() {}
virtual optional<expr> resolve(state & s, expr const & pr) const {
expr new_pr = mk_proof_lambda(s, m_new_hs, unfold_hypotheses_ge(s, pr));
return some_expr(new_pr);
virtual action_result resolve(expr const & pr) const {
expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, unfold_hypotheses_ge(curr_state(), pr));
return action_result::solved(new_pr);
}
};
@ -26,7 +26,7 @@ bool intros_action() {
if (!is_pi(target))
return false;
auto pcell = new intros_proof_step_cell();
s.push_proof_step(proof_step(pcell));
s.push_proof_step(pcell);
buffer<expr> new_hs;
while (is_pi(target)) {
expr href = s.mk_hypothesis(binding_name(target), binding_domain(target));

82
src/library/blast/simple_strategy.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "library/blast/choice_point.h"
#include "library/blast/assumption.h"
#include "library/blast/intros.h"
#include "library/blast/backward.h"
namespace lean {
namespace blast {
@ -25,52 +26,66 @@ class simple_strategy {
return curr_state().activate_hypothesis();
}
pair<status, expr> next_action() {
if (intros_action()) {
return mk_pair(Continue, expr());
} else if (activate_hypothesis()) {
action_result next_action() {
if (intros_action())
return action_result::new_branch();
if (activate_hypothesis()) {
// TODO(Leo): we should probably eagerly simplify the activated hypothesis.
return mk_pair(Continue, expr());
} else if (auto pr = assumption_action()) {
return mk_pair(ClosedBranch, *pr);
} else {
// TODO(Leo): add more actions...
return mk_pair(NoAction, expr());
return action_result::new_branch();
}
if (auto pr = assumption_action()) {
return action_result::solved(*pr);
}
action_result r = constructor_action();
if (!failed(r)) return r;
// TODO(Leo): add more actions...
return action_result::failed();
}
optional<expr> resolve(expr pr) {
action_result next_branch(expr pr) {
while (curr_state().has_proof_steps()) {
proof_step s = curr_state().top_proof_step();
if (auto new_pr = s.resolve(curr_state(), pr)) {
pr = *new_pr;
proof_step s = curr_state().top_proof_step();
action_result r = s.resolve(pr);
switch (r.get_kind()) {
case action_result::Failed:
return r;
case action_result::Solved:
pr = r.get_proof();
curr_state().pop_proof_step();
} else {
return none_expr(); // continue the search
break;
case action_result::NewBranch:
return action_result::new_branch();
}
}
return some_expr(pr); // closed all branches
return action_result::solved(pr);
}
optional<expr> search_upto(unsigned depth) {
action_result r = next_action();
while (true) {
if (curr_state().get_proof_depth() > depth) {
// maximum depth reached
if (!next_choice_point()) {
if (curr_state().get_proof_depth() > depth)
r = action_result::failed();
switch (r.get_kind()) {
case action_result::Failed:
r = next_choice_point();
if (failed(r)) {
// all choice points failed...
return none_expr();
}
}
auto s = next_action();
switch (s.first) {
case NoAction:
if (!next_choice_point())
return none_expr();
break;
case ClosedBranch:
if (auto pr = resolve(s.second))
return pr;
case action_result::Solved:
r = next_branch(r.get_proof());
if (r.get_kind() == action_result::Solved) {
// all branches have been solved
return some_expr(r.get_proof());
}
break;
case Continue:
case action_result::NewBranch:
r = next_action();
break;
}
}
@ -79,14 +94,17 @@ class simple_strategy {
optional<expr> search() {
state s = curr_state();
unsigned d = m_init_depth;
while (d <= m_max_depth) {
while (true) {
if (auto r = search_upto(d))
return r;
d += m_inc_depth;
if (d > m_max_depth) {
display_curr_state();
return none_expr();
}
curr_state() = s;
clear_choice_points();
}
return none_expr();
}
public:

32
src/library/blast/state.cpp
View file

@ -369,23 +369,23 @@ struct hypothesis_dep_depth_lt {
};
void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) {
m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) {
r.push_back(hidx);
});
std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this));
}
void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
if (auto s = m_forward_deps.find(hidx_provider)) {
if (auto s = m_branch.m_forward_deps.find(hidx_provider)) {
if (!s->contains(hidx_user)) {
hypothesis_idx_set new_s(*s);
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
m_branch.m_forward_deps.insert(hidx_provider, new_s);
}
} else {
hypothesis_idx_set new_s;
new_s.insert(hidx_user);
m_forward_deps.insert(hidx_provider, new_s);
m_branch.m_forward_deps.insert(hidx_provider, new_s);
}
}
@ -407,7 +407,7 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
}
return false;
} else if (is_mref(l)) {
m_mvar_idxs.insert(mref_index(l));
m_branch.m_mvar_idxs.insert(mref_index(l));
return false;
} else {
return true;
@ -436,11 +436,11 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type,
new_h.m_self = r;
new_h.m_proof_depth = m_proof_depth;
add_deps(new_h, new_hidx);
m_hyp_decls.insert(new_hidx, new_h);
m_branch.m_hyp_decls.insert(new_hidx, new_h);
if (new_h.is_assumption())
m_assumption.insert(new_hidx);
m_branch.m_assumption.insert(new_hidx);
double w = compute_weight(new_hidx, type);
m_todo_queue.insert(w, new_hidx);
m_branch.m_todo_queue.insert(w, new_hidx);
return r;
}
@ -468,18 +468,18 @@ void state::update_indices(unsigned /* hidx */) {
}
optional<unsigned> state::activate_hypothesis() {
if (m_todo_queue.empty()) {
if (m_branch.m_todo_queue.empty()) {
return optional<unsigned>();
} else {
unsigned hidx = m_todo_queue.erase_min();
m_active.insert(hidx);
unsigned hidx = m_branch.m_todo_queue.erase_min();
m_branch.m_active.insert(hidx);
update_indices(hidx);
return optional<unsigned>(hidx);
}
}
bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
if (auto s = m_forward_deps.find(hidx_provider)) {
if (auto s = m_branch.m_forward_deps.find(hidx_provider)) {
return s->contains(hidx_user);
} else {
return false;
@ -487,17 +487,17 @@ bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
}
void state::set_target(expr const & t) {
m_target = t;
m_target_deps.clear();
m_branch.m_target = t;
m_branch.m_target_deps.clear();
if (has_href(t) || has_mref(t)) {
for_each(t, [&](expr const & e, unsigned) {
if (!has_href(e) && !has_mref(e)) {
return false;
} else if (is_href(e)) {
m_target_deps.insert(href_index(e));
m_branch.m_target_deps.insert(href_index(e));
return false;
} else if (is_mref(e)) {
m_mvar_idxs.insert(mref_index(e));
m_branch.m_mvar_idxs.insert(mref_index(e));
return false;
} else {
return true;

87
src/library/blast/state.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "util/rb_map.h"
#include "kernel/expr.h"
#include "library/tactic/goal.h"
#include "library/blast/action_result.h"
#include "library/blast/hypothesis.h"
namespace lean {
@ -44,15 +45,16 @@ public:
virtual ~proof_step_cell() {}
/** \brief Every proof-step must provide a resolve method.
When the branch created by the proof-step is closed,
a proof pr is provided, and the proof-step can perform two operations
1- setup the next branch and return none_expr
2- finish and return a new proof
a proof pr is provided, and the proof-step can:
1- setup the next branch, or
2- fail, or
3- finish and return a new proof
\remark Proof steps may be shared, i.e., they may ocurren the
proof-step stack of different proof state objects.
So, resolve must not perform destructive updates.
This is why we marked it as const. */
virtual optional<expr> resolve(state & s, expr const & pr) const = 0;
virtual action_result resolve(expr const & pr) const = 0;
};
/** \brief Smart pointer for proof steps */
@ -67,35 +69,18 @@ public:
proof_step & operator=(proof_step const & s) { LEAN_COPY_REF(s); }
proof_step & operator=(proof_step && s) { LEAN_MOVE_REF(s); }
optional<expr> resolve(state & s, expr const & pr) const {
action_result resolve(expr const & pr) const {
lean_assert(m_ptr);
return m_ptr->resolve(s, pr);
return m_ptr->resolve(pr);
}
};
/** \brief Proof state for the blast tactic */
class state {
/** \brief Information associated with the current branch of the proof state.
This is essentially a mechanism for creating snapshots of the current branch. */
class branch {
friend class state;
typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
typedef rb_map<double, unsigned, double_cmp> todo_queue;
typedef metavar_idx_map<metavar_decl> metavar_decls;
typedef metavar_idx_map<expr> eassignment;
typedef metavar_idx_map<level> uassignment;
typedef hypothesis_idx_map<metavar_idx_set> fixed_by;
typedef list<proof_step> proof_steps;
uassignment m_uassignment;
metavar_decls m_metavar_decls;
eassignment m_eassignment;
// In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared
// in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them.
// That is, to be able to clear `h` in a branch `B`, we first need to check whether it
// is contained in this mapping or not. If it is, we should check whether any of the
// metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since
// `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs).
// If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still
// non-empty, then we cannot clear `h`.
fixed_by m_fixed_by;
unsigned m_proof_depth{0};
proof_steps m_proof_steps;
// Hypothesis/facts in the current state
hypothesis_decls m_hyp_decls;
// We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint:
@ -119,6 +104,30 @@ class state {
expr m_target;
hypothesis_idx_set m_target_deps;
metavar_idx_set m_mvar_idxs;
};
/** \brief Proof state for the blast tactic */
class state {
typedef metavar_idx_map<metavar_decl> metavar_decls;
typedef metavar_idx_map<expr> eassignment;
typedef metavar_idx_map<level> uassignment;
typedef hypothesis_idx_map<metavar_idx_set> fixed_by;
typedef list<proof_step> proof_steps;
uassignment m_uassignment;
metavar_decls m_metavar_decls;
eassignment m_eassignment;
// In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared
// in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them.
// That is, to be able to clear `h` in a branch `B`, we first need to check whether it
// is contained in this mapping or not. If it is, we should check whether any of the
// metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since
// `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs).
// If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still
// non-empty, then we cannot clear `h`.
fixed_by m_fixed_by;
unsigned m_proof_depth{0};
proof_steps m_proof_steps;
branch m_branch;
void add_forward_dep(unsigned hidx_user, unsigned hidx_provider);
void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user);
@ -164,7 +173,13 @@ public:
metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); }
metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); }
bool has_mvar(expr const & e) const { return m_branch.m_mvar_idxs.contains(mref_index(e)); }
/************************
Save/Restore branch
*************************/
branch const & get_branch() const { return m_branch; }
void set_branch(branch const & b) { m_branch = b; }
/************************
Hypotheses
@ -179,12 +194,12 @@ public:
\c hidx_provider. */
bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const;
hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_hyp_decls.find(hidx); }
hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_branch.m_hyp_decls.find(hidx); }
hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); }
void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_hyp_decls.for_each(fn); }
void for_each_hypothesis(std::function<void(unsigned, hypothesis const &)> const & fn) const { m_branch.m_hyp_decls.for_each(fn); }
optional<unsigned> find_active_hypothesis(std::function<bool(unsigned, hypothesis const &)> const & fn) const { // NOLINT
return m_active.find_if([&](unsigned hidx) {
return m_branch.m_active.find_if([&](unsigned hidx) {
return fn(hidx, *get_hypothesis_decl(hidx));
});
}
@ -197,7 +212,7 @@ public:
expr expand_hrefs(expr const & e, list<expr> const & hrefs) const;
hypothesis_idx_set get_assumptions() const { return m_assumption; }
hypothesis_idx_set get_assumptions() const { return m_branch.m_assumption; }
/************************
Abstracting hypotheses
@ -226,9 +241,9 @@ public:
/** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that
must be synthesize in the current branch) */
void set_target(expr const & t);
expr const & get_target() const { return m_target; }
expr const & get_target() const { return m_branch.m_target; }
/** \brief Return true iff the target depends on the given hypothesis */
bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); }
bool target_depends_on(expr const & h) const { return m_branch.m_target_deps.contains(href_index(h)); }
/************************
Proof steps
@ -239,6 +254,10 @@ public:
m_proof_steps = cons(ps, m_proof_steps);
}
void push_proof_step(proof_step_cell * cell) {
push_proof_step(proof_step(cell));
}
bool has_proof_steps() const {
return static_cast<bool>(m_proof_steps);
}

35
tests/lean/run/blast3.lean Normal file
View file

@ -0,0 +1,35 @@
set_option blast.init_depth 10
example (a b c : Prop) : b → c → b ∧ c :=
by blast
example (a b c : Prop) : b → c → c ∧ b :=
by blast
example (a b : Prop) : a → a ∨ b :=
by blast
example (a b : Prop) : b → a ∨ b :=
by blast
example (a b : Prop) : b → a ∨ a ∨ b :=
by blast
example (a b c : Prop) : b → c → a ∨ a ∨ (b ∧ c) :=
by blast
example (p q : nat → Prop) (a b : nat) : p a → q b → ∃ x, p x :=
by blast
example {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, p x :=
by blast
lemma foo₁ {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, (p x ∧ x = b) ∨ q x :=
by blast
lemma foo₂ {A : Type} (p q : A → Prop) (a b : A) : p b → ∃ x, q x ∨ (p x ∧ x = b) :=
by blast
reveal foo₁ foo₂
print foo₁
print foo₂