From 6bbe72190dee0b083035b4afe215bef3dc4d2eb4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Dec 2015 14:21:30 -0800
Subject: [PATCH] fix(library/congr_lemma_manager): bug in congruence lemma
 generator

---
 src/library/congr_lemma_manager.cpp          |  3 ++-
 tests/lean/congr_lemma_bug.lean              |  6 ++++++
 tests/lean/congr_lemma_bug.lean.expected.out |  4 ++++
 tests/lean/run/blast_congr_bug.lean          | 21 ++++++++++++++++++++
 4 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/congr_lemma_bug.lean
 create mode 100644 tests/lean/congr_lemma_bug.lean.expected.out
 create mode 100644 tests/lean/run/blast_congr_bug.lean

diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp
index 61d7a4002..512656194 100644
--- a/src/library/congr_lemma_manager.cpp
+++ b/src/library/congr_lemma_manager.cpp
@@ -320,7 +320,8 @@ public:
             if (std::find(result_deps.begin(), result_deps.end(), i) != result_deps.end()) {
                 kinds[i] = congr_arg_kind::Fixed;
             } else if (pinfos[i].is_subsingleton()) {
-                if (empty(pinfos[i].get_dependencies()))
+                // See comment at mk_congr.
+                if (!pinfos[i].is_prop() && pinfos[i].is_dep())
                     kinds[i] = congr_arg_kind::Fixed;
                 else
                     kinds[i] = congr_arg_kind::Cast;
diff --git a/tests/lean/congr_lemma_bug.lean b/tests/lean/congr_lemma_bug.lean
new file mode 100644
index 000000000..155a135fd
--- /dev/null
+++ b/tests/lean/congr_lemma_bug.lean
@@ -0,0 +1,6 @@
+constant P : Type₁
+constant P_sub : subsingleton P
+attribute P_sub [instance]
+constant q : P → Prop
+
+#congr q
diff --git a/tests/lean/congr_lemma_bug.lean.expected.out b/tests/lean/congr_lemma_bug.lean.expected.out
new file mode 100644
index 000000000..0ccf4e708
--- /dev/null
+++ b/tests/lean/congr_lemma_bug.lean.expected.out
@@ -0,0 +1,4 @@
+[cast]
+λ (a a_1 : P), eq.trans (eq.refl (q a)) (congr (eq.refl q) (subsingleton.elim a a_1))
+:
+∀ (a a_1 : P), q a = q a_1
diff --git a/tests/lean/run/blast_congr_bug.lean b/tests/lean/run/blast_congr_bug.lean
new file mode 100644
index 000000000..fda591fc5
--- /dev/null
+++ b/tests/lean/run/blast_congr_bug.lean
@@ -0,0 +1,21 @@
+constant P : Type₁
+constant P_sub : subsingleton P
+attribute P_sub [instance]
+constant q : P → Prop
+
+section
+set_option blast.simp true
+set_option blast.cc   false
+
+example (h₁ h₂ : P) : q h₁ = q h₂ :=
+by blast
+end
+
+
+section
+set_option blast.simp false
+set_option blast.cc   true
+
+example (h₁ h₂ : P) : q h₁ = q h₂ :=
+by blast
+end