From fb95b71a5e9e6c20dff426e9949b5c74b7c1eb0a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Jan 2016 13:27:58 -0800 Subject: [PATCH] fix(library/blast/forward/pattern): bug in the pattern inference code --- src/library/blast/forward/pattern.cpp | 6 ++++-- tests/lean/run/blast_pattern_inference_bug.lean | 8 ++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/blast_pattern_inference_bug.lean diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index 37ee990f98..f13d459678 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -342,10 +342,12 @@ struct mk_hi_lemma_fn { }); } - candidate_set collect_pattern_hints(buffer const & mvars, expr const & B) { + candidate_set collect_pattern_hints(buffer const & mvars, buffer const & residue, expr const & B) { candidate_set s; for (expr const & mvar : mvars) collect_pattern_hints(m_ctx.infer(mvar), s); + for (expr const & r : residue) + collect_pattern_hints(m_ctx.infer(r), s); collect_pattern_hints(B, s); return s; } @@ -571,9 +573,9 @@ struct mk_hi_lemma_fn { lean_assert(m_mvars.size() == inst_implicit_flags.size()); buffer subst; buffer residue_locals; - candidate_set hints = collect_pattern_hints(m_mvars, B); expr proof = mk_proof(residue_locals, subst); B = replace_mvars(B, subst); + candidate_set hints = collect_pattern_hints(m_mvars, residue_locals, B); list mps; if (!hints.empty()) { mps = mk_multi_patterns_using(hints, false); diff --git a/tests/lean/run/blast_pattern_inference_bug.lean b/tests/lean/run/blast_pattern_inference_bug.lean new file mode 100644 index 0000000000..af308c0ef1 --- /dev/null +++ b/tests/lean/run/blast_pattern_inference_bug.lean @@ -0,0 +1,8 @@ +constant p : nat → Prop +constant q : ∀ a, p a → Prop +lemma ex [forward] : ∀ (a : nat) (h : p a), (:q a h:) := sorry + +set_option blast.strategy "ematch" + +lemma test (h : p 0) : q 0 h := +by blast