From 07cb35fd3ce16352943ca7d61a42b0ecf9c20b57 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 09:27:21 -0800 Subject: [PATCH] fix(library/abstract_expr_manager): incorrect handling of de-Bruijn variables --- src/library/abstract_expr_manager.cpp | 9 +++++++-- tests/lean/run/blast_simp3.lean | 11 +++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/blast_simp3.lean diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp index f49e3f8d7..f02e931f0 100644 --- a/src/library/abstract_expr_manager.cpp +++ b/src/library/abstract_expr_manager.cpp @@ -23,7 +23,11 @@ unsigned abstract_expr_manager::hash(expr const & e) { case expr_kind::Lambda: case expr_kind::Pi: h = hash(binding_domain(e)); - m_locals.push_back(m_tctx.mk_tmp_local(binding_domain(e))); + // Remark binding_domain(e) may contain de-bruijn variables. + // We can instantiate them eagerly as we do here, or lazily. + // The lazy approach is potentially more efficient, but we would have + // to use something more sophisticated than an instantiate_rev at expr_kind::App + m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(e)), m_locals.size(), m_locals.data())); h = ::lean::hash(h, hash(binding_body(e))); m_locals.pop_back(); return h; @@ -62,7 +66,8 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) { return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b)); case expr_kind::Lambda: case expr_kind::Pi: if (!is_equal(binding_domain(a), binding_domain(b))) return false; - m_locals.push_back(m_tctx.mk_tmp_local(binding_domain(a))); + // see comment at abstract_expr_manager::hash + m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(a)), m_locals.size(), m_locals.data())); is_eq = is_equal(binding_body(a), binding_body(b)); m_locals.pop_back(); return is_eq; diff --git a/tests/lean/run/blast_simp3.lean b/tests/lean/run/blast_simp3.lean new file mode 100644 index 000000000..c83b1dbb2 --- /dev/null +++ b/tests/lean/run/blast_simp3.lean @@ -0,0 +1,11 @@ +set_option blast.simp false + +example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ → + (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) := +by blast + +set_option blast.simp true + +example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ → + (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) := +by blast