feat(library/tactic): add tactic.defeq_simp

library/init/meta/tactic.lean

@@ -102,9 +102,11 @@ meta_constant subst         : name → tactic unit
 meta_constant exact         : expr → tactic unit
 /- Elaborate the given quoted expression with respect to the current main goal. -/
 meta_constant to_expr       : qexpr → tactic expr
-/- Try to create an instance of the given type class -/
+/- Try to create an instance of the given type class. -/
 meta_constant mk_instance   : expr → tactic expr
-
+/- Simplify the given expression using [defeq] lemmas.
+   The resulting expression is definitionally equal to the input. -/
+meta_constant defeq_simp    : expr → tactic expr
 open list nat
 
 meta_definition intros : tactic unit :=

src/library/defeq_simplifier.cpp

@@ -215,6 +215,7 @@ class defeq_simplify_fn {
     }
 
     expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
+        type_context::scope scope(m_ctx);
         m_ctx.set_tmp_mode(sl.get_num_umeta(), sl.get_num_emeta());
         if (!m_ctx.is_def_eq(e, sl.get_lhs())) return e;
 
@@ -288,7 +289,10 @@ public:
 
     ~defeq_simplify_fn() {}
 
-    expr operator()(expr const & e)  { return defeq_simplify(e); }
+    expr operator()(expr const & e)  {
+        scope_trace_env scope(env(), m_ctx);
+        return defeq_simplify(e);
+    }
 };
 
 /* Setup and teardown */

src/library/tactic/tactic_state.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/type_context.h"
 #include "library/pp_options.h"
+#include "library/defeq_simplifier.h"
 #include "library/trace.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
@@ -334,6 +335,19 @@ vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & s) {
     return mk_tactic_success(qe, to_tactic_state(s));
 }
 
+vm_obj tactic_defeq_simp(vm_obj const & e, vm_obj const & s0) {
+    tactic_state const & s   = to_tactic_state(s0);
+    try {
+        metavar_context mctx_tmp   = s.mctx();
+        type_context ctx           = mk_type_context_for(s, mctx_tmp);
+        defeq_simp_lemmas lemmas   = get_defeq_simp_lemmas(s.env());
+        expr new_e                 = defeq_simplify(ctx, lemmas, to_expr(e));
+        return mk_tactic_success(to_obj(new_e), s);
+    } catch (exception & e) {
+        return mk_tactic_exception(e, s);
+    }
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),         tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);
@@ -349,6 +363,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "local_context"}),     tactic_local_context);
     DECLARE_VM_BUILTIN(name({"tactic", "num_goals"}),         tactic_num_goals);
     DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}),           tactic_to_expr);
+    DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}),        tactic_defeq_simp);
 }
 
 void finalize_tactic_state() {

tests/lean/defeq1.lean

@@ -0,0 +1,12 @@
+open nat tactic
+variables {A : Type}
+
+definition succ_eq_add [defeq] (n : nat) : succ n = n + 1 :=
+rfl
+
+example (n m : nat) (H : succ (succ n) = succ m) : true :=
+by do H  ← get_local "H",
+      t  ← infer_type H,
+      t' ← defeq_simp t,
+      trace_expr t',
+      exact (expr.const "trivial" [])

tests/lean/defeq1.lean.expected.out

@@ -0,0 +1 @@
+n + 1 + 1 = m + 1