feat(library/tactic/simp_lemmas_tactics): add simp_lemmas.drewrite

library/init/meta/simp_tactic.lean

@@ -42,13 +42,15 @@ meta def simp_lemmas.append : simp_lemmas → list expr → tactic simp_lemmas
    - 'R'     is the equivalence relation being used (e.g., 'eq', 'iff')
    - 'e'     is the expression to be "simplified"
 
-   Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e)
--/
+   Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e) -/
 meta constant simp_lemmas.rewrite_core : transparency → simp_lemmas → tactic unit → name → expr → tactic (expr × expr)
 
 meta def simp_lemmas.rewrite : simp_lemmas → tactic unit → name → expr → tactic (expr × expr) :=
 simp_lemmas.rewrite_core reducible
 
+/- (simp_lemmas.drewrite s e) tries to rewrite 'e' using only refl lemmas in 's' -/
+meta constant simp_lemmas.drewrite : simp_lemmas → expr → tactic expr
+
 /- Simplify the given expression using [simp] and [congr] lemmas.
    The first argument is a tactic to be used to discharge proof obligations.
    The second argument is the name of the relation to simplify over.

src/library/tactic/simp_lemmas_tactics.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/trace.h"
 #include "library/simp_lemmas.h"
+#include "library/constants.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
@@ -219,6 +220,31 @@ vm_obj simp_lemmas_rewrite(vm_obj const & m, vm_obj const & sls, vm_obj const &
                                     to_name(R), to_expr(e), to_tactic_state(s));
 }
 
+vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic_state const & s) {
+    LEAN_TACTIC_TRY;
+    simp_lemmas_for const * sr = sls.find(get_eq_name());
+    if (!sr) return mk_tactic_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s);
+
+    list<simp_lemma> const * srs = sr->find(e);
+    if (!srs) return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s);
+
+    type_context ctx = mk_type_context_for(s);
+
+    for (simp_lemma const & lemma : *srs) {
+        if (lemma.is_refl()) {
+            expr new_e = refl_lemma_rewrite(ctx, e, lemma);
+            if (new_e != e)
+                return mk_tactic_success(to_obj(new_e), s);
+        }
+    }
+    return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s);
+    LEAN_TACTIC_CATCH(s);
+}
+
+vm_obj simp_lemmas_drewrite(vm_obj const & sls, vm_obj const & e, vm_obj const & s) {
+    return simp_lemmas_drewrite_core(to_simp_lemmas(sls), to_expr(e), to_tactic_state(s));
+}
+
 void initialize_simp_lemmas_tactics() {
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "mk"}), simp_lemmas_mk);
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "join"}), simp_lemmas_join);
@@ -228,6 +254,7 @@ void initialize_simp_lemmas_tactics() {
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_simp_core"}),   simp_lemmas_add_simp);
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_congr_core"}),  simp_lemmas_add_congr);
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "rewrite_core"}),    simp_lemmas_rewrite);
+    DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite"}),        simp_lemmas_drewrite);
 }
 
 void finalize_simp_lemmas_tactics() {

tests/lean/run/dsimplify2.lean

@@ -0,0 +1,16 @@
+open tactic
+
+def f : nat → nat := λ x, x + 10
+
+@[simp] lemma f_lemma (x : nat) : f x = x + 10 :=
+rfl
+
+example (p : nat → Prop) (a : nat) (h : p (a + 10)) : p (f a) :=
+by do
+  t ← target,
+  S ← simp_lemmas.mk_default,
+  new_t ← dsimplify (λ e, failed) (λ e, do new_e ← S^.drewrite e, return (new_e, tt)) t,
+  expected ← to_expr `(p (a + 10)),
+  guard (new_t = expected),
+  change new_t,
+  assumption