From 0f4e59a84faaffcc13ee65dbb6da3ded3522d3c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 18:19:05 -0800 Subject: [PATCH] feat(library/blast): add "no_confusion" action --- src/library/blast/CMakeLists.txt | 2 +- src/library/blast/no_confusion.cpp | 105 ++++++++++++++++++++++++++ src/library/blast/no_confusion.h | 14 ++++ src/library/blast/simple_strategy.cpp | 7 ++ src/library/blast/state.h | 5 ++ src/library/blast/subst.cpp | 2 +- tests/lean/run/blast8.lean | 23 ++++++ tests/lean/run/blast9.lean | 11 +++ 8 files changed, 167 insertions(+), 2 deletions(-) create mode 100644 src/library/blast/no_confusion.cpp create mode 100644 src/library/blast/no_confusion.h create mode 100644 tests/lean/run/blast8.lean create mode 100644 tests/lean/run/blast9.lean diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 99c303360..b6e256056 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 subst.cpp) + gexpr.cpp revert.cpp subst.cpp no_confusion.cpp) diff --git a/src/library/blast/no_confusion.cpp b/src/library/blast/no_confusion.cpp new file mode 100644 index 000000000..f9fa6b148 --- /dev/null +++ b/src/library/blast/no_confusion.cpp @@ -0,0 +1,105 @@ +/* +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/inductive/inductive.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +struct no_confusion_proof_step_cell : public proof_step_cell { + name m_I_name; + expr m_target; + expr m_eq_href; + unsigned m_num_new_eqs; + no_confusion_proof_step_cell(name const & I_name, expr const & t, expr const & e, unsigned n): + m_I_name(I_name), m_target(t), m_eq_href(e), m_num_new_eqs(n) {} + virtual ~no_confusion_proof_step_cell() {} + + virtual action_result resolve(expr const & pr) const { + try { + expr it = pr; + bool skip = true; + for (unsigned i = 0; i < m_num_new_eqs; i++) { + if (!is_lambda(it)) { + break; + skip = false; + } + it = binding_body(it); + } + if (skip && closed(it)) { + // new eq hypotheses were not used + return action_result::solved(it); + } + state & s = curr_state(); + app_builder & b = get_app_builder(); + hypothesis const * h = s.get_hypothesis_decl(href_index(m_eq_href)); + lean_assert(h); + expr type = h->get_type(); + expr lhs, rhs; + lean_verify(is_eq(type, lhs, rhs)); + name nc_name(m_I_name, "no_confusion"); + expr new_pr = mk_app(b.mk_app(nc_name, {m_target, lhs, rhs, m_eq_href}), pr); + return action_result::solved(new_pr); + } catch (app_builder_exception &) { + return action_result::failed(); + } + } +}; + +action_result no_confusion_action(hypothesis_idx hidx) { + try { + 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 action_result::failed(); + lhs = whnf(lhs); + rhs = whnf(rhs); + optional c1 = is_constructor_app(env(), lhs); + optional c2 = is_constructor_app(env(), rhs); + if (!c1 || !c2) + return action_result::failed(); + expr A = whnf(infer_type(lhs)); + expr I = get_app_fn(A); + if (!is_constant(I) || !inductive::is_inductive_decl(env(), const_name(I))) + return action_result::failed(); + name nct_name(const_name(I), "no_confusion_type"); + if (!env().find(nct_name)) + return action_result::failed(); + expr target = s.get_target(); + expr nct = whnf(b.mk_app(nct_name, target, lhs, rhs)); + if (c1 == c2) { + if (!is_pi(nct)) + return action_result::failed(); + if (s.has_target_forward_deps(hidx)) { + // TODO(Leo): we currently do not handle this case. + // To avoid non-termination we remove the given hypothesis, if there + // forward dependencies, we would also have to remove them. + // Remark: this is a low priority refinement since it will not happen + // very often in practice. + return action_result::failed(); + } + unsigned num_params = *inductive::get_num_params(env(), const_name(I)); + unsigned cnstr_arity = get_arity(env().get(*c1).get_type()); + lean_assert(cnstr_arity >= num_params); + unsigned num_new_eqs = cnstr_arity - num_params; + s.push_proof_step(new no_confusion_proof_step_cell(const_name(I), target, h->get_self(), num_new_eqs)); + s.set_target(binding_domain(nct)); + s.del_hypothesis(hidx); + return action_result::new_branch(); + } else { + name nc_name(const_name(I), "no_confusion"); + expr pr = b.mk_app(nc_name, {target, lhs, rhs, h->get_self()}); + return action_result::solved(pr); + } + } catch (app_builder_exception &) { + return action_result::failed(); + } +} +}} diff --git a/src/library/blast/no_confusion.h b/src/library/blast/no_confusion.h new file mode 100644 index 000000000..c2c3eed3a --- /dev/null +++ b/src/library/blast/no_confusion.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/action_result.h" +#include "library/blast/hypothesis.h" + +namespace lean { +namespace blast { +action_result no_confusion_action(hypothesis_idx hidx); +}} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 2b9832023..9a63fedc4 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/blast/intros.h" #include "library/blast/subst.h" #include "library/blast/backward.h" +#include "library/blast/no_confusion.h" namespace lean { namespace blast { @@ -65,6 +66,12 @@ class simple_strategy { } if (subst_action(*hidx)) { display_action("subst"); + return action_result::new_branch(); + } + action_result r = no_confusion_action(*hidx); + if (!failed(r)) { + display_action("no_confusion"); + return r; } return action_result::new_branch(); } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 5c89864e4..8123b0c2a 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -221,6 +221,11 @@ public: /** \brief Return the set of hypotheses that (directly) depend on the given one */ hypothesis_idx_set get_direct_forward_deps(hypothesis_idx hidx) const; + bool has_forward_deps(hypothesis_idx hidx) const { return !get_direct_forward_deps(hidx).empty(); } + /** \brief Return true iff other hypotheses or the target type depends on hidx. */ + bool has_target_forward_deps(hypothesis_idx hidx) const { + return has_forward_deps(hidx) || m_branch.m_target_deps.contains(hidx); + } /** \brief Collect in \c result the hypotheses that (directly) depend on \c hidx and satisfy \c pred. */ template void collect_direct_forward_deps(hypothesis_idx hidx, hypothesis_idx_buffer_set & result, P && pred) { diff --git a/src/library/blast/subst.cpp b/src/library/blast/subst.cpp index c7b794466..574a4e3dc 100644 --- a/src/library/blast/subst.cpp +++ b/src/library/blast/subst.cpp @@ -96,7 +96,7 @@ bool subst_action(hypothesis_idx hidx) { if (is_href(rhs)) { return subst_core(hidx); } else if (is_href(lhs)) { - if (!s.get_direct_forward_deps(href_index(lhs)).empty()) { + if (s.has_forward_deps(href_index(lhs))) { // TODO(Leo): we don't handle this case yet. // Other hypotheses depend on this equality. return false; diff --git a/tests/lean/run/blast8.lean b/tests/lean/run/blast8.lean new file mode 100644 index 000000000..0d311deb3 --- /dev/null +++ b/tests/lean/run/blast8.lean @@ -0,0 +1,23 @@ +open nat +set_option blast.init_depth 10 +set_option blast.max_depth 10 + +lemma l1 (a : nat) : zero = succ a → a = a → false := +by blast + +lemma l2 (p : Prop) (a : nat) : zero = succ a → a = a → p := +by blast + +lemma l3 (a b : nat) : succ (succ a) = succ (succ b) → a = b := +by blast + +lemma l4 (a b : nat) : succ a = succ b → a = b := +by blast + +lemma l5 (a b c : nat) : succ (succ a) = succ (succ b) → c = c := +by blast + +reveal l3 l4 l5 +print l3 +print l4 +print l5 diff --git a/tests/lean/run/blast9.lean b/tests/lean/run/blast9.lean new file mode 100644 index 000000000..652239b0c --- /dev/null +++ b/tests/lean/run/blast9.lean @@ -0,0 +1,11 @@ +import data.list +open list + +example (p : Prop) (a b c : nat) : [a, b, c] = [] → p := +by blast + +lemma l1 (a b c d e f : nat) : [a, b, c] = [d, e, f] → a = d ∧ b = e ∧ c = f := +by blast + +reveal l1 +print l1