From e1dc18f6b6aad5dabc13cb9b93978c32f31e7939 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 May 2015 17:48:08 -0700
Subject: [PATCH] fix(library/tactic/inversion_tactic): check whether
 eliminator can only eliminate to Prop

fixes #571
---
 src/library/tactic/inversion_tactic.cpp |  8 +++++++-
 tests/lean/571.lean                     |  7 +++++++
 tests/lean/571.lean.expected.out        | 13 +++++++++++++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/571.lean
 create mode 100644 tests/lean/571.lean.expected.out

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index b9dd010d3..29375dec3 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -379,10 +379,16 @@ class inversion_tac {
         name const & I_name = const_name(I);
         expr g_type         = g.get_type();
         expr cases_on;
+        level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
         if (m_cases_on_decl.get_num_univ_params() != m_I_decl.get_num_univ_params()) {
-            level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
             cases_on     = mk_constant({I_name, "cases_on"}, cons(g_lvl, const_levels(I)));
         } else {
+            if (!is_zero(g_lvl)) {
+                if (m_throw_tactic_exception)
+                    throw tactic_exception(sstream() << "invalid 'cases' tactic, '" << const_name(I) << "' can only eliminate to Prop");
+                else
+                    throw inversion_exception();
+            }
             cases_on     = mk_constant({I_name, "cases_on"}, const_levels(I));
         }
         // add params
diff --git a/tests/lean/571.lean b/tests/lean/571.lean
new file mode 100644
index 000000000..2b646fd9c
--- /dev/null
+++ b/tests/lean/571.lean
@@ -0,0 +1,7 @@
+open nat
+variables (P : ℕ → Prop)
+
+example (H : ∃n, P n) : ℕ :=
+begin
+  cases H with n p,
+end
diff --git a/tests/lean/571.lean.expected.out b/tests/lean/571.lean.expected.out
new file mode 100644
index 000000000..0d9564630
--- /dev/null
+++ b/tests/lean/571.lean.expected.out
@@ -0,0 +1,13 @@
+571.lean:6:2: error:invalid 'cases' tactic, 'Exists' can only eliminate to Prop
+proof state:
+P : ℕ → Prop,
+H : ∃ (n : ℕ), P n
+⊢ ℕ
+571.lean:7:0: error: don't know how to synthesize placeholder
+P : ℕ → Prop,
+H : ∃ (n : ℕ), P n
+⊢ ℕ
+571.lean:7:0: error: failed to add declaration '14.1' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (P : …) (H : …),
+    ?M_1