From 76cebb45f96e90da9ede88b3d2fa09760c30a205 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jan 2016 17:30:25 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): add support for 'no_confusion' in the congruence closure module --- src/library/blast/congruence_closure.cpp | 74 +++++++++++++++++----- src/library/blast/congruence_closure.h | 5 +- src/library/blast/strategies/portfolio.cpp | 7 +- tests/lean/run/blast_cc_noconfusion.lean | 32 ++++++++++ 4 files changed, 99 insertions(+), 19 deletions(-) create mode 100644 tests/lean/run/blast_cc_noconfusion.lean diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index ae8f3148f4..55c16bbef7 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -100,11 +100,21 @@ scope_congruence_closure::~scope_congruence_closure() { } void congruence_closure::initialize() { - mk_entry_core(get_iff_name(), mk_true(), false, true); - mk_entry_core(get_iff_name(), mk_false(), false, true); + bool propagate_back = false; + bool interpreted = true; + bool constructor = false; + mk_entry_core(get_iff_name(), mk_true(), propagate_back, interpreted, constructor); + mk_entry_core(get_iff_name(), mk_false(), propagate_back, interpreted, constructor); + + /* Put (nat.zero) and (@zero nat nat_has_zero) in the same equivalence class. + TODO(Leo): this is hackish, we should have a more general solution for this kind of equality. */ + app_builder & b = get_app_builder(); + expr nat_zero = mk_constant(get_nat_zero_name()); + expr zero_nat = normalize(b.mk_zero(mk_constant(get_nat_name()))); + add_eqv(get_eq_name(), nat_zero, zero_nat, b.mk_eq_refl(nat_zero)); } -void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted) { +void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted, bool constructor) { lean_assert(!m_entries.find(eqc_key(R, e))); entry n; n.m_next = e; @@ -113,6 +123,7 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p n.m_size = 1; n.m_flipped = false; n.m_interpreted = interpreted; + n.m_constructor = constructor; n.m_to_propagate = to_propagate; n.m_mt = m_gmt; m_entries.insert(eqc_key(R, e), n); @@ -135,6 +146,12 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p } } +void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate) { + bool interpreted = false; + bool constructor = R == get_eq_name() && is_constructor_app(env(), e); + return mk_entry_core(R, e, to_propagate, interpreted, constructor); +} + void congruence_closure::mk_entry(name const & R, expr const & e, bool to_propagate) { if (to_propagate && !is_prop(e)) to_propagate = false; @@ -146,8 +163,7 @@ void congruence_closure::mk_entry(name const & R, expr const & e, bool to_propag } return; } - bool interpreted = false; - mk_entry_core(R, e, to_propagate, interpreted); + mk_entry_core(R, e, to_propagate); } static bool all_distinct(buffer const & es) { @@ -618,15 +634,15 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t return; case expr_kind::Constant: case expr_kind::Local: case expr_kind::Meta: - mk_entry_core(R, e, to_propagate, false); + mk_entry_core(R, e, to_propagate); return; case expr_kind::Lambda: - mk_entry_core(R, e, false, false); + mk_entry_core(R, e, false); return; case expr_kind::Macro: for (unsigned i = 0; i < macro_num_args(e); i++) internalize_core(R, macro_arg(e, i), false, false); - mk_entry_core(R, e, to_propagate, false); + mk_entry_core(R, e, to_propagate); break; case expr_kind::Pi: // TODO(Leo): should we support congruence for arrows? @@ -636,12 +652,12 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t internalize_core(R, binding_body(e), toplevel, to_propagate); } if (is_prop(e)) { - mk_entry_core(R, e, false, false); + mk_entry_core(R, e, false); } return; case expr_kind::App: { bool is_lapp = is_logical_app(e); - mk_entry_core(R, e, to_propagate && !is_lapp, false); + mk_entry_core(R, e, to_propagate && !is_lapp); buffer args; expr const & fn = get_app_args(e, args); if (toplevel) { @@ -757,6 +773,19 @@ static bool is_true_or_false(expr const & e) { return is_constant(e, get_true_name()) || is_constant(e, get_false_name()); } +void congruence_closure::propagate_no_confusion_eq(expr const & e1, expr const & e2) { + lean_assert(is_constructor_app(env(), e1)); + lean_assert(is_constructor_app(env(), e2)); + /* Add equality e1 =?= e2 to set of hypotheses. no_confusion_action will process it */ + app_builder & b = get_app_builder(); + state & s = curr_state(); + expr type = b.mk_eq(e1, e2); + expr pr = *get_eqv_proof(get_eq_name(), e1, e2); + expr H = s.mk_hypothesis(type, pr); + lean_trace(name({"cc", "propagation"}), + tout() << "no confusion eq: " << ppb(H) << " : " << ppb(infer_type(H)) << "\n";); +} + /* Remark: If added_prop is not none, then it contains the proposition provided to ::add. We use it here to avoid an unnecessary propagation back to the current_state. */ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional const & added_prop) { @@ -774,14 +803,18 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con // We want r2 to be the root of the combined class. // We swap (e1,n1,r1) with (e2,n2,r2) when - // 1- is_interpreted(n1->m_root) && !is_interpreted(n2->m_root). + // 1- r1->m_interpreted && !r2->m_interpreted. // Reason: to decide when to propagate we check whether the root of the equivalence class // is true/false. So, this condition is to make sure if true/false is an equivalence class, // then one of them is the root. If both are, it doesn't matter, since the state is inconsistent // anyway. - // 2- r1->m_size > r2->m_size - // Reason: performance. Condition was has precedence - if ((r1->m_size > r2->m_size && !r2->m_interpreted) || r1->m_interpreted) { + // 2- r1->m_constructor && !r2->m_interpreted && !r2->m_constructor + // Reason: we want constructors to be the representative of their equivalence classes. + // 2- r1->m_size > r2->m_size && !r2->m_interpreted && !r2->m_constructor + // Reason: performance. + if ((r1->m_interpreted && !r2->m_interpreted) || + (r1->m_constructor && !r2->m_interpreted && !r2->m_constructor) || + (r1->m_size > r2->m_size && !r2->m_interpreted && !r2->m_constructor)) { std::swap(e1, e2); std::swap(n1, n2); std::swap(r1, r2); @@ -792,6 +825,8 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con if (r1->m_interpreted && r2->m_interpreted) m_inconsistent = true; + bool use_no_confusion = R == get_eq_name() && r1->m_constructor && r2->m_constructor; + expr e1_root = n1->m_root; expr e2_root = n2->m_root; entry new_n1 = *n1; @@ -862,8 +897,9 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con for (name const & R2 : m_non_eq_relations) { if (m_entries.find(eqc_key(R2, e1)) || m_entries.find(eqc_key(R2, e2))) { - mk_entry(R2, e1, false); - mk_entry(R2, e2, false); + bool propagate_back = false; + mk_entry(R2, e1, propagate_back); + mk_entry(R2, e2, propagate_back); push_todo(R2, e1, e2, *g_lift_mark); } } @@ -892,9 +928,13 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con } } + if (use_no_confusion) { + propagate_no_confusion_eq(e1_root, e2_root); + } + update_mt(R, e2_root); - lean_trace(name({"cc", "merge"}), tout() << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";); + lean_trace(name({"cc", "merge"}), tout() << ppb(e1_root) << " [" << R << "] " << ppb(e2_root) << "\n";); lean_trace(name({"cc", "state"}), trace();); } diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h index d09e1829e4..ba0897fa71 100644 --- a/src/library/blast/congruence_closure.h +++ b/src/library/blast/congruence_closure.h @@ -47,6 +47,7 @@ class congruence_closure { unsigned m_flipped:1; // proof has been flipped unsigned m_to_propagate:1; // must be propagated back to state when in equivalence class containing true/false unsigned m_interpreted:1; // true if the node should be viewed as an abstract value + unsigned m_constructor:1; // true if head symbol is a constructor unsigned m_size; // number of elements in the equivalence class, it is meaningless if 'e' != m_root unsigned m_mt; // The field m_mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. @@ -125,7 +126,8 @@ class congruence_closure { congr_key mk_congr_key(ext_congr_lemma const & lemma, expr const & e) const; void check_iff_true(congr_key const & k); - void mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted); + void mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted, bool constructor); + void mk_entry_core(name const & R, expr const & e, bool to_propagate); void mk_entry(name const & R, expr const & e, bool to_propagate); void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child); void add_congruence_table(ext_congr_lemma const & lemma, expr const & e); @@ -138,6 +140,7 @@ class congruence_closure { expr mk_iff_true_intro(expr const & proof); void add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional const & added_prop); void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H, optional const & added_prop); + void propagate_no_confusion_eq(expr const & e1, expr const & e2); expr mk_congr_proof_core(name const & R, expr const & lhs, expr const & rhs) const; expr mk_congr_proof(name const & R, expr const & lhs, expr const & rhs) const; diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp index c3e6ac2360..5ca789c1e5 100644 --- a/src/library/blast/strategies/portfolio.cpp +++ b/src/library/blast/strategies/portfolio.cpp @@ -43,7 +43,12 @@ static optional apply_simple() { static optional apply_cc() { flet set(get_config().m_cc, true); - return mk_pre_action_strategy("cc", assert_cc_action)(); + return mk_pre_action_strategy("cc", + [](hypothesis_idx hidx) { + Try(no_confusion_action(hidx)); + Try(assert_cc_action(hidx)); + return action_result::new_branch(); + })(); } static optional apply_ematch() { diff --git a/tests/lean/run/blast_cc_noconfusion.lean b/tests/lean/run/blast_cc_noconfusion.lean new file mode 100644 index 0000000000..462dc49af3 --- /dev/null +++ b/tests/lean/run/blast_cc_noconfusion.lean @@ -0,0 +1,32 @@ +import data.list +open nat + +constant f : nat → nat + +example (a b c d : nat) : f d = f b → succ a = f b → f d = succ c → a = c := +by blast + +example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = succ c → a = c := +by blast + +example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = zero → false := +by blast + +example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = 0 → false := +by blast + +open list +example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = [c, d, succ e] → l3 = l4 → c = e := +by blast + +example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ (succ c)] → l1 = [c, d, succ (succ e)] → l3 = l4 → l1 = l2 → l2 = l3 → c = e := +by blast + +example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = [c, d, 0] → l3 = l4 → l1 = l2 → l2 = l3 → false := +by blast + +example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = nil → l3 = l4 → l1 = l2 → l2 = l3 → false := +by blast + +example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = nil → l3 = l4 → false := +by blast