diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 11ad170ad..99c303360 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp - gexpr.cpp revert.cpp) + gexpr.cpp revert.cpp subst.cpp) diff --git a/src/library/blast/intros.cpp b/src/library/blast/intros.cpp index 21574a994..1935c059e 100644 --- a/src/library/blast/intros.cpp +++ b/src/library/blast/intros.cpp @@ -16,7 +16,7 @@ struct intros_proof_step_cell : public proof_step_cell { list m_new_hs; virtual ~intros_proof_step_cell() {} 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)); + expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, pr); return action_result::solved(new_pr); } diff --git a/src/library/blast/revert.cpp b/src/library/blast/revert.cpp index 936440980..7444a5acf 100644 --- a/src/library/blast/revert.cpp +++ b/src/library/blast/revert.cpp @@ -23,7 +23,7 @@ struct revert_proof_step_cell : public proof_step_cell { virtual bool is_silent() const override { return true; } }; -unsigned revert(buffer & hidxs, hypothesis_idx_set & hidxs_set) { +unsigned revert_action(buffer & hidxs, hypothesis_idx_set & hidxs_set) { lean_assert(hidxs.size() == hidxs_set.size()); state & s = curr_state(); unsigned hidxs_size = hidxs.size(); @@ -41,8 +41,8 @@ unsigned revert(buffer & hidxs, hypothesis_idx_set & hidxs_set) return hidxs.size(); } -unsigned revert(buffer & hidxs) { +unsigned revert_action(buffer & hidxs) { hypothesis_idx_set hidxs_set(hidxs); - return revert(hidxs, hidxs_set); + return revert_action(hidxs, hidxs_set); } }} diff --git a/src/library/blast/revert.h b/src/library/blast/revert.h index e55e540b1..5440f09d4 100644 --- a/src/library/blast/revert.h +++ b/src/library/blast/revert.h @@ -11,5 +11,9 @@ namespace lean { namespace blast { /** \brief Revert the given hypotheses and their dependencies. Return the total number of hypotheses reverted. */ -unsigned revert(buffer & hidxs); +unsigned revert_action(buffer & hidxs); + +/** \brief Lower-level version of previous procedure. + \pre hidxs and hidxs_set contain the same elements. */ +unsigned revert_action(buffer & hidxs, hypothesis_idx_set & hidxs_set); }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 185e90c8b..73d2d6e4d 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -8,7 +8,9 @@ Author: Leonardo de Moura #include "library/blast/options.h" #include "library/blast/choice_point.h" #include "library/blast/simple_actions.h" +#include "library/blast/proof_expr.h" #include "library/blast/intros.h" +#include "library/blast/subst.h" #include "library/blast/backward.h" namespace lean { @@ -59,6 +61,9 @@ class simple_strategy { display_action("assumption-contradiction"); return action_result::solved(*pr); } + if (subst_action(*hidx)) { + display_action("subst"); + } return action_result::new_branch(); } @@ -84,7 +89,7 @@ class simple_strategy { action_result next_branch(expr pr) { while (curr_state().has_proof_steps()) { proof_step s = curr_state().top_proof_step(); - action_result r = s.resolve(pr); + action_result r = s.resolve(unfold_hypotheses_ge(curr_state(), pr)); switch (r.get_kind()) { case action_result::Failed: display_msg(">>> next-branch FAILED <<<"); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index f479a93b3..59ff065fb 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -263,6 +263,10 @@ public: /** \brief Return the set of hypotheses that (directly) depend on the given one */ hypothesis_idx_set get_forward_deps(hypothesis_idx hidx) const; + template + void for_each_forward_dep(hypothesis_idx hidx, F && f) const { + get_forward_deps(hidx).for_each(f); + } /************************ Abstracting hypotheses diff --git a/src/library/blast/subst.cpp b/src/library/blast/subst.cpp new file mode 100644 index 000000000..dc8d0edff --- /dev/null +++ b/src/library/blast/subst.cpp @@ -0,0 +1,117 @@ +/* +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/abstract.h" +#include "kernel/instantiate.h" +#include "library/blast/revert.h" +#include "library/blast/intros.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +struct subst_proof_step_cell : public proof_step_cell { + expr m_target; + expr m_eq_href; + expr m_rhs; + bool m_dep; + subst_proof_step_cell(expr const & t, expr const & e, expr const & r, bool d): + m_target(t), m_eq_href(e), m_rhs(r), m_dep(d) {} + virtual ~subst_proof_step_cell() {} + + virtual action_result resolve(expr const & pr) const { + try { + state & s = curr_state(); + app_builder & b = get_app_builder(); + if (m_dep) { + buffer hs; + hs.push_back(m_rhs); + hs.push_back(m_eq_href); + expr motive = s.mk_lambda(hs, m_target); + return action_result::solved(b.mk_eq_drec(motive, pr, m_eq_href)); + } else { + expr motive = s.mk_lambda(m_rhs, m_target); + return action_result::solved(b.mk_eq_rec(motive, pr, m_eq_href)); + } + } catch (app_builder &) { + return action_result::failed(); + } + } +}; + +bool subst_core(hypothesis_idx hidx) { + state & s = curr_state(); + state saved = s; + app_builder & b = get_app_builder(); + hypothesis const * h = s.get_hypothesis_decl(hidx); + lean_assert(h); + expr type = h->get_type(); + expr lhs, rhs; + lean_verify(is_eq(type, lhs, rhs)); + lean_assert(is_href(rhs)); + try { + hypothesis_idx_buffer to_revert; + s.for_each_forward_dep(href_index(rhs), + [&](hypothesis_idx d) { + if (d != hidx) to_revert.push_back(d); + }); + s.for_each_forward_dep(hidx, + [&](hypothesis_idx d) { to_revert.push_back(d); }); + unsigned num = revert_action(to_revert); + expr target = s.get_target(); + expr new_target = abstract(target, h->get_self()); + bool dep = !closed(new_target); + if (dep) + new_target = instantiate(new_target, b.mk_eq_refl(lhs)); + new_target = instantiate(abstract(new_target, rhs), lhs); + s.push_proof_step(new subst_proof_step_cell(target, h->get_self(), rhs, dep)); + s.set_target(new_target); + lean_verify(intros_action(num)); + lean_verify(s.del_hypothesis(hidx)); + lean_verify(s.del_hypothesis(href_index(rhs))); + return true; + } catch (app_builder_exception &) { + s = saved; + return false; + } +} + +bool subst_action(hypothesis_idx hidx) { + state & s = curr_state(); + app_builder & b = get_app_builder(); + hypothesis const * h = s.get_hypothesis_decl(hidx); + lean_assert(h); + expr type = h->get_type(); + expr lhs, rhs; + if (!is_eq(type, lhs, rhs)) + return false; + if (is_href(rhs)) { + return subst_core(hidx); + } else if (is_href(lhs)) { + if (!s.get_forward_deps(href_index(lhs)).empty()) { + // TODO(Leo): we don't handle this case yet. + // Other hypotheses depend on this equality. + return false; + } + state saved = s; + try { + expr new_eq = b.mk_eq(rhs, lhs); + expr new_pr = b.mk_eq_symm(h->get_self()); + expr new_href = s.mk_hypothesis(new_eq, new_pr); + if (subst_core(href_index(new_href))) { + return true; + } else { + s = saved; + return false; + } + } catch (app_builder_exception &) { + s = saved; + return false; + } + } else { + return false; + } +} +}} diff --git a/src/library/blast/subst.h b/src/library/blast/subst.h new file mode 100644 index 000000000..d0d79ac91 --- /dev/null +++ b/src/library/blast/subst.h @@ -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/hypothesis.h" +namespace lean { +namespace blast { +/** \brief If the given hypothesis is of the form (H : t = x) or (H : x = s), then + eliminate x (and H). Return true if success. */ +bool subst_action(hypothesis_idx hidx); +}}