From c9ff175cf4bec1b21c0074c8ebfb304d656ade70 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Dec 2015 09:19:58 -0800
Subject: [PATCH] fix(library/tactic/induction_tactic): fixes #893

---
 src/library/tactic/induction_tactic.cpp |  5 +++++
 tests/lean/893.hlean                    |  5 +++++
 tests/lean/893.hlean.expected.out       | 16 ++++++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 tests/lean/893.hlean
 create mode 100644 tests/lean/893.hlean.expected.out

diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index 5694ca721..6aba484be 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -243,6 +243,11 @@ class induction_tac {
                                                << pos+1 << " of major premise '" << h << "' type is an index, "
                                                << "but it occurs more than once");
                     }
+                    if (i < pos && depends_on(h_type_args[i], idx)) {
+                        throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
+                                               << pos+1 << " of major premise '" << h << "' type is an index, "
+                                               << "but it occurs in previous arguments");
+                    }
                     if (i > pos && // occurs after idx
                         std::find(idx_pos.begin(), idx_pos.end(), i) != idx_pos.end() && // it is also an index
                         is_local(h_type_args[i]) && // if it is not an index, it will fail anyway.
diff --git a/tests/lean/893.hlean b/tests/lean/893.hlean
new file mode 100644
index 000000000..c3eec150a
--- /dev/null
+++ b/tests/lean/893.hlean
@@ -0,0 +1,5 @@
+example {A : Type} (f : A → A) (a : A) (H : f a = a) : unit :=
+begin
+  induction H, -- this should raise an error
+  exact unit.star
+end
diff --git a/tests/lean/893.hlean.expected.out b/tests/lean/893.hlean.expected.out
new file mode 100644
index 000000000..4515f437f
--- /dev/null
+++ b/tests/lean/893.hlean.expected.out
@@ -0,0 +1,16 @@
+893.hlean:3:2: error:invalid 'induction' tactic, invalid 'induction' tactic, argument #3 of major premise 'H' type is an index, but it occurs in previous arguments
+proof state:
+A : Type,
+f : A → A,
+a : A,
+H : f a = a
+⊢ unit
+893.hlean:5:0: error: don't know how to synthesize placeholder
+A : Type,
+f : A → A,
+a : A,
+H : f a = a
+⊢ unit
+893.hlean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1