From 48cd421852e676a4b28220137a6a4687092bc669 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Dec 2016 20:34:42 -0800 Subject: [PATCH] feat(library/tactic/congruence): add congruence closure basics --- library/init/logic.lean | 5 + library/init/propext.lean | 6 + src/CMakeLists.txt | 2 + src/library/app_builder.cpp | 15 + src/library/app_builder.h | 7 + src/library/constants.cpp | 12 + src/library/constants.h | 3 + src/library/constants.txt | 3 + src/library/tactic/congruence/CMakeLists.txt | 1 + .../tactic/congruence/congruence_closure.cpp | 1076 +++++++++++++++++ .../tactic/congruence/congruence_closure.h | 223 ++++ src/library/util.cpp | 10 +- src/library/util.h | 3 +- 13 files changed, 1362 insertions(+), 4 deletions(-) create mode 100644 src/library/tactic/congruence/CMakeLists.txt create mode 100644 src/library/tactic/congruence/congruence_closure.cpp create mode 100644 src/library/tactic/congruence/congruence_closure.h diff --git a/library/init/logic.lean b/library/init/logic.lean index 2f6c965b3b..00c39f86e7 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -290,6 +290,11 @@ iff.intro iff.symm iff.symm lemma eq.to_iff {a b : Prop} (h : a = b) : a ↔ b := eq.rec_on h iff.rfl +lemma neq_of_not_iff {a b : Prop} : ¬(a ↔ b) → a ≠ b := +λ h₁ h₂, +have a ↔ b, from eq.subst h₂ (iff.refl a), +absurd this h₁ + lemma not_iff_not_of_iff (h₁ : a ↔ b) : ¬a ↔ ¬b := iff.intro (assume (hna : ¬ a) (hb : b), hna (iff.elim_right h₁ hb)) diff --git a/library/init/propext.lean b/library/init/propext.lean index cef8d18894..4c1ace3e12 100644 --- a/library/init/propext.lean +++ b/library/init/propext.lean @@ -19,3 +19,9 @@ propext (imp_congr h₁^.to_iff h₂^.to_iff) lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) := propext (imp_congr_ctx h₁^.to_iff (λ hc, (h₂ hc)^.to_iff)) + +lemma eq_true_intro {a : Prop} (h : a) : a = true := +propext (iff_true_intro h) + +lemma eq_false_intro {a : Prop} (h : ¬a) : a = false := +propext (iff_false_intro h) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3a8d3d0280..a97a5758f9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -342,6 +342,8 @@ add_subdirectory(library/tactic) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic/backward) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/tactic/congruence) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/constructions) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/equations_compiler) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 2ce98cbf1d..2e06bb3177 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -885,6 +885,21 @@ expr mk_iff_true_intro(type_context & ctx, expr const & H) { return mk_app(ctx, get_iff_true_intro_name(), {H}); } +expr mk_eq_false_intro(type_context & ctx, expr const & H) { + // TODO(Leo): implement custom version if bottleneck. + return mk_app(ctx, get_eq_false_intro_name(), {H}); +} + +expr mk_eq_true_intro(type_context & ctx, expr const & H) { + // TODO(Leo): implement custom version if bottleneck. + return mk_app(ctx, get_eq_true_intro_name(), {H}); +} + +expr mk_neq_of_not_iff(type_context & ctx, expr const & H) { + // TODO(Leo): implement custom version if bottleneck. + return mk_app(ctx, get_neq_of_not_iff_name(), {H}); +} + expr mk_not_of_iff_false(type_context & ctx, expr const & H) { if (is_constant(get_app_fn(H), get_iff_false_intro_name())) { // not_of_iff_false (iff_false_intro H) == H diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 3a37b92de0..e5bbfd34dc 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -137,6 +137,13 @@ expr mk_of_iff_true(type_context & ctx, expr const & H); /** \brief (true <-> false) -> false */ expr mk_false_of_true_iff_false(type_context & ctx, expr const & H); +/** \brief not p -> (p = false) */ +expr mk_eq_false_intro(type_context & ctx, expr const & H); +/** \brief p -> (p = true) */ +expr mk_eq_true_intro(type_context & ctx, expr const & H); +/** not(p <-> q) -> not(p = q) */ +expr mk_neq_of_not_iff(type_context & ctx, expr const & H); + expr mk_not(type_context & ctx, expr const & H); expr mk_partial_add(type_context & ctx, expr const & A); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index f1e44adf16..6580a01991 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -71,6 +71,8 @@ name const * g_eq_symm = nullptr; name const * g_eq_trans = nullptr; name const * g_eq_of_heq = nullptr; name const * g_eq_rec_heq = nullptr; +name const * g_eq_true_intro = nullptr; +name const * g_eq_false_intro = nullptr; name const * g_exists_elim = nullptr; name const * g_format = nullptr; name const * g_functor = nullptr; @@ -228,6 +230,7 @@ name const * g_nat_one_lt_bit1 = nullptr; name const * g_nat_le_of_lt = nullptr; name const * g_nat_le_refl = nullptr; name const * g_neg = nullptr; +name const * g_neq_of_not_iff = nullptr; name const * g_norm_num_add1 = nullptr; name const * g_norm_num_add1_bit0 = nullptr; name const * g_norm_num_add1_bit1_helper = nullptr; @@ -498,6 +501,8 @@ void initialize_constants() { g_eq_trans = new name{"eq", "trans"}; g_eq_of_heq = new name{"eq_of_heq"}; g_eq_rec_heq = new name{"eq_rec_heq"}; + g_eq_true_intro = new name{"eq_true_intro"}; + g_eq_false_intro = new name{"eq_false_intro"}; g_exists_elim = new name{"exists", "elim"}; g_format = new name{"format"}; g_functor = new name{"functor"}; @@ -655,6 +660,7 @@ void initialize_constants() { g_nat_le_of_lt = new name{"nat", "le_of_lt"}; g_nat_le_refl = new name{"nat", "le_refl"}; g_neg = new name{"neg"}; + g_neq_of_not_iff = new name{"neq_of_not_iff"}; g_norm_num_add1 = new name{"norm_num", "add1"}; g_norm_num_add1_bit0 = new name{"norm_num", "add1_bit0"}; g_norm_num_add1_bit1_helper = new name{"norm_num", "add1_bit1_helper"}; @@ -926,6 +932,8 @@ void finalize_constants() { delete g_eq_trans; delete g_eq_of_heq; delete g_eq_rec_heq; + delete g_eq_true_intro; + delete g_eq_false_intro; delete g_exists_elim; delete g_format; delete g_functor; @@ -1083,6 +1091,7 @@ void finalize_constants() { delete g_nat_le_of_lt; delete g_nat_le_refl; delete g_neg; + delete g_neq_of_not_iff; delete g_norm_num_add1; delete g_norm_num_add1_bit0; delete g_norm_num_add1_bit1_helper; @@ -1353,6 +1362,8 @@ name const & get_eq_symm_name() { return *g_eq_symm; } name const & get_eq_trans_name() { return *g_eq_trans; } name const & get_eq_of_heq_name() { return *g_eq_of_heq; } name const & get_eq_rec_heq_name() { return *g_eq_rec_heq; } +name const & get_eq_true_intro_name() { return *g_eq_true_intro; } +name const & get_eq_false_intro_name() { return *g_eq_false_intro; } name const & get_exists_elim_name() { return *g_exists_elim; } name const & get_format_name() { return *g_format; } name const & get_functor_name() { return *g_functor; } @@ -1510,6 +1521,7 @@ name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; } name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; } name const & get_nat_le_refl_name() { return *g_nat_le_refl; } name const & get_neg_name() { return *g_neg; } +name const & get_neq_of_not_iff_name() { return *g_neq_of_not_iff; } name const & get_norm_num_add1_name() { return *g_norm_num_add1; } name const & get_norm_num_add1_bit0_name() { return *g_norm_num_add1_bit0; } name const & get_norm_num_add1_bit1_helper_name() { return *g_norm_num_add1_bit1_helper; } diff --git a/src/library/constants.h b/src/library/constants.h index 453da34501..c7be7b0150 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -73,6 +73,8 @@ name const & get_eq_symm_name(); name const & get_eq_trans_name(); name const & get_eq_of_heq_name(); name const & get_eq_rec_heq_name(); +name const & get_eq_true_intro_name(); +name const & get_eq_false_intro_name(); name const & get_exists_elim_name(); name const & get_format_name(); name const & get_functor_name(); @@ -230,6 +232,7 @@ name const & get_nat_one_lt_bit1_name(); name const & get_nat_le_of_lt_name(); name const & get_nat_le_refl_name(); name const & get_neg_name(); +name const & get_neq_of_not_iff_name(); name const & get_norm_num_add1_name(); name const & get_norm_num_add1_bit0_name(); name const & get_norm_num_add1_bit1_helper_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index d660a5a80c..66f31ee9fc 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -66,6 +66,8 @@ eq.symm eq.trans eq_of_heq eq_rec_heq +eq_true_intro +eq_false_intro exists.elim format functor @@ -223,6 +225,7 @@ nat.one_lt_bit1 nat.le_of_lt nat.le_refl neg +neq_of_not_iff norm_num.add1 norm_num.add1_bit0 norm_num.add1_bit1_helper diff --git a/src/library/tactic/congruence/CMakeLists.txt b/src/library/tactic/congruence/CMakeLists.txt new file mode 100644 index 0000000000..3fdabb117d --- /dev/null +++ b/src/library/tactic/congruence/CMakeLists.txt @@ -0,0 +1 @@ +add_library(congruence OBJECT congruence_closure.cpp) diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp new file mode 100644 index 0000000000..a9ae3b5778 --- /dev/null +++ b/src/library/tactic/congruence/congruence_closure.cpp @@ -0,0 +1,1076 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "library/util.h" +#include "library/constants.h" +#include "library/trace.h" +#include "library/app_builder.h" +#include "library/defeq_canonizer.h" +#include "library/tactic/congruence/congruence_closure.h" + +namespace lean { +/* Small hack for not storing a pointer to the congruence_closure object + for congruence_closure::congr_key_cmp */ +LEAN_THREAD_PTR(congruence_closure, g_cc); + +struct congr_lemma_key { + expr m_fn; + unsigned m_nargs; + unsigned m_hash; + congr_lemma_key(expr const & fn, unsigned nargs): + m_fn(fn), m_nargs(nargs), + m_hash(hash(fn.hash(), nargs)) {} +}; + +struct congr_lemma_key_hash_fn { + unsigned operator()(congr_lemma_key const & k) const { return k.m_hash; } +}; + +struct congr_lemma_key_eq_fn { + bool operator()(congr_lemma_key const & k1, congr_lemma_key const & k2) const { + return k1.m_fn == k2.m_fn && k1.m_nargs == k2.m_nargs; + } +}; + +typedef std::unordered_map, congr_lemma_key_hash_fn, congr_lemma_key_eq_fn> congr_lemma_cache_data; + +struct congr_lemma_cache { + environment m_env; + congr_lemma_cache_data m_cache[4]; + + congr_lemma_cache(environment const & env):m_env(env) { + } +}; + +typedef std::shared_ptr congr_lemma_cache_ptr; + +class congr_lemma_cache_manager { + congr_lemma_cache_ptr m_cache_ptr; + unsigned m_reducibility_fingerprint; + environment m_env; + + congr_lemma_cache_ptr release() { + auto c = m_cache_ptr; + m_cache_ptr.reset(); + return c; + } + +public: + congr_lemma_cache_manager() {} + + congr_lemma_cache_ptr mk(environment const & env) { + if (!m_cache_ptr) + return std::make_shared(env); + if (is_eqp(env, m_env)) + return release(); + if (!env.is_descendant(m_env) || + get_reducibility_fingerprint(env) != m_reducibility_fingerprint) + return std::make_shared(env); + m_cache_ptr->m_env = env; + return release(); + } + + void recycle(congr_lemma_cache_ptr const & ptr) { + m_cache_ptr = ptr; + if (!is_eqp(ptr->m_env, m_env)) { + m_env = ptr->m_env; + m_reducibility_fingerprint = get_reducibility_fingerprint(ptr->m_env); + } + } +}; + +MK_THREAD_LOCAL_GET_DEF(congr_lemma_cache_manager, get_clcm); + +congruence_closure::congruence_closure(type_context & ctx, state & s): + m_ctx(ctx), m_state(s), m_cache_ptr(get_clcm().mk(ctx.env())), m_mode(ctx.mode()), + m_rel_info_getter(mk_relation_info_getter(ctx.env())), + m_symm_info_getter(mk_symm_info_getter(ctx.env())) { +} + +congruence_closure::~congruence_closure() { + get_clcm().recycle(m_cache_ptr); +} + +inline congr_lemma_cache_ptr & get_cache_ptr(congruence_closure & cc) { + return cc.m_cache_ptr; +} + +inline congr_lemma_cache_data & get_cache(congruence_closure & cc) { + return get_cache_ptr(cc)->m_cache[static_cast(cc.mode())]; +} + +/* Automatically generated congruence lemma based on heterogeneous equality. */ +static optional mk_hcongr_lemma_core(type_context & ctx, expr const & fn, unsigned nargs) { + optional eq_congr = mk_hcongr(ctx, fn, nargs); + if (!eq_congr) return optional(); + ext_congr_lemma res1(*eq_congr); + expr type = eq_congr->get_type(); + while (is_pi(type)) type = binding_body(type); + /* If all arguments are Eq kind, then we can use generic congr axiom and consider equality for the function. */ + if (!is_heq(type) && eq_congr->all_eq_kind()) + res1.m_fixed_fun = false; + lean_assert(is_eq(type) || is_heq(type)); + res1.m_hcongr_lemma = true; + if (is_heq(type)) + res1.m_heq_result = true; + return optional(res1); +} + +optional congruence_closure::mk_ext_congr_lemma(expr const & e) { + expr const & fn = get_app_fn(e); + unsigned nargs = get_app_num_args(e); + auto & cache = get_cache(*this); + + /* Check if (fn, nargs) is in the cache */ + congr_lemma_key key1(fn, nargs); + auto it1 = cache.find(key1); + if (it1 != cache.end()) + return it1->second; + + /* Try automatically generated congruence lemma with support for heterogeneous equality. */ + auto lemma = mk_hcongr_lemma_core(m_ctx, fn, nargs); + + if (lemma) { + /* succeeded */ + cache.insert(mk_pair(key1, lemma)); + return lemma; + } + + /* cache failure */ + cache.insert(mk_pair(key1, optional())); + return optional(); +} + +expr congruence_closure::state::get_root(expr const & e) const { + if (auto n = m_entries.find(e)) { + return n->m_root; + } else { + return e; + } +} + +expr congruence_closure::state::get_next(expr const & e) const { + if (auto n = m_entries.find(e)) { + return n->m_next; + } else { + return e; + } +} + +unsigned congruence_closure::state::get_mt(expr const & e) const { + if (auto n = m_entries.find(e)) { + return n->m_mt; + } else { + return m_gmt; + } +} + +bool congruence_closure::state::is_congr_root(expr const & e) const { + if (auto n = m_entries.find(e)) { + return e == n->m_cg_root; + } else { + return true; + } +} + +/** \brief Return true iff the given function application are congruent + + See paper: Congruence Closure for Intensional Type Theory. */ +static bool is_congruent(expr const & e1, expr const & e2) { + lean_assert(is_app(e1) && is_app(e2)); + /* Given e1 := f a, e2 := g b */ + expr f = app_fn(e1); + expr a = app_arg(e1); + expr g = app_fn(e2); + expr b = app_arg(e2); + if (g_cc->get_root(a) != g_cc->get_root(b)) { + /* a and b are not equivalent */ + return false; + } + if (g_cc->get_root(f) != g_cc->get_root(g)) { + /* f and g are not equivalent */ + return false; + } + type_context & ctx = g_cc->ctx(); + if (ctx.is_def_eq(ctx.infer(f), ctx.infer(g))) { + /* Case 1: f and g have the same type, then we can create a congruence proof for f a == g b */ + return true; + } + if (is_app(f) && is_app(g)) { + /* Case 2: f and g are congruent */ + return is_congruent(f, g); + } + /* + f and g are not congruent nor they have the same type. + We can't generate a congruence proof in this case because the following lemma + + hcongr : f1 == f2 -> a1 == a2 -> f1 a1 == f2 a2 + + is not provable. Remark: it is also not provable in MLTT, Coq and Agda (even if we assume UIP). */ + return false; +} + +int congruence_closure::congr_key_cmp::operator()(congr_key const & k1, congr_key const & k2) const { + if (k1.m_hash != k2.m_hash) + return unsigned_cmp()(k1.m_hash, k2.m_hash); + if (is_congruent(k1.m_expr, k2.m_expr)) + return 0; + return expr_quick_cmp()(k1.m_expr, k2.m_expr); +} + +/* Auxiliary function for comparing (lhs1 ~ rhs1) and (lhs2 ~ rhs2), + when ~ is symmetric/commutative. + It returns 0 (equal) for (a ~ b) (b ~ a) */ +int congruence_closure::compare_symm(expr lhs1, expr rhs1, expr lhs2, expr rhs2) const { + lhs1 = get_root(lhs1); + rhs1 = get_root(rhs1); + lhs2 = get_root(lhs2); + rhs2 = get_root(rhs2); + if (is_lt(lhs1, rhs1, true)) + std::swap(lhs1, rhs1); + if (is_lt(lhs2, rhs2, true)) + std::swap(lhs2, rhs2); + if (lhs1 != lhs2) + return is_lt(lhs1, lhs2, true) ? -1 : 1; + if (rhs1 != rhs2) + return is_lt(rhs1, rhs2, true) ? -1 : 1; + return 0; +} + +unsigned congruence_closure::symm_hash(expr const & lhs, expr const & rhs) const { + unsigned h1 = get_root(lhs).hash(); + unsigned h2 = get_root(rhs).hash(); + if (h1 > h2) + std::swap(h1, h2); + return (h1 << 16) | (h2 & 0xFFFF); +} + +/* \brief Create a equality congruence table key. */ +auto congruence_closure::mk_congr_key(expr const & e) const -> congr_key { + lean_assert(is_app(e)); + congr_key k; + k.m_expr = e; + expr const & f = app_fn(e); + expr const & a = app_arg(e); + k.m_hash = hash(get_root(f).hash(), get_root(a).hash()); + return k; +} + +auto congruence_closure::is_symm_relation(expr const & e, expr & lhs, expr & rhs) const -> optional { + if (is_eq(e, lhs, rhs)) { + return optional(symm_kind::Eq); + } else if (is_iff(e, lhs, rhs)) { + return optional(symm_kind::Iff); + } else { + if (!is_app(e)) return optional(); + expr fn = get_app_fn(e); + if (!is_constant(fn)) return optional(); + if (auto info = m_rel_info_getter(const_name(fn))) { + if (!m_symm_info_getter(const_name(fn))) return optional(); + buffer args; + get_app_args(e, args); + if (args.size() != info->get_arity()) return optional(); + lhs = args[info->get_lhs_pos()]; + rhs = args[info->get_rhs_pos()]; + return optional(symm_kind::Other); + } + return optional(); + } +} + +bool congruence_closure::is_symm_relation(expr const & e) { + expr lhs, rhs; + return static_cast(is_symm_relation(e, lhs, rhs)); +} + +/* \brief Create a symm congruence table key. */ +auto congruence_closure::mk_symm_congr_key(expr const & e) const -> symm_congr_key { + expr lhs, rhs; + if (auto kind = is_symm_relation(e, lhs, rhs)) { + symm_congr_key key; + key.m_expr = e; + key.m_hash = symm_hash(lhs, rhs); + key.m_kind = *kind; + return key; + } + lean_unreachable(); +} + +int congruence_closure::symm_congr_key_cmp::operator()(symm_congr_key const & k1, symm_congr_key const & k2) const { + if (k1.m_hash != k2.m_hash) + return unsigned_cmp()(k1.m_hash, k2.m_hash); + if (k1.m_kind != k2.m_kind) + return unsigned_cmp()(static_cast(k1.m_kind), static_cast(k2.m_kind)); + expr const & e1 = k1.m_expr; + expr const & e2 = k2.m_expr; + switch (k1.m_kind) { + case symm_kind::Eq: case symm_kind::Iff: + return g_cc->compare_symm(app_arg(app_fn(e1)), app_arg(e1), app_arg(app_fn(e2)), app_arg(e2)); + case symm_kind::Other: { + expr lhs1, rhs1, lhs2, rhs2; + g_cc->is_symm_relation(e1, lhs1, rhs1); + g_cc->is_symm_relation(e2, lhs2, rhs2); + return g_cc->compare_symm(lhs1, rhs1, lhs2, rhs2); + }} + lean_unreachable(); +} + +/* TODO(Leo): this should not be hard-coded. + In the future, we may add a new attribute to control it. */ +bool congruence_closure::is_logical_app(expr const & n) { + if (!is_app(n)) return false; + expr const & fn = get_app_fn(n); + return + is_constant(fn) && + (const_name(fn) == get_or_name() || + const_name(fn) == get_and_name() || + const_name(fn) == get_not_name() || + const_name(fn) == get_iff_name() || + (const_name(fn) == get_ite_name() && m_ctx.is_prop(n))); +} + +void congruence_closure::push_todo(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof) { + m_todo.emplace_back(lhs, rhs, H, heq_proof); +} + +void congruence_closure::process_subsingleton_elem(expr const & e) { + expr type = m_ctx.infer(e); + optional ss = m_ctx.mk_subsingleton_instance(type); + if (!ss) return; /* type is not a subsingleton */ + /* use defeq_canonize to "normalize" instance */ + bool dummy; + type = defeq_canonize(m_ctx, type, dummy); + /* Make sure type has been internalized */ + bool toplevel = true; + bool propagate = false; + internalize_core(type, toplevel, propagate); + /* Try to find representative */ + if (auto it = m_state.m_subsingleton_reprs.find(type)) { + push_subsingleton_eq(e, *it); + } else { + m_state.m_subsingleton_reprs.insert(type, e); + } + expr type_root = get_root(type); + if (type_root == type) + return; + if (auto it2 = m_state.m_subsingleton_reprs.find(type_root)) { + push_subsingleton_eq(e, *it2); + } else { + m_state.m_subsingleton_reprs.insert(type_root, e); + } +} + +/* This method is invoked during internalization and eagerly apply basic equivalences for term \c e + Examples: + - If e := cast H e', then it merges the equivalence classes of (cast H e') and e' + + In principle, we could mark theorems such as cast_eq as simplification rules, but this creates + problems with the builtin support for cast-introduction in the ematching module. + + Eagerly merging the equivalence classes is also more efficient. */ +void congruence_closure::apply_simple_eqvs(expr const & e) { + if (is_app_of(e, get_cast_name(), 4)) { + /* cast H a == a + + theorem cast_heq : ∀ {A B : Type.{l_1}} (H : A = B) (a : A), @cast.{l_1} A B H a == a + */ + buffer args; + expr const & cast = get_app_args(e, args); + expr const & a = args[3]; + expr proof = mk_app(mk_constant(get_cast_heq_name(), const_levels(cast)), args); + bool heq_proof = true; + push_todo(e, a, proof, heq_proof); + } + + if (is_app_of(e, get_eq_rec_name(), 6)) { + /* eq.rec p H == p + + theorem eq_rec_heq : ∀ {A : Type.{l_1}} {P : A → Type.{l_2}} {a a' : A} (H : a = a') (p : P a), @eq.rec.{l_2 l_1} A a P p a' H == p + */ + buffer args; + expr const & eq_rec = get_app_args(e, args); + expr A = args[0]; expr a = args[1]; expr P = args[2]; expr p = args[3]; + expr a_prime = args[4]; expr H = args[5]; + level l_2 = head(const_levels(eq_rec)); + level l_1 = head(tail(const_levels(eq_rec))); + expr proof = mk_app({mk_constant(get_eq_rec_heq_name(), {l_1, l_2}), A, P, a, a_prime, H, p}); + bool heq_proof = true; + push_todo(e, p, proof, heq_proof); + } +} + +void congruence_closure::add_occurrence(expr const & parent, expr const & child, bool symm_table) { + parent_occ_set ps; + if (auto old_ps = m_state.m_parents.find(child)) + ps = *old_ps; + ps.insert(parent_occ(parent, symm_table)); + m_state.m_parents.insert(child, ps); +} + +static expr * g_congr_mark = nullptr; // dummy congruence proof, it is just a placeholder. +static expr * g_eq_true_mark = nullptr; // dummy eq_true proof, it is just a placeholder. + +void congruence_closure::add_congruence_table(expr const & e) { + lean_assert(is_app(e)); + congr_key k = mk_congr_key(e); + if (auto old_k = m_state.m_congruences.find(k)) { + /* + Found new equivalence: e ~ old_k->m_expr + 1. Update m_cg_root field for e + */ + entry new_entry = *get_entry(e); + new_entry.m_cg_root = old_k->m_expr; + m_state.m_entries.insert(e, new_entry); + /* 2. Put new equivalence in the todo queue */ + /* TODO(Leo): check if the following line is a bottleneck */ + bool heq_proof = !m_ctx.is_def_eq(m_ctx.infer(e), m_ctx.infer(old_k->m_expr)); + push_todo(e, old_k->m_expr, *g_congr_mark, heq_proof); + } else { + m_state.m_congruences.insert(k); + } +} + +void congruence_closure::check_eq_true(symm_congr_key const & k) { + expr const & e = k.m_expr; + expr lhs, rhs; + if (!is_symm_relation(e, lhs, rhs)) + return; + if (is_eqv(e, mk_true())) + return; // it is already equivalent to true + lhs = get_root(lhs); + rhs = get_root(rhs); + if (lhs != rhs) return; + // Add e <-> true + bool heq_proof = false; + push_todo(e, mk_true(), *g_eq_true_mark, heq_proof); +} + +void congruence_closure::add_symm_congruence_table(expr const & e) { + lean_assert(is_symm_relation(e)); + symm_congr_key k = mk_symm_congr_key(e); + if (auto old_k = m_state.m_symm_congruences.find(k)) { + /* + Found new equivalence: e ~ old_k->m_expr + 1. Update m_cg_root field for e + */ + entry new_entry = *get_entry(e); + new_entry.m_cg_root = old_k->m_expr; + m_state.m_entries.insert(e, new_entry); + /* 2. Put new equivalence in the TODO queue */ + bool heq_proof = false; + push_todo(e, old_k->m_expr, *g_congr_mark, heq_proof); + } else { + m_state.m_symm_congruences.insert(k); + } + check_eq_true(k); +} + +void congruence_closure::mk_entry_core(expr const & e, bool to_propagate, bool interpreted, bool constructor) { + lean_assert(!get_entry(e)); + entry n; + n.m_next = e; + n.m_root = e; + n.m_cg_root = e; + n.m_size = 1; + n.m_flipped = false; + n.m_interpreted = interpreted; + n.m_constructor = constructor; + n.m_to_propagate = to_propagate; + n.m_heq_proofs = false; + n.m_mt = m_state.m_gmt; + m_state.m_entries.insert(e, n); + process_subsingleton_elem(e); +} + +void congruence_closure::mk_entry_core(expr const & e, bool to_propagate) { + bool interpreted = false; + bool constructor = static_cast(is_constructor_app(env(), e)); + return mk_entry_core(e, to_propagate, interpreted, constructor); +} + +void congruence_closure::mk_entry(expr const & e, bool to_propagate) { + if (to_propagate && !m_ctx.is_prop(e)) + to_propagate = false; + if (auto it = get_entry(e)) { + if (!it->m_to_propagate && to_propagate) { + entry new_it = *it; + new_it.m_to_propagate = to_propagate; + m_state.m_entries.insert(e, new_it); + } + return; + } + mk_entry_core(e, to_propagate); +} + +void congruence_closure::internalize_core(expr const & e, bool toplevel, bool to_propagate) { + lean_assert(closed(e)); + /* We allow metavariables after partitions have been frozen. */ + if (has_expr_metavar(e) && !m_state.m_froze_partitions) + return; + /* Check whether 'e' has already been internalized. */ + if (get_entry(e)) + return; + switch (e.kind()) { + case expr_kind::Var: + lean_unreachable(); + case expr_kind::Sort: + return; + case expr_kind::Constant: + case expr_kind::Local: + case expr_kind::Meta: + mk_entry_core(e, to_propagate); + return; + case expr_kind::Lambda: + case expr_kind::Let: + mk_entry_core(e, false); + return; + case expr_kind::Macro: + for (unsigned i = 0; i < macro_num_args(e); i++) + internalize_core(macro_arg(e, i), false, false); + mk_entry_core(e, to_propagate); + break; + case expr_kind::Pi: + if (is_arrow(e) && m_ctx.is_prop(binding_domain(e)) && m_ctx.is_prop(binding_body(e))) { + to_propagate = toplevel; /* We must propagate children if arrow is top-level */ + internalize_core(binding_domain(e), toplevel, to_propagate); + internalize_core(binding_body(e), toplevel, to_propagate); + } + if (m_ctx.is_prop(e)) { + mk_entry_core(e, false); + } + return; + case expr_kind::App: { + bool is_lapp = is_logical_app(e); + mk_entry_core(e, to_propagate && !is_lapp); + if (toplevel) { + if (is_lapp) { + to_propagate = true; // we must propagate the children of a top-level logical app (or, and, iff, ite) + } else { + toplevel = false; // children of a non-logical application will not be marked as toplevel + } + } else { + to_propagate = false; + } + expr lhs, rhs; + if (is_symm_relation(e, lhs, rhs)) { + internalize_core(lhs, toplevel, to_propagate); + internalize_core(rhs, toplevel, to_propagate); + bool symm_table = true; + add_occurrence(e, lhs, symm_table); + add_occurrence(e, rhs, symm_table); + add_symm_congruence_table(e); + } else if (auto lemma = mk_ext_congr_lemma(e)) { + internalize_core(app_fn(e), toplevel, to_propagate); + internalize_core(app_arg(e), toplevel, to_propagate); + expr it = e; + bool symm_table = false; + while (is_app(it)) { + add_occurrence(e, app_fn(it), symm_table); + add_occurrence(e, app_arg(it), symm_table); + it = app_fn(it); + } + add_congruence_table(e); + } + apply_simple_eqvs(e); + break; + }} +} + +/* + The fields m_target and m_proof in e's entry are encoding a transitivity proof + Let target(e) and proof(e) denote these fields. + + e = target(e) : proof(e) + ... = target(target(e)) : proof(target(e)) + ... ... + = root(e) : ... + + The transitivity proof eventually reaches the root of the equivalence class. + This method "inverts" the proof. That is, the m_target goes from root(e) to e after + we execute it. +*/ +void congruence_closure::invert_trans(expr const & e, bool new_flipped, optional new_target, optional new_proof) { + auto n = get_entry(e); + lean_assert(n); + entry new_n = *n; + if (n->m_target) + invert_trans(*new_n.m_target, !new_n.m_flipped, some_expr(e), new_n.m_proof); + new_n.m_target = new_target; + new_n.m_proof = new_proof; + new_n.m_flipped = new_flipped; + m_state.m_entries.insert(e, new_n); +} + +void congruence_closure::invert_trans(expr const & e) { + invert_trans(e, false, none_expr(), none_expr()); +} + +void congruence_closure::remove_parents(expr const & e) { + auto ps = m_state.m_parents.find(e); + if (!ps) return; + ps->for_each([&](parent_occ const & p) { + if (p.m_symm_table) { + symm_congr_key k = mk_symm_congr_key(p.m_expr); + m_state.m_symm_congruences.erase(k); + } else { + congr_key k = mk_congr_key(p.m_expr); + m_state.m_congruences.erase(k); + } + }); +} + +void congruence_closure::reinsert_parents(expr const & e) { + auto ps = m_state.m_parents.find(e); + if (!ps) return; + ps->for_each([&](parent_occ const & p) { + if (p.m_symm_table) { + add_symm_congruence_table(p.m_expr); + } else { + add_congruence_table(p.m_expr); + } + }); +} + +void congruence_closure::update_mt(expr const & e) { + expr r = get_root(e); + auto ps = m_state.m_parents.find(r); + if (!ps) return; + ps->for_each([&](parent_occ const & p) { + auto it = get_entry(p.m_expr); + lean_assert(it); + if (it->m_mt < m_state.m_gmt) { + auto new_it = *it; + new_it.m_mt = m_state.m_gmt; + m_state.m_entries.insert(p.m_expr, new_it); + update_mt(p.m_expr); + } + }); +} + +bool congruence_closure::has_heq_proofs(expr const & root) const { + lean_assert(get_entry(root)); + lean_assert(get_entry(root)->m_root == root); + return get_entry(root)->m_heq_proofs; +} + +expr congruence_closure::flip_proof(expr const & H, bool flipped, bool heq_proofs) const { + if (H == *g_congr_mark || H == *g_eq_true_mark) { + return H; + } else { + expr new_H = H; + if (heq_proofs && is_eq(m_ctx.relaxed_whnf(m_ctx.infer(new_H)))) { + new_H = mk_heq_of_eq(m_ctx, new_H); + } + if (!flipped) { + return new_H; + } else { + return heq_proofs ? mk_heq_symm(m_ctx, new_H) : mk_eq_symm(m_ctx, new_H); + } + } +} + +expr congruence_closure::mk_trans(bool heq_proofs, optional const & H1, expr const & H2) const { + if (!H1) return H2; + return heq_proofs ? mk_heq_trans(m_ctx, *H1, H2) : mk_eq_trans(m_ctx, *H1, H2); +} + +expr congruence_closure::mk_congr_proof(expr const & /* lhs */, expr const & /* rhs */, bool /* heq_proofs */) const { + /* TODO(Leo) */ + return expr(); +} + +expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const & H, bool heq_proofs) const { + if (H == *g_congr_mark) { + return mk_congr_proof(lhs, rhs, heq_proofs); + } else if (H == *g_eq_true_mark) { + /* TODO(Leo) */ + return expr(); + } else { + return H; + } +} + +/* + If as_heq is true, then build a proof for (e1 == e2). + Otherwise, build a proof for (e1 = e2). + The result is none if e1 and e2 are not in the same equivalence class. */ +optional congruence_closure::get_eq_proof_core(expr const & e1, expr const & e2, bool as_heq) const { + if (has_expr_metavar(e1) || has_expr_metavar(e2)) return none_expr(); + if (m_ctx.is_def_eq(e1, e2)) + return some_expr(mk_eq_refl(m_ctx, e1)); + auto n1 = get_entry(e1); + if (!n1) return none_expr(); + auto n2 = get_entry(e2); + if (!n2) return none_expr(); + if (n1->m_root != n2->m_root) return none_expr(); + bool heq_proofs = has_heq_proofs(n1->m_root); + // 1. Retrieve "path" from e1 to root + buffer path1, Hs1; + rb_tree visited; + expr it1 = e1; + while (true) { + visited.insert(it1); + auto it1_n = get_entry(it1); + lean_assert(it1_n); + if (!it1_n->m_target) + break; + path1.push_back(*it1_n->m_target); + Hs1.push_back(flip_proof(*it1_n->m_proof, it1_n->m_flipped, heq_proofs)); + it1 = *it1_n->m_target; + } + lean_assert(it1 == n1->m_root); + // 2. The path from e2 to root must have at least one element c in visited + // Retrieve "path" from e2 to c + buffer path2, Hs2; + expr it2 = e2; + while (true) { + if (visited.contains(it2)) + break; // found common + auto it2_n = get_entry(it2); + lean_assert(it2_n); + lean_assert(it2_n->m_target); + path2.push_back(it2); + Hs2.push_back(flip_proof(*it2_n->m_proof, !it2_n->m_flipped, heq_proofs)); + it2 = *it2_n->m_target; + } + // it2 is the common element... + // 3. Shrink path1/Hs1 until we find it2 (the common element) + while (true) { + if (path1.empty()) { + lean_assert(it2 == e1); + break; + } + if (path1.back() == it2) { + // found it! + break; + } + path1.pop_back(); + Hs1.pop_back(); + } + + // 4. Build transitivity proof + optional pr; + expr lhs = e1; + for (unsigned i = 0; i < path1.size(); i++) { + pr = mk_trans(heq_proofs, pr, mk_proof(lhs, path1[i], Hs1[i], heq_proofs)); + lhs = path1[i]; + } + unsigned i = Hs2.size(); + while (i > 0) { + --i; + pr = mk_trans(heq_proofs, pr, mk_proof(lhs, path2[i], Hs2[i], heq_proofs)); + lhs = path2[i]; + } + lean_assert(pr); + if (heq_proofs && !as_heq) + pr = mk_eq_of_heq(m_ctx, *pr); + else if (!heq_proofs && as_heq) + pr = mk_heq_of_eq(m_ctx, *pr); + return pr; +} + +optional congruence_closure::get_eq_proof(expr const & e1, expr const & e2) const { + return get_eq_proof_core(e1, e2, false); +} + +optional congruence_closure::get_heq_proof(expr const & e1, expr const & e2) const { + return get_eq_proof_core(e1, e2, true); +} + +void congruence_closure::push_subsingleton_eq(expr const & a, expr const & b) { + expr A = m_ctx.infer(a); + expr B = m_ctx.infer(b); + /* TODO(Leo): check if the following test is a performance bottleneck */ + if (m_ctx.relaxed_is_def_eq(A, B)) { + /* TODO(Leo): to improve performance we can create the following proof lazily */ + bool heq_proof = false; + expr proof = mk_app(m_ctx, get_subsingleton_elim_name(), a, b); + push_todo(a, b, proof, heq_proof); + } else { + expr A_eq_B = *get_eq_proof(A, B); + expr proof = mk_app(m_ctx, get_subsingleton_helim_name(), A_eq_B, a, b); + bool heq_proof = true; + push_todo(a, b, proof, heq_proof); + } +} + +void congruence_closure::check_new_subsingleton_eq(expr const & old_root, expr const & new_root) { + lean_assert(is_eqv(old_root, new_root)); + lean_assert(get_root(old_root) == new_root); + auto it1 = m_state.m_subsingleton_reprs.find(old_root); + if (!it1) return; + if (auto it2 = m_state.m_subsingleton_reprs.find(new_root)) { + push_subsingleton_eq(*it1, *it2); + } else { + m_state.m_subsingleton_reprs.insert(new_root, *it1); + } +} + +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)); + expr type = mk_eq(m_ctx, e1, e2); + expr pr = *get_eq_proof(e1, e2); + /* TODO(Leo): use no_confusion to build proofs for arguments */ +} + +static bool is_true_or_false(expr const & e) { + return is_constant(e, get_true_name()) || is_constant(e, get_false_name()); +} + +/* 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(expr e1, expr e2, expr const & H, + optional const & /* added_prop */, bool heq_proof) { + auto n1 = get_entry(e1); + auto n2 = get_entry(e2); + if (!n1 || !n2) + return; /* e1 and e2 have not been internalized */ + if (n1->m_root == n2->m_root) + return; /* they are already in the same equivalence class. */ + auto r1 = get_entry(n1->m_root); + auto r2 = get_entry(n2->m_root); + lean_assert(r1 && r2); + bool flipped = false; + + /* We want r2 to be the root of the combined class. */ + + /* + We swap (e1,n1,r1) with (e2,n2,r2) when + 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 in 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_constructor && !r2->m_interpreted && !r2->m_constructor + Reason: we want constructors to be the representative of their equivalence classes. + 3- 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); + // Remark: we don't apply symmetry eagerly. So, we don't adjust H. + flipped = true; + } + + if (r1->m_interpreted && r2->m_interpreted) + m_state.m_inconsistent = true; + + bool use_no_confusion = r1->m_constructor && r2->m_constructor; + + expr e1_root = n1->m_root; + expr e2_root = n2->m_root; + entry new_n1 = *n1; + + /* + Following target/proof we have + e1 -> ... -> r1 + e2 -> ... -> r2 + We want + r1 -> ... -> e1 -> e2 -> ... -> r2 + */ + invert_trans(e1); + new_n1.m_target = e2; + new_n1.m_proof = H; + new_n1.m_flipped = flipped; + m_state.m_entries.insert(e1, new_n1); + + /* The hash code for the parents is going to change */ + remove_parents(e1_root); + + /* force all m_root fields in e1 equivalence class to point to e2_root */ + bool propagate = is_true_or_false(e2_root); + buffer to_propagate; + expr it = e1; + do { + auto it_n = get_entry(it); + if (propagate && it_n->m_to_propagate) + to_propagate.push_back(it); + lean_assert(it_n); + entry new_it_n = *it_n; + new_it_n.m_root = e2_root; + m_state.m_entries.insert(it, new_it_n); + it = new_it_n.m_next; + } while (it != e1); + + reinsert_parents(e1_root); + + // update next of e1_root and e2_root, and size of e2_root + r1 = get_entry(e1_root); + r2 = get_entry(e2_root); + lean_assert(r1 && r2); + lean_assert(r1->m_root == e2_root); + entry new_r1 = *r1; + entry new_r2 = *r2; + new_r1.m_next = r2->m_next; + new_r2.m_next = r1->m_next; + new_r2.m_size += r1->m_size; + if (heq_proof) + new_r2.m_heq_proofs = true; + m_state.m_entries.insert(e1_root, new_r1); + m_state.m_entries.insert(e2_root, new_r2); + lean_assert(check_invariant()); + + // copy e1_root parents to e2_root + auto ps1 = m_state.m_parents.find(e1_root); + if (ps1) { + parent_occ_set ps2; + if (auto it = m_state.m_parents.find(e2_root)) + ps2 = *it; + ps1->for_each([&](parent_occ const & p) { + if (is_congr_root(p.m_expr)) + ps2.insert(p); + }); + m_state.m_parents.erase(e1_root); + m_state.m_parents.insert(e2_root, ps2); + } + + // propagate new hypotheses back to current state + if (!to_propagate.empty()) { + /* + TODO(Leo): decide how to communicate propagations. + */ + } + + if (use_no_confusion) { + propagate_no_confusion_eq(e1_root, e2_root); + } + + update_mt(e2_root); + check_new_subsingleton_eq(e1_root, e2_root); + lean_trace(name({"cc", "merge"}), scope_trace_env scope(m_ctx.env(), m_ctx); + tout() << e1_root << " = " << e2_root << "\n";); +} + +void congruence_closure::process_todo(optional const & added_prop) { + while (!m_todo.empty()) { + expr lhs, rhs, H; bool heq_proof; + std::tie(lhs, rhs, H, heq_proof) = m_todo.back(); + m_todo.pop_back(); + add_eqv_step(lhs, rhs, H, added_prop, heq_proof); + } +} + +void congruence_closure::add_eqv_core(expr const & lhs, expr const & rhs, expr const & H, + optional const & added_prop, bool heq_proof) { + push_todo(lhs, rhs, H, heq_proof); + process_todo(added_prop); +} + +void congruence_closure::add(expr const & type, expr const & proof) { + if (m_state.m_inconsistent) return; + flet set_cc(g_cc, this); + m_todo.clear(); + expr p = type; + bool is_neg = is_not(type, p); + expr lhs, rhs; + if (is_eq(type, lhs, rhs) || is_heq(type, lhs, rhs)) { + if (is_neg) { + bool toplevel = true; + bool to_propagate = false; + bool heq_proof = false; + internalize_core(p, toplevel, to_propagate); + add_eqv_core(p, mk_false(), mk_eq_false_intro(m_ctx, proof), some_expr(type), heq_proof); + } else { + bool toplevel = false; + bool to_propagate = false; + bool heq_proof = is_heq(type); + internalize_core(lhs, toplevel, to_propagate); + internalize_core(rhs, toplevel, to_propagate); + add_eqv_core(lhs, rhs, proof, some_expr(type), heq_proof); + } + } else if (is_iff(type, lhs, rhs)) { + bool toplevel = true; + bool to_propagate = true; + bool heq_proof = false; + if (is_neg) { + expr neq_proof = mk_neq_of_not_iff(m_ctx, proof); + internalize_core(p, toplevel, to_propagate); + add_eqv_core(p, mk_false(), mk_eq_false_intro(m_ctx, neq_proof), some_expr(type), heq_proof); + } else { + internalize_core(lhs, toplevel, to_propagate); + internalize_core(rhs, toplevel, to_propagate); + add_eqv_core(lhs, rhs, mk_propext(lhs, rhs, proof), some_expr(type), heq_proof); + } + } else if (is_neg || m_ctx.is_prop(p)) { + bool toplevel = true; + bool to_propagate = false; + bool heq_proof = false; + internalize_core(p, toplevel, to_propagate); + if (is_neg) { + add_eqv_core(p, mk_false(), mk_eq_false_intro(m_ctx, proof), some_expr(type), heq_proof); + } else { + add_eqv_core(p, mk_true(), mk_eq_true_intro(m_ctx, proof), some_expr(type), heq_proof); + } + } +} + +bool congruence_closure::is_eqv(expr const & e1, expr const & e2) const { + auto n1 = get_entry(e1); + if (!n1) return false; + auto n2 = get_entry(e2); + if (!n2) return false; + /* Remark: this method assumes that is_eqv is invoked with type correct parameters. + An eq class may contain equality and heterogeneous equality proofs is enabled. + When this happens, the answer is correct only if e1 and e2 have the same type. */ + return n1->m_root == n2->m_root; +} + +bool congruence_closure::is_not_eqv(expr const & e1, expr const & e2) const { + try { + expr tmp = mk_eq(m_ctx, e1, e2); + if (is_eqv(tmp, mk_false())) + return true; + tmp = mk_heq(m_ctx, e1, e2); + return is_eqv(tmp, mk_false()); + } catch (app_builder_exception &) { + return false; + } +} + +bool congruence_closure::proved(expr const & e) const { + return is_eqv(e, mk_true()); +} + +bool congruence_closure::state::check_eqc(expr const & e) const { + expr root = get_root(e); + unsigned size = 0; + expr it = e; + do { + auto it_n = m_entries.find(it); + lean_assert(it_n); + lean_assert(it_n->m_root == root); + auto it2 = it; + // following m_target fields should lead to root + while (true) { + auto it2_n = m_entries.find(it2); + if (!it2_n->m_target) + break; + it2 = *it2_n->m_target; + } + lean_assert(it2 == root); + it = it_n->m_next; + size++; + } while (it != e); + lean_assert(m_entries.find(root)->m_size == size); + return true; +} + +bool congruence_closure::state::check_invariant() const { + m_entries.for_each([&](expr const & k, entry const & n) { + if (k == n.m_root) { + lean_assert(check_eqc(k)); + } + }); + return true; +} +} diff --git a/src/library/tactic/congruence/congruence_closure.h b/src/library/tactic/congruence/congruence_closure.h new file mode 100644 index 0000000000..9288fc1a70 --- /dev/null +++ b/src/library/tactic/congruence/congruence_closure.h @@ -0,0 +1,223 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +#include "library/expr_lt.h" +#include "library/type_context.h" +#include "library/congr_lemma.h" +#include "library/relation_manager.h" + +namespace lean { +struct ext_congr_lemma; + +class congr_lemma_cache; +typedef std::shared_ptr congr_lemma_cache_ptr; + +class congruence_closure { + /* Key for the equality congruence table. */ + struct congr_key { + expr m_expr; + unsigned m_hash; + }; + + struct congr_key_cmp { + int operator()(congr_key const & k1, congr_key const & k2) const; + }; + + enum class symm_kind {Eq, Iff, Other}; + + /* Key for the equality congruence table for symmetric relations. + + Remark: the same congruence table can be used to handle + commutative operations. */ + struct symm_congr_key { + expr m_expr; + unsigned m_hash; + symm_kind m_kind; + }; + + struct symm_congr_key_cmp { + int operator()(symm_congr_key const & k1, symm_congr_key const & k2) const; + }; + + /* Equivalence class data associated with an expression 'e' */ + struct entry { + expr m_next; // next element in the equivalence class. + expr m_root; // root (aka canonical) representative of the equivalence class. + expr m_cg_root; // root of the congruence class, it is meaningless if 'e' is not an application. + /* When 'e' was added to this equivalence class because of an equality (H : e = target), then we + store 'target' at 'm_target', and 'H' at 'm_proof'. Both fields are none if 'e' == m_root */ + optional m_target; + optional m_proof; + 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 + /* m_heq_proofs == true iff some proofs in the equivalence class are based on heterogeneous equality. + We represent equality and heterogeneous equality in a single equivalence class. */ + unsigned m_heq_proofs:1; + unsigned m_size; // number of elements in the equivalence class, it is meaningless if 'e' != m_root + /* The field m_mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. + The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have + occurred in the current branch. It is incremented after each round of heuristic instantiation. + The field m_mt records the last time any proper descendant of of thie entry was involved in a merge. */ + unsigned m_mt; + }; + + struct parent_occ { + expr m_expr; + /* If m_symm_table is true, then we should use the m_symm_congruences, otherwise m_congruences. + Remark: this information is redundant, it can be inferred from m_expr. We use store it for + performance reasons. */ + bool m_symm_table; + parent_occ() {} + parent_occ(expr const & e, bool symm_table):m_expr(e), m_symm_table(symm_table) {} + }; + + struct parent_occ_cmp { + int operator()(parent_occ const & k1, parent_occ const & k2) const { + return expr_quick_cmp()(k1.m_expr, k2.m_expr); + } + }; + + typedef rb_tree expr_set; + typedef rb_map entries; + typedef rb_tree parent_occ_set; + typedef rb_map parents; + typedef rb_tree congruences; + typedef rb_tree symm_congruences; + typedef rb_map subsingleton_reprs; + typedef std::tuple todo_entry; + + class state { + entries m_entries; + parents m_parents; + congruences m_congruences; + symm_congruences m_symm_congruences; + /** The following mapping store a representative for each subsingleton type */ + subsingleton_reprs m_subsingleton_reprs; + /** The congruence closure module has a mode where the root of + each equivalence class is marked as an interpreted/abstract + value. Moreover, in this mode proof production is disabled. + This capability is useful for heuristic instantiation. */ + short m_froze_partitions{false}; + short m_inconsistent{false}; + unsigned m_gmt{0}; + friend class congruence_closure; + bool check_eqc(expr const & e) const; + public: + expr get_root(expr const & e) const; + expr get_next(expr const & e) const; + unsigned get_mt(expr const & e) const; + bool is_congr_root(expr const & e) const; + bool check_invariant() const; + }; + + type_context & m_ctx; + state & m_state; + buffer m_todo; + congr_lemma_cache_ptr m_cache_ptr; + transparency_mode m_mode; + relation_info_getter m_rel_info_getter; + symm_info_getter m_symm_info_getter; + + entry const * get_entry(expr const & e) const { return m_state.m_entries.find(e); } + int compare_symm(expr lhs1, expr rhs1, expr lhs2, expr rhs2) const; + unsigned symm_hash(expr const & lhs, expr const & rhs) const; + optional is_symm_relation(expr const & e, expr & lhs, expr & rhs) const; + bool is_symm_relation(expr const & e); + congr_key mk_congr_key(expr const & e) const; + symm_congr_key mk_symm_congr_key(expr const & e) const; + bool is_logical_app(expr const & n); + void process_subsingleton_elem(expr const & e); + void apply_simple_eqvs(expr const & e); + void add_occurrence(expr const & parent, expr const & child, bool symm_table); + void add_congruence_table(expr const & e); + void check_eq_true(symm_congr_key const & k); + void add_symm_congruence_table(expr const & e); + void mk_entry_core(expr const & e, bool to_propagate, bool interpreted, bool constructor); + void mk_entry_core(expr const & e, bool to_propagate); + void mk_entry(expr const & e, bool to_propagate); + void internalize_core(expr const & e, bool toplevel, bool to_propagate); + void push_todo(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof); + void invert_trans(expr const & e, bool new_flipped, optional new_target, optional new_proof); + void invert_trans(expr const & e); + void remove_parents(expr const & e); + void reinsert_parents(expr const & e); + void update_mt(expr const & e); + bool has_heq_proofs(expr const & root) const; + expr flip_proof(expr const & H, bool flipped, bool heq_proofs) const; + expr mk_trans(bool heq_proofs, optional const & H1, expr const & H2) const; + expr mk_congr_proof(expr const & lhs, expr const & rhs, bool heq_proofs) const; + expr mk_proof(expr const & lhs, expr const & rhs, expr const & H, bool heq_proofs) const; + optional get_eq_proof_core(expr const & e1, expr const & e2, bool as_heq) const; + optional get_heq_proof(expr const & e1, expr const & e2) const; + optional get_eq_proof(expr const & e1, expr const & e2) const; + void push_subsingleton_eq(expr const & a, expr const & b); + void check_new_subsingleton_eq(expr const & old_root, expr const & new_root); + void propagate_no_confusion_eq(expr const & e1, expr const & e2); + void add_eqv_step(expr e1, expr e2, expr const & H, + optional const & added_prop, bool heq_proof); + void process_todo(optional const & added_prop); + void add_eqv_core(expr const & lhs, expr const & rhs, expr const & H, + optional const & added_prop, bool heq_proof); + bool check_eqc(expr const & e) const; + optional mk_ext_congr_lemma(expr const & e); + + friend congr_lemma_cache_ptr & get_cache_ptr(congruence_closure & cc); + +public: + congruence_closure(type_context & ctx, state & s); + ~congruence_closure(); + + environment const & env() const { return m_ctx.env(); } + type_context & ctx() { return m_ctx; } + transparency_mode mode() const { return m_mode; } + + /** \brief Register expression \c e in this data-structure. + It creates entries for each sub-expression in \c e. + It also updates the m_parents mapping. + + We ignore the following subterms of \c e. + 1- and, or and not-applications are not inserted into the data-structures, but + their arguments are visited. + 2- (Pi (x : A), B), the subterms A and B are not visited if B depends on x. + 3- (A -> B) is not inserted into the data-structures, but their arguments are visited + if they are propositions. + 4- Terms containing meta-variables. + 5- The subterms of lambda-expressions. + 6- Sorts (Type and Prop). */ + void internalize(expr const & e, bool toplevel); + void internalize(expr const & e); + + void add(expr const & type, expr const & proof); + + bool is_eqv(expr const & e1, expr const & e2) const; + bool is_not_eqv(expr const & e1, expr const & e2) const; + bool proved(expr const & e) const; + + expr get_root(expr const & e) const { return m_state.get_root(e); } + expr get_next(expr const & e) const { return m_state.get_next(e); } + bool is_congr_root(expr const & e) const { return m_state.is_congr_root(e); } + + bool check_invariant() const { return m_state.check_invariant(); } +}; + +struct ext_congr_lemma { + /* The basic congr_lemma object defined at congr_lemma_manager */ + congr_lemma m_congr_lemma; + /* If m_fixed_fun is false, then we build equivalences for functions, and use generic congr lemma, and ignore m_congr_lemma. + That is, even the function can be treated as an Eq argument. */ + unsigned m_fixed_fun:1; + /* If m_heq_result is true, then lemma is based on heterogeneous equality and the conclusion is a heterogeneous equality. */ + unsigned m_heq_result:1; + /* If m_heq_lemma is true, then lemma was created using mk_hcongr_lemma. */ + unsigned m_hcongr_lemma:1; + ext_congr_lemma(congr_lemma const & H): + m_congr_lemma(H), m_fixed_fun(false), m_heq_result(false), m_hcongr_lemma(false) {} +}; +} diff --git a/src/library/util.cpp b/src/library/util.cpp index 1a61eeda21..64e671867a 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -540,9 +540,8 @@ expr mk_iff(expr const & lhs, expr const & rhs) { expr mk_iff_refl(expr const & a) { return mk_app(mk_constant(get_iff_refl_name()), a); } -expr apply_propext(expr const & iff_pr, expr const & iff_term) { - lean_assert(is_iff(iff_term)); - return mk_app(mk_constant(get_propext_name()), app_arg(app_fn(iff_term)), app_arg(iff_term), iff_pr); +expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr) { + return mk_app(mk_constant(get_propext_name()), lhs, rhs, iff_pr); } expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) { @@ -695,6 +694,11 @@ bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs) { } } +bool is_heq(expr const & e, expr & lhs, expr & rhs) { + expr A, B; + return is_heq(e, A, lhs, B, rhs); +} + expr mk_false() { return mk_constant(get_false_name()); } diff --git a/src/library/util.h b/src/library/util.h index 5f041c174b..55b22a0efa 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -186,7 +186,7 @@ bool is_iff(expr const & e, expr & lhs, expr & rhs); expr mk_iff(expr const & lhs, expr const & rhs); expr mk_iff_refl(expr const & a); -expr apply_propext(expr const & iff_pr, expr const & iff_term); +expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr); expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs); expr mk_eq_refl(abstract_type_context & ctx, expr const & a); @@ -218,6 +218,7 @@ bool is_eq_a_a(abstract_type_context & ctx, expr const & e); expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs); bool is_heq(expr const & e); +bool is_heq(expr const & e, expr & lhs, expr & rhs); bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs); expr mk_false();