feat(library/tactic/smt/hinst_lemmas): change how transparency is used to process hinst_lemmas

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

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));
 }

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, candidate_lt> 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<multi_pattern> mk_multi_patterns_using(candidate_set s, bool heuristic) {
+
         if (heuristic) {
             buffer<multi_pattern> 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<level> 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) {

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<expr>(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_lemma, hinst_lemma_cmp> hinst_lemmas;
 
 /** \brief Try to compute multipatterns for declaration \c c using the current environment configuration. */
 list<multi_pattern> 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);
 

src/util/list.h

@@ -174,6 +174,24 @@ template<typename T> inline list<T>         to_list(optional<T> const & v) { ret
 template<typename T> inline list<T>         to_list(T const * v) { return v ? to_list(*v) : list<T>(); }
 template<typename T> inline list<T>         ptr_to_list(list<T> const * l) { return l ? *l : list<T>(); }
 
+template<typename T, typename CMP>
+int cmp(list<T> const & l1, list<T> const & l2, CMP const & c) {
+    list<T> const * it1 = &l1;
+    list<T> 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<typename T> inline std::ostream & operator<<(std::ostream & out, list<T> const & l) {
     out << "(";
     bool first = true;

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

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}}]}