From 1b864a838febac5d8048b51f67281f1cc6615a16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jun 2015 13:07:02 -0700
Subject: [PATCH] fix(library/tactic/induction_tactic.cpp): condition for
 checking whether 'induction' tatic is applicable or not

fixes #690
---
 src/library/tactic/induction_tactic.cpp | 11 ++++++++++-
 tests/lean/690.hlean                    | 12 ++++++++++++
 tests/lean/690.hlean.expected.out       | 21 +++++++++++++++++++++
 3 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/690.hlean
 create mode 100644 tests/lean/690.hlean.expected.out

diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index d444fe0f2..fa997d429 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -228,7 +228,8 @@ class induction_tac {
                 }
             }
             buffer<expr> indices;
-            for (unsigned pos : rec_info.get_indices_pos()) {
+            list<unsigned> const & idx_pos = rec_info.get_indices_pos();
+            for (unsigned pos : idx_pos) {
                 if (pos >= h_type_args.size()) {
                     throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed");
                 }
@@ -243,6 +244,14 @@ class induction_tac {
                                                << pos+1 << " of major premise '" << h << "' type is an index, "
                                                << "but it occurs more than once");
                     }
+                    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.
+                        depends_on(mlocal_type(idx), h_type_args[i])) {
+                        throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
+                                               << pos+1 << " of major premise '" << h << "' type is an index, "
+                                               << "but its type depends on the index at position #" << i+1);
+                    }
                 }
                 indices.push_back(idx);
             }
diff --git a/tests/lean/690.hlean b/tests/lean/690.hlean
new file mode 100644
index 000000000..db3357b8a
--- /dev/null
+++ b/tests/lean/690.hlean
@@ -0,0 +1,12 @@
+-- HoTT
+import types.sigma
+open sigma sigma.ops eq
+definition dpair_sigma_eq {A : Type} {B : A → Type} {u v : Σa, B a} (p : u.1 = v.1) (q : u.2 =[p] v.2)
+  : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩ :=
+begin
+  induction u with u₁ u₂,
+  induction v with v₁ v₂,
+  esimp at q,
+  induction q, -- Should fail here since index p depends one index v₂
+  reflexivity
+end
diff --git a/tests/lean/690.hlean.expected.out b/tests/lean/690.hlean.expected.out
new file mode 100644
index 000000000..4d05275fd
--- /dev/null
+++ b/tests/lean/690.hlean.expected.out
@@ -0,0 +1,21 @@
+690.hlean:10:2: error:invalid 'induction' tactic, invalid 'induction' tactic, argument #6 of major premise 'q' type is an index, but its type depends on the index at position #7
+proof state:
+A : Type,
+B : A → Type,
+u₁ : A,
+u₂ : B u₁,
+v₁ : A,
+v₂ : B v₁,
+p : ⟨u₁, u₂⟩.1 = ⟨v₁, v₂⟩.1,
+q : u₂ =[ p ] v₂
+⊢ ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩
+690.hlean:12:0: error: don't know how to synthesize placeholder
+A : Type,
+B : A → Type,
+u v : Σ (a : A), B a,
+p : u.1 = v.1,
+q : u.2 =[ p ] v.2
+⊢ ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩
+690.hlean:12:0: error: failed to add declaration 'dpair_sigma_eq' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1