From d217655a62131a634d20ae9cb97ea46d0662e8f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 May 2015 00:04:46 -0700
Subject: [PATCH] fix(kernel/quotient/quotient): bug in reduction rule for
 quot.ind

---
 src/kernel/quotient/quotient.cpp          | 9 ++++++---
 tests/lean/quot_ind_bug.lean              | 6 ++++++
 tests/lean/quot_ind_bug.lean.expected.out | 3 +++
 3 files changed, 15 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/quot_ind_bug.lean
 create mode 100644 tests/lean/quot_ind_bug.lean.expected.out

diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index 27e3ce39a..5983a9e7e 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -59,10 +59,13 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
     if (!ext.m_initialized)
         return none_ecs();
     unsigned mk_pos;
+    unsigned arg_pos;
     if (const_name(fn) == *g_quotient_lift) {
-        mk_pos = 5;
+        mk_pos  = 5;
+        arg_pos = 3;
     } else if (const_name(fn) == *g_quotient_ind) {
-        mk_pos = 4;
+        mk_pos  = 4;
+        arg_pos = 3;
     } else {
         return none_ecs();
     }
@@ -80,7 +83,7 @@ optional<pair<expr, constraint_seq>> quotient_normalizer_extension::operator()(e
     if (const_name(mk_fn) != *g_quotient_mk)
         return none_ecs();
 
-    expr const & f = args[mk_pos-2];
+    expr const & f = args[arg_pos];
     expr r = mk_app(f, app_arg(mk));
     unsigned elim_arity = mk_pos+1;
     if (args.size() > elim_arity)
diff --git a/tests/lean/quot_ind_bug.lean b/tests/lean/quot_ind_bug.lean
new file mode 100644
index 000000000..31b060c78
--- /dev/null
+++ b/tests/lean/quot_ind_bug.lean
@@ -0,0 +1,6 @@
+open quot
+
+variables {A : Type} [s : setoid A] {B : quot s → Prop} (c : ∀ (a : A), B (quot.mk a)) (a : A)
+check quot.ind c ⟦a⟧
+check c a
+eval quot.ind c ⟦a⟧
diff --git a/tests/lean/quot_ind_bug.lean.expected.out b/tests/lean/quot_ind_bug.lean.expected.out
new file mode 100644
index 000000000..f8d085512
--- /dev/null
+++ b/tests/lean/quot_ind_bug.lean.expected.out
@@ -0,0 +1,3 @@
+ind c ⟦a⟧ : B ⟦a⟧
+c a : B ⟦a⟧
+c a