feat(library/tactic/smt/smt_state): allow user to provide a function ("to be unfolded") in the ematch_using tactic

library/init/meta/smt/interactive.lean

@@ -151,7 +151,10 @@ private meta def add_hinst_lemma_from_name (md : transparency) (lhs_lemma : bool
 do {
   e ← resolve_name n,
   match e with
-  | expr.const n _           := do h ← hinst_lemma.mk_from_decl_core md n lhs_lemma, return $ hs^.add h
+  | expr.const n _           :=
+    (do h ← hinst_lemma.mk_from_decl_core md n lhs_lemma, return $ hs^.add h)
+    <|>
+    (do hs₁ ← mk_ematch_eqn_lemmas_for_core md n, return $ hs^.merge hs₁)
   | expr.local_const _ _ _ _ := do h ← hinst_lemma.mk_core md e lhs_lemma, return $ hs^.add h
   | _                        := fail "failed"
   end

src/library/tactic/smt/smt_state.cpp

@@ -95,10 +95,8 @@ void smt::ematch(buffer<expr_pair> & result) {
     ::lean::ematch(m_ctx, m_goal.m_em_state, m_cc, result);
 }
 
-void smt::ematch_using(hinst_lemmas const & lemmas, buffer<expr_pair> & result) {
-    lemmas.for_each([&](hinst_lemma const & lemma) {
-            ::lean::ematch(m_ctx, m_goal.m_em_state, m_cc, lemma, false, result);
-        });
+void smt::ematch_using(hinst_lemma const & lemma, buffer<expr_pair> & result) {
+    ::lean::ematch(m_ctx, m_goal.m_em_state, m_cc, lemma, false, result);
 }
 
 struct vm_smt_goal : public vm_external {
@@ -795,7 +793,18 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons
     smt S(ctx, g);
     S.internalize(target);
     buffer<expr_pair> new_instances;
-    S.ematch_using(to_hinst_lemmas(hs), new_instances);
+    to_hinst_lemmas(hs).for_each([&](hinst_lemma const & lemma) {
+            if (lemma.m_num_mvars == 0 && lemma.m_num_uvars == 0) {
+                expr type  = lemma.m_prop;
+                expr h     = lemma.m_proof;
+                std::tie(type, h) = preprocess_forward(ctx, g, type, h);
+                lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
+                           tout() << "new ground fact: " << type << "\n";);
+                S.add(type, h);
+            } else {
+                S.ematch_using(lemma, new_instances);
+            }
+        });
     for (expr_pair const & p : new_instances) {
         expr type   = p.first;
         expr proof  = p.second;

src/library/tactic/smt/smt_state.h

@@ -59,7 +59,7 @@ public:
     void internalize(expr const & e);
     void add(expr const & type, expr const & proof);
     void ematch(buffer<expr_pair> & result);
-    void ematch_using(hinst_lemmas const & lemmas, buffer<expr_pair> & result);
+    void ematch_using(hinst_lemma const & lemma, buffer<expr_pair> & result);
 
     optional<expr> get_proof(expr const & e);
     bool inconsistent() const { return m_cc.inconsistent(); }

tests/lean/run/smt_tests.lean

@@ -28,6 +28,11 @@ begin [smt]
   ematch
 end
 
+example (n : nat) : n = 0 → foo (n+1) = 2*0 :=
+begin [smt]
+  ematch_using [foo, mul_zero, zero_mul],
+end
+
 example (n : nat) : n = 0 → foo n = 0 :=
 begin [smt]
   add_eqn_lemmas foo
@@ -47,6 +52,11 @@ begin [smt]
   ematch,
 end
 
+example (n : nat) : n = 0 → boo (n+1) = 2 :=
+begin [smt]
+  ematch_using [boo, foo]
+end
+
 def r (x : nat) := x
 
 example (n : nat) : n = 0 → boo (n+1) = r 2 :=