fix(library/tactic/induction_tactic): fixes #893

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.

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

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