From 0d8e62ed4071a2f7da7699f5ce4c76dff6713d1f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 17 Aug 2017 18:55:53 +0200
Subject: [PATCH] feat(library/tactic/simp_lemmas): add both equational lemmas
 and the definition itself

---
 src/library/tactic/simp_lemmas.cpp | 20 ++++++++++----------
 src/library/tactic/simp_lemmas.h   |  4 ++++
 2 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 8ff545a8da..2982704e99 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -678,10 +678,6 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
                             expr const & e, expr const & h, unsigned priority) {
     lean_assert(ctx.in_tmp_mode());
     list<expr_pair> ceqvs   = to_ceqvs(ctx, id, e, h);
-    if (is_nil(ceqvs)) {
-        report_failure(sstream() << "invalid simplification lemma '" << id << "' : " << e);
-        return s;
-    }
     environment const & env = ctx.env();
     simp_lemmas new_s = s;
     for (expr_pair const & p : ceqvs) {
@@ -779,16 +775,20 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
 /* Extended version. If cname is a definition with equational lemmas associated to it, then
    add the equational lemmas. */
 static simp_lemmas ext_add_core(type_context & ctx, simp_lemmas const & s, name const & cname, unsigned priority) {
+    simp_lemmas r = s;
+
+    // equational lemmas
     buffer<name> eqn_lemmas;
     get_ext_eqn_lemmas_for(ctx.env(), cname, eqn_lemmas);
-    if (eqn_lemmas.empty())
-        return add_core(ctx, s, cname, priority);
-    expr type = ctx.env().get(cname).get_type();
-    if (ctx.is_prop(type))
-        return add_core(ctx, s, cname, priority);
-    simp_lemmas r = s;
     for (name const & eqn_lemma : eqn_lemmas)
         r = add_core(ctx, r, eqn_lemma, priority);
+
+    // the definition itself
+    r = add_core(ctx, r, cname, priority);
+
+    if (is_eqp(r, s)) {
+        report_failure(sstream() << "invalid simplification lemma '" << cname << "'");
+    }
     return r;
 }
 
diff --git a/src/library/tactic/simp_lemmas.h b/src/library/tactic/simp_lemmas.h
index 4ff4f5724b..582ed82983 100644
--- a/src/library/tactic/simp_lemmas.h
+++ b/src/library/tactic/simp_lemmas.h
@@ -119,6 +119,10 @@ public:
     format pp_simp(formatter const & fmt) const;
     format pp_congr(formatter const & fmt) const;
     format pp(formatter const & fmt) const;
+
+    friend bool is_eqp(simp_lemmas const & a, simp_lemmas const & b) {
+        return is_eqp(a.m_sets, b.m_sets);
+    }
 };
 
 typedef unsigned simp_lemmas_token;