From 6ba42bb7bcff8403f73889288ead4a119b8b643c Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 16 Nov 2015 16:40:54 -0800
Subject: [PATCH] test(simplifier11.lean): add rule for (not P)

---
 src/library/blast/simplifier.cpp | 11 +++++++++++
 tests/lean/simplifier11.lean     |  4 ++++
 2 files changed, 15 insertions(+)

diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index c18c6af137..df2b34ad0c 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -191,6 +191,9 @@ class simplifier {
         simp_rule_sets srss = _srss;
         for (unsigned i = 0; i < ls.size(); i++) {
             expr & l = ls[i];
+            if (m_trace) {
+                ios().get_diagnostic_channel() << "Local: " << l << " : " << mlocal_type(l) << "\n";
+            }
             tmp_type_context tctx(env(), ios());
             srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
         }
@@ -593,6 +596,14 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
 result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
 
+    if (m_trace) {
+        expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
+        expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
+        ios().get_diagnostic_channel()
+            << "TRYREW(" << sr.get_id() << ") "
+            << "[" << new_lhs << " =?= " << new_rhs << "]\n";
+    }
+
     if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
 
     if (m_trace) {
diff --git a/tests/lean/simplifier11.lean b/tests/lean/simplifier11.lean
index 47e64154b4..4f14e25c2c 100644
--- a/tests/lean/simplifier11.lean
+++ b/tests/lean/simplifier11.lean
@@ -1,6 +1,10 @@
 -- Conditional congruence
 import logic.connectives logic.quantifiers
 
+-- TODO(dhs): either add this to the library or add a `ceqv` rule for
+-- ¬ c ==> (¬ c ↔ true) in addition to (c ↔ false)
+lemma not_workaround [simp] : ∀ (P : Prop), (P ↔ false) → (¬ P ↔ true) := sorry
+
 namespace if_congr
 constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
           {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v)