feat(library/blast/forward/ematch): generate new instances

src/library/blast/forward/ematch.cpp

@@ -45,6 +45,7 @@ struct ematch_branch_extension : public branch_extension {
     hi_lemma_set                                  m_new_lemmas;
     rb_map<head_index, expr_set, head_index::cmp> m_apps;
     name_set                                      m_initialized;
+    expr_set                                      m_instances;
 
     ematch_branch_extension() {}
     ematch_branch_extension(ematch_branch_extension const &) {}
@@ -111,6 +112,14 @@ struct ematch_branch_extension : public branch_extension {
     virtual void target_updated() override { collect_apps(curr_state().get_target()); }
 };
 
+/* Auxiliary proof step used to bump proof depth */
+struct noop_proof_step_cell : public proof_step_cell {
+    virtual ~noop_proof_step_cell() {}
+    virtual action_result resolve(expr const & pr) const override {
+        return action_result::solved(pr);
+    }
+};
+
 void initialize_ematch() {
     g_ext_id = register_branch_extension(new ematch_branch_extension());
 }
@@ -217,7 +226,7 @@ struct ematch_fn {
         name R; frame_kind kind; expr p, t;
         std::tie(R, kind, p, t) = head(m_state);
         m_state = tail(m_state);
-        diagnostic(env(), ios()) << ">> " << R << ", " << ppb(p) << " =?= " << ppb(t) << "\n";
+        // diagnostic(env(), ios()) << ">> " << R << ", " << ppb(p) << " =?= " << ppb(t) << "\n";
         switch (kind) {
         case DefEqOnly:
             return m_ctx->is_def_eq(p, t);
@@ -256,9 +265,21 @@ struct ematch_fn {
             }
             it = &tail(*it);
         }
-        for (expr const & mvar : lemma.m_mvars) {
+        expr new_inst  = normalize(m_ctx->instantiate_uvars_mvars(lemma.m_prop));
-            diagnostic(env(), ios()) << "[" << mvar << "] := " << ppb(m_ctx->instantiate_uvars_mvars(mvar)) << "\n";
+        if (has_idx_metavar(new_inst))
+            return; // result contains temporary metavariables
+        if (m_ext.m_instances.contains(new_inst))
+            return; // already added this instance
+        if (!m_new_instances) {
+            trace_action("ematch");
         }
+        if (is_trace_enabled()) {
+            diagnostic(env(), ios()) << "ematch_instance: " << ppb(new_inst) << "\n";
+        }
+        m_new_instances = true;
+        expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof);
+        m_ext.m_instances.insert(new_inst);
+        curr_state().mk_hypothesis(new_inst, new_proof);
     }
 
     void search(hi_lemma const & lemma) {
@@ -353,6 +374,8 @@ struct ematch_fn {
         m_ext.m_new_lemmas = hi_lemma_set();
         m_cc.inc_gmt();
         if (m_new_instances) {
+            curr_state().push_proof_step(new noop_proof_step_cell());
+            trace("");
             return action_result::new_branch();
         } else {
             return action_result::failed();

tests/lean/run/blast_ematch1.lean

@@ -0,0 +1,15 @@
+import data.nat
+open nat
+constant f : nat → nat
+constant g : nat → nat
+
+definition lemma1 [forward] : ∀ x, (:g (f x):) = x :=
+sorry
+
+set_option blast.init_depth 10
+set_option blast.inc_depth 1000
+set_option blast.subst false
+set_option blast.ematch true
+
+example (a b c : nat) : a = f b → a = f c → g a ≠ b → false :=
+by blast