diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index cee1a66957..15aa3718a6 100644 --- a/library/init/meta/smt/ematch.lean +++ b/library/init/meta/smt/ematch.lean @@ -12,17 +12,19 @@ meta constant hinst_lemma : Type meta constant hinst_lemmas : Type -/- (mk_core m e as_simp prio) -/ +/- (mk_core m e as_simp), m is used to decide which definitions will be unfolded in patterns. + If as_simp is tt, then this tactic will try to use the left-hand-side of the conclusion + as a pattern. -/ meta constant hinst_lemma.mk_core : transparency → expr → bool → tactic hinst_lemma meta constant hinst_lemma.mk_from_decl_core : transparency → name → bool → tactic hinst_lemma meta constant hinst_lemma.pp : hinst_lemma → tactic format meta constant hinst_lemma.id : hinst_lemma → name meta def hinst_lemma.mk (h : expr) : tactic hinst_lemma := -hinst_lemma.mk_core semireducible h ff +hinst_lemma.mk_core reducible h ff meta def hinst_lemma.mk_from_decl (h : name) : tactic hinst_lemma := -hinst_lemma.mk_from_decl_core semireducible h ff +hinst_lemma.mk_from_decl_core reducible h ff meta constant hinst_lemmas.mk : hinst_lemmas meta constant hinst_lemmas.add : hinst_lemmas → hinst_lemma → hinst_lemmas diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp index 1ad65da437..ca821d0ecc 100644 --- a/src/library/tactic/smt/congruence_tactics.cpp +++ b/src/library/tactic/smt/congruence_tactics.cpp @@ -236,16 +236,16 @@ vm_obj to_obj(hinst_lemma const & s) { vm_obj hinst_lemma_mk_core(vm_obj const & m, vm_obj const & lemma, vm_obj const & simp, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); - hinst_lemma h = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp)); + type_context ctx = mk_type_context_for(s); + hinst_lemma h = mk_hinst_lemma(ctx, to_transparency_mode(m), to_expr(lemma), to_bool(simp)); return mk_tactic_success(to_obj(h), to_tactic_state(s)); LEAN_TACTIC_CATCH(to_tactic_state(s)); } vm_obj hinst_lemma_mk_from_decl_core(vm_obj const & m, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); - hinst_lemma h = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp)); + type_context ctx = mk_type_context_for(s); + hinst_lemma h = mk_hinst_lemma(ctx, to_transparency_mode(m), to_name(lemma_name), to_bool(simp)); return mk_tactic_success(to_obj(h), to_tactic_state(s)); LEAN_TACTIC_CATCH(to_tactic_state(s)); } diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp index d1bc734443..2424694c73 100644 --- a/src/library/tactic/smt/hinst_lemmas.cpp +++ b/src/library/tactic/smt/hinst_lemmas.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "library/util.h" #include "library/trace.h" +#include "library/normalize.h" #include "library/idx_metavar.h" #include "library/type_context.h" #include "library/annotation.h" @@ -241,6 +242,7 @@ expr extract_trackable(type_context & ctx, expr const & type, struct mk_hinst_lemma_fn { type_context & m_ctx; + transparency_mode m_md_norm; name_set m_no_inst_patterns; expr m_H; unsigned m_num_uvars; @@ -255,10 +257,10 @@ struct mk_hinst_lemma_fn { unsigned m_num_steps; name m_id; - mk_hinst_lemma_fn(type_context & ctx, expr const & H, + mk_hinst_lemma_fn(type_context & ctx, transparency_mode md_norm, expr const & H, unsigned num_uvars, unsigned max_steps, bool simp, name const & id): - m_ctx(ctx), m_no_inst_patterns(get_no_inst_patterns(ctx.env())), + m_ctx(ctx), m_md_norm(md_norm), m_no_inst_patterns(get_no_inst_patterns(ctx.env())), m_H(H), m_num_uvars(num_uvars), m_max_steps(max_steps), m_simp(simp), m_id(id) {} @@ -283,6 +285,11 @@ struct mk_hinst_lemma_fn { typedef rb_tree candidate_set; + expr normalize(expr const & e) { + type_context::transparency_scope _(m_ctx, m_md_norm); + return ::lean::normalize(m_ctx, e); + } + void collect_pattern_hints(expr const & e, candidate_set & s) { for_each(e, [&](expr const & e, unsigned) { if (is_pattern_hint(e)) { @@ -290,7 +297,7 @@ struct mk_hinst_lemma_fn { // TODO(Leo): if hint was unfolded and is not an application anymore, we should // report to user this fact. if (is_app(hint)) { - s.insert(candidate(hint)); + s.insert(candidate(normalize(hint))); } return false; } @@ -382,10 +389,10 @@ struct mk_hinst_lemma_fn { if (m_simp) { expr lhs, rhs; if (is_eq(a, lhs, rhs) || is_heq(a, lhs, rhs)) { - m_candidates.insert(candidate(lhs)); + m_candidates.insert(candidate(normalize(lhs))); } } else { - save_candidates(collect_core(a)); + save_candidates(collect_core(normalize(a))); } return m_candidates; } @@ -425,6 +432,7 @@ struct mk_hinst_lemma_fn { b) delete any candidate c_1 if there is a c_2 s.t. c_1 is a subterm of c_2, and c_2.m_vars is a strict superset of c_1.m_vars */ list mk_multi_patterns_using(candidate_set s, bool heuristic) { + if (heuristic) { buffer unit_patterns; s.for_each([&](candidate const & c) { @@ -586,17 +594,17 @@ struct mk_hinst_lemma_fn { } }; -hinst_lemma mk_hinst_lemma_core(type_context & ctx, expr const & H, unsigned num_uvars, +hinst_lemma mk_hinst_lemma_core(type_context & ctx, transparency_mode md_norm, expr const & H, unsigned num_uvars, unsigned max_steps, bool simp, name const & id) { try { type_context::tmp_mode_scope tscope(ctx, num_uvars, 0); bool erase_hints = false; - return mk_hinst_lemma_fn(ctx, H, num_uvars, max_steps, simp, id)(erase_hints); + return mk_hinst_lemma_fn(ctx, md_norm, H, num_uvars, max_steps, simp, id)(erase_hints); } catch (mk_hinst_lemma_fn::try_again_without_hints &) { type_context::tmp_mode_scope tscope(ctx, num_uvars, 0); try { bool erase_hints = true; - return mk_hinst_lemma_fn(ctx, H, num_uvars, max_steps, simp, id)(erase_hints); + return mk_hinst_lemma_fn(ctx, md_norm, H, num_uvars, max_steps, simp, id)(erase_hints); } catch (mk_hinst_lemma_fn::try_again_without_hints &) { lean_unreachable(); } @@ -609,15 +617,15 @@ unsigned get_hinst_lemma_max_steps(options const & o) { return o.get_unsigned(*g_hinst_lemma_max_steps, LEAN_DEFAULT_HINST_LEMMA_PATTERN_MAX_STEPS); } -hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp) { +hinst_lemma mk_hinst_lemma(type_context & ctx, transparency_mode md_norm, expr const & H, bool simp) { unsigned max_steps = get_hinst_lemma_max_steps(ctx.get_options()); name id; if (is_local(H)) id = local_pp_name(H); - return mk_hinst_lemma_core(ctx, H, 0, max_steps, simp, id); + return mk_hinst_lemma_core(ctx, md_norm, H, 0, max_steps, simp, id); } -hinst_lemma mk_hinst_lemma(type_context & ctx, name const & c, bool simp) { +hinst_lemma mk_hinst_lemma(type_context & ctx, transparency_mode md_norm, name const & c, bool simp) { unsigned max_steps = get_hinst_lemma_max_steps(ctx.get_options()); declaration const & d = ctx.env().get(c); buffer us; @@ -626,7 +634,7 @@ hinst_lemma mk_hinst_lemma(type_context & ctx, name const & c, bool simp) { us.push_back(mk_idx_metauniv(i)); expr H = mk_constant(c, to_list(us)); name id = c; - return mk_hinst_lemma_core(ctx, H, num_us, max_steps, simp, id); + return mk_hinst_lemma_core(ctx, md_norm, H, num_us, max_steps, simp, id); } format pp_hinst_lemma(formatter const & fmt, hinst_lemma const & h) { diff --git a/src/library/tactic/smt/hinst_lemmas.h b/src/library/tactic/smt/hinst_lemmas.h index 3bc3f0efb6..5c35462aba 100644 --- a/src/library/tactic/smt/hinst_lemmas.h +++ b/src/library/tactic/smt/hinst_lemmas.h @@ -44,20 +44,30 @@ struct hinst_lemma { expr m_expr; }; +inline int multi_pattern_cmp(multi_pattern const & m1, multi_pattern const & m2) { + return cmp(m1, m2, expr_quick_cmp()); +} + struct hinst_lemma_cmp { int operator()(hinst_lemma const & l1, hinst_lemma const & l2) const { - return expr_quick_cmp()(l1.m_prop, l2.m_prop); + int r = expr_quick_cmp()(l1.m_prop, l2.m_prop); + if (r != 0) return r; + return cmp(l1.m_multi_patterns, l2.m_multi_patterns, multi_pattern_cmp); } }; + typedef rb_tree hinst_lemmas; /** \brief Try to compute multipatterns for declaration \c c using the current environment configuration. */ list mk_multipatterns(environment const & env, io_state const & ios, name const & c); /** \brief Create a (local) heuristic instantiation lemma for \c H. - The maximum number of steps is extracted from the blast config object. */ -hinst_lemma mk_hinst_lemma(type_context & ctx, expr const & H, bool simp = false); -hinst_lemma mk_hinst_lemma(type_context & ctx, name const & n, bool simp = false); + The maximum number of steps is extracted from the blast config object. + + \c md_norm is the transparency_mode used for normalizing the type of the lemma. + The idea is to unfold the lemmas using the given transparency mode. */ +hinst_lemma mk_hinst_lemma(type_context & ctx, transparency_mode md_norm, expr const & H, bool simp = false); +hinst_lemma mk_hinst_lemma(type_context & ctx, transparency_mode md_norm, name const & n, bool simp = false); format pp_hinst_lemma(formatter const & fmt, hinst_lemma const & h); diff --git a/src/util/list.h b/src/util/list.h index 4e1560ae68..f4d0428eb4 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -174,6 +174,24 @@ template inline list to_list(optional const & v) { ret template inline list to_list(T const * v) { return v ? to_list(*v) : list(); } template inline list ptr_to_list(list const * l) { return l ? *l : list(); } +template +int cmp(list const & l1, list const & l2, CMP const & c) { + list const * it1 = &l1; + list const * it2 = &l2; + while (*it1 && *it2) { + int r = c(head(*it1), head(*it2)); + if (r != 0) return r; + it1 = &tail(*it1); + it2 = &tail(*it2); + } + if (!*it1) { + return !*it2 ? 0 : -1; + } else { + lean_assert(*it1 && !*it2); + return 1; + } +} + template inline std::ostream & operator<<(std::ostream & out, list const & l) { out << "("; bool first = true; diff --git a/tests/lean/hinst_lemmas1.lean b/tests/lean/hinst_lemmas1.lean new file mode 100644 index 0000000000..e5c637ddb0 --- /dev/null +++ b/tests/lean/hinst_lemmas1.lean @@ -0,0 +1,13 @@ +axiom foo1 : ∀ (a b c : nat), b > a → b < c → a < c +axiom foo2 : ∀ (a b c : nat), b > a → b < c → a < c +axiom foo3 : ∀ (a b c : nat), b > a → b < c + c → a < c + c + + +run_command +do + hs ← return $ hinst_lemmas.mk, + h₁ ← hinst_lemma.mk_from_decl `foo1, + h₂ ← hinst_lemma.mk_from_decl_core tactic.transparency.none `foo2 ff, + h₃ ← hinst_lemma.mk_from_decl `foo3, + hs ← return $ ((hs^.add h₁)^.add h₂)^.add h₃, + hs^.pp >>= tactic.trace diff --git a/tests/lean/hinst_lemmas1.lean.expected.out b/tests/lean/hinst_lemmas1.lean.expected.out new file mode 100644 index 0000000000..58814455b6 --- /dev/null +++ b/tests/lean/hinst_lemmas1.lean.expected.out @@ -0,0 +1,3 @@ +{[foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}], + [foo1, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2}}], + [foo3, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2 + ?x_2}}]}