From ea19bb40dd3fcf7895d010263ac98a813eded2db Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Wed, 6 Jul 2016 09:21:08 -0700
Subject: [PATCH] feat(simplifier): detect refl proofs from simp extensions

---
 src/library/tactic/simplifier/simplifier.cpp |  7 +++--
 tests/lean/run/simp_ext_refl.lean            | 32 ++++++++++++++++++++
 2 files changed, 37 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/simp_ext_refl.lean

diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp
index a398441ec8..b884edb156 100644
--- a/src/library/tactic/simplifier/simplifier.cpp
+++ b/src/library/tactic/simplifier/simplifier.cpp
@@ -514,8 +514,11 @@ simp_result simplifier::simplify_extensions(expr const & _e) {
             expr proof = m_tctx.instantiate_mvars(goal_mvar);
             lean_trace(name({"simplifier", "extensions"}),
                        tout() << proof << " : " << e << " " << m_rel << " " << result << "\n";);
-            // TODO(dhs): detect refl proofs
-            r = join(r, simp_result(result, proof));
+            if (is_app_of(proof, get_eq_refl_name(), 2) || is_app_of(proof, get_rfl_name(), 2)) {
+                r.update(result);
+            } else {
+                r = join(r, simp_result(result, proof));
+            }
         } else {
             lean_trace(name({"simplifier", "extensions"}),
                        tout() << "extension failed on goal " << goal_type << "\n";);
diff --git a/tests/lean/run/simp_ext_refl.lean b/tests/lean/run/simp_ext_refl.lean
new file mode 100644
index 0000000000..a0774e9309
--- /dev/null
+++ b/tests/lean/run/simp_ext_refl.lean
@@ -0,0 +1,32 @@
+open tactic
+
+constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z)
+attribute Hg [simp]
+
+definition f (a : A) := y
+lemma f.def : ∀ (a), f a = y := λ a, rfl
+
+meta_definition simp_f_to_y : tactic unit := mk_eq_simp_ext $
+  λ e, if expr.get_app_num_args e = 1
+       then do res ← mk_const "y",
+               pf ← mk_app "rfl" [e],
+               return (res, pf)
+       else fail "expected f applied to one arg"
+
+meta_definition simp_f_to_y₂ : tactic unit := mk_eq_simp_ext $
+  λ e, if expr.get_app_num_args e = 1
+       then do res ← mk_const "y",
+               pf ← mk_app ("f" <.> "def") [expr.app_arg e],
+               return (res, pf)
+       else fail "expected f applied to one arg"
+
+register_simp_ext f simp_f_to_y
+
+definition foo : g (f x) = z := by simp >> triv
+
+register_simp_ext f simp_f_to_y₂
+
+definition foo₂ : g (f x) = z := by simp >> triv
+
+print foo
+print foo₂