feat(library/blast/forward): display lemma name when printing instance

src/library/blast/forward/ematch.cpp

@@ -424,7 +424,7 @@ struct ematch_fn {
         if (!m_new_instances) {
             trace_action("ematch");
         }
-        lean_trace_ematch(tout() << "instance: " << ppb(new_inst) << "\n";);
+        lean_trace_ematch(tout() << "instance [" << ppb(lemma.m_expr) << "]: " << ppb(new_inst) << "\n";);
         m_new_instances = true;
         expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof);
         curr_state().mk_hypothesis(new_inst, new_proof);

src/library/blast/forward/pattern.cpp

@@ -598,6 +598,7 @@ struct mk_hi_lemma_fn {
         r.m_is_inst_implicit = to_list(inst_implicit_flags);
         r.m_prop             = m_ctx.infer(proof);
         r.m_proof            = proof;
+        r.m_expr             = m_H;
         return r;
     }
 };

src/library/blast/forward/pattern.h

@@ -40,6 +40,8 @@ struct hi_lemma {
     list<expr>           m_mvars;
     expr                 m_prop;
     expr                 m_proof;
+    /* term that was used to generate hi_lemma, it is only used for tracing and profiling */
+    expr                 m_expr;
 };
 
 inline bool operator==(hi_lemma const & l1, hi_lemma const & l2) { return l1.m_prop == l2.m_prop; }