feat(library/tactic/smt/smt_state): add tactic for adding equational lemmas for a definition

library/init/meta/smt/interactive.lean

@@ -129,5 +129,20 @@ add_lemma_pexprs reducible ff l
 meta def add_lhs_lemma (l : qexpr_list_or_qexpr0) : smt_tactic unit :=
 add_lemma_pexprs reducible tt l
 
+private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt_tactic unit
+| []      := return ()
+| (c::cs) := do
+  e ← resolve_name c,
+  match e with
+  | expr.const n _           := add_ematch_eqn_lemmas_for_core md n >> add_eqn_lemmas_for_core cs
+  | _                        := fail $ "'" ++ to_string c ++ "' is not a constant"
+  end
+
+meta def add_eqn_lemmas_for (ids : raw_ident_list) : smt_tactic unit :=
+add_eqn_lemmas_for_core reducible ids
+
+meta def add_eqn_lemmas (ids : raw_ident_list) : smt_tactic unit :=
+add_eqn_lemmas_for ids
+
 end interactive
 end smt_tactic

library/init/meta/smt/smt_tactic.lean

@@ -103,6 +103,7 @@ meta constant close                           : smt_tactic unit
 meta constant ematch_core                     : (expr → bool) → smt_tactic unit
 meta constant add_ematch_lemma_core           : transparency → bool → expr → smt_tactic unit
 meta constant add_ematch_lemma_from_decl_core : transparency → bool → name → smt_tactic unit
+meta constant add_ematch_eqn_lemmas_for_core  : transparency → name → smt_tactic unit
 meta constant to_cc_state                     : smt_tactic cc_state
 meta constant to_em_state                     : smt_tactic ematch_state
 meta constant preprocess                      : expr → smt_tactic (expr × expr)
@@ -262,6 +263,21 @@ meta def get_refuted_facts : smt_tactic (list expr) :=
 do cc ← to_cc_state,
    return $ cc^.eqc_of expr.mk_false
 
+meta def add_ematch_lemma : expr → smt_tactic unit :=
+add_ematch_lemma_core reducible ff
+
+meta def add_ematch_lhs_lemma : expr → smt_tactic unit :=
+add_ematch_lemma_core reducible tt
+
+meta def add_ematch_lemma_from_decl : name → smt_tactic unit :=
+add_ematch_lemma_from_decl_core reducible ff
+
+meta def add_ematch_lhs_lemma_from_decl : name → smt_tactic unit :=
+add_ematch_lemma_from_decl_core reducible ff
+
+meta def add_ematch_eqn_lemmas_for : name → smt_tactic unit :=
+add_ematch_eqn_lemmas_for_core reducible
+
 meta def add_lemmas_from_facts_core : list expr → smt_tactic unit
 | []      := return ()
 | (f::fs) := do

src/library/tactic/eqn_lemmas.cpp

@@ -5,9 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include "kernel/for_each_fn.h"
 #include "library/attribute_manager.h"
 #include "library/kernel_serializer.h"
 #include "library/trace.h"
+#include "library/util.h"
 #include "library/constants.h"
 #include "library/module.h"
 #include "library/tactic/eqn_lemmas.h"
@@ -93,6 +95,39 @@ void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_o
     }
 }
 
+void get_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result) {
+    name base(name(cname, "equations"), "eqn");
+    unsigned idx = 1;
+    while (true) {
+        name eqn = base.append_after(idx);
+        if (env.find(eqn)) {
+            result.push_back(eqn);
+            idx++;
+        } else {
+            break;
+        }
+    }
+}
+
+void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result) {
+    name_set visited;
+    unsigned i = result.size();
+    get_eqn_lemmas_for(env, cname, result);
+    for (; i < result.size(); i++) {
+        expr type = env.get(result[i]).get_type();
+        for_each(type, [&](expr const & e, unsigned) {
+                if (is_constant(e)) {
+                    name const & n = const_name(e);
+                    if (n != cname && is_prefix_of(cname, n) && !visited.contains(n) && is_internal_name(n)) {
+                        get_eqn_lemmas_for(env, n, result);
+                        visited.insert(n);
+                    }
+                }
+                return true;
+            });
+    }
+}
+
 bool has_eqn_lemmas(environment const & env, name const & cname) {
     eqn_lemmas_ext const & ext = get_extension(env);
     return ext.m_lemmas.contains(cname);

src/library/tactic/eqn_lemmas.h

@@ -11,6 +11,9 @@ namespace lean {
 environment add_eqn_lemma(environment const & env, name const & eqn_lemma);
 bool has_eqn_lemmas(environment const & env, name const & cname);
 void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer<simp_lemma> & result);
+void get_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result);
+void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer<name> & result);
+
 void initialize_eqn_lemmas();
 void finalize_eqn_lemmas();
 }

src/library/tactic/smt/smt_state.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/tactic/revert_tactic.h"
 #include "library/tactic/dsimplify.h"
 #include "library/tactic/simplify.h"
+#include "library/tactic/eqn_lemmas.h"
 #include "library/tactic/change_tactic.h"
 #include "library/tactic/smt/congruence_tactics.h"
 #include "library/tactic/smt/ematch.h"
@@ -706,6 +707,36 @@ vm_obj smt_tactic_add_ematch_lemma_from_decl_core(vm_obj const & md, vm_obj cons
     LEAN_TACTIC_CATCH(ts);
 }
 
+vm_obj smt_tactic_add_ematch_eqn_lemmas_for_core(vm_obj const & md, vm_obj const & decl_name, vm_obj const & ss, vm_obj const & _ts) {
+    tactic_state ts = to_tactic_state(_ts);
+    if (is_nil(ss)) return mk_smt_state_empty_exception(ts);
+    lean_assert(ts.goals());
+    LEAN_TACTIC_TRY;
+    type_context ctx    = mk_type_context_for(ts);
+    smt_goal g          = to_smt_goal(head(ss));
+    smt S(ctx, g);
+    buffer<name> eqns;
+    get_ext_eqn_lemmas_for(ts.env(), to_name(decl_name), eqns);
+    if (eqns.empty())
+        return mk_tactic_exception(sstream() << "tactic failed, '" << to_name(decl_name) << "' does not have equation lemmas", ts);
+    for (name const & eqn : eqns) {
+        declaration eqn_decl = ctx.env().get(eqn);
+        if (eqn_decl.get_num_univ_params() == 0 && !is_pi(ctx.relaxed_whnf(ctx.env().get(eqn).get_type()))) {
+            expr h            = mk_constant(eqn);
+            expr type         = ctx.infer(h);
+            std::tie(type, h) = preprocess_forward(ctx, g, type, h);
+            S.add(type, h);
+        } else {
+            hinst_lemma lemma   = mk_hinst_lemma(ctx, to_transparency_mode(md), eqn, true);
+            g.add_lemma(lemma);
+        }
+    }
+    vm_obj new_ss       = mk_vm_cons(to_obj(g), tail(ss));
+    tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx());
+    return mk_smt_tactic_success(new_ss, new_ts);
+    LEAN_TACTIC_CATCH(ts);
+}
+
 vm_obj smt_tactic_to_cc_state(vm_obj const & ss, vm_obj const & ts) {
     if (is_nil(ss)) return mk_smt_state_empty_exception(ts);
     return mk_smt_tactic_success(to_obj(to_smt_goal(head(ss)).get_cc_state()), ss, ts);
@@ -745,6 +776,7 @@ void initialize_smt_state() {
     DECLARE_VM_BUILTIN(name({"smt_tactic", "preprocess"}),                       smt_tactic_preprocess);
     DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_lemma_core"}),            smt_tactic_add_ematch_lemma_core);
     DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_lemma_from_decl_core"}),  smt_tactic_add_ematch_lemma_from_decl_core);
+    DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_eqn_lemmas_for_core"}),   smt_tactic_add_ematch_eqn_lemmas_for_core);
 }
 
 void finalize_smt_state() {

tests/lean/run/smt_tests.lean

@@ -4,8 +4,6 @@ constant p    : nat → nat → Prop
 constants a b : nat
 constant h    : p (a + 1 * b + 0) (a + b)
 
-set_option trace.app_builder true
-
 open tactic smt_tactic
 
 def ex : p (a + b) (a + b) :=
@@ -18,3 +16,33 @@ begin [smt]
     exact new_h
   }
 end
+
+def foo : nat → nat
+| 0     := 0
+| (n+1) := 2*n
+
+example (n : nat) : n = 0 → foo (n+1) = 2*0 :=
+begin [smt]
+  add_lemma [mul_zero, zero_mul],
+  add_eqn_lemmas foo,
+  ematch
+end
+
+example (n : nat) : n = 0 → foo n = 0 :=
+begin [smt]
+  add_eqn_lemmas foo
+end
+
+def boo : nat → nat
+| 0     := 1
+| (n+1) :=
+  match foo n with
+  | 0 := 2
+  | _ := 3
+  end
+
+example (n : nat) : n = 0 → boo (n+1) = 2 :=
+begin [smt]
+  add_eqn_lemmas boo foo,
+  ematch,
+end