From a0d650d9cc5cfd446f98e52bba92d7dc46ab997a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Nov 2014 09:36:41 -0800
Subject: [PATCH] fix(library/tactic/inversion_tactic): complete 'deletion'
 transition

---
 src/library/tactic/inversion_tactic.cpp | 13 +++++++------
 tests/lean/inv_del.lean                 | 16 ++++++++++++++++
 tests/lean/inv_del.lean.expected.out    | 10 ++++++++++
 3 files changed, 33 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/inv_del.lean
 create mode 100644 tests/lean/inv_del.lean.expected.out

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index 67d8ff207..d80420cb7 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -273,11 +273,6 @@ class inversion_tac {
         }
     }
 
-    goal clear_eq(goal g) {
-        // TODO(Leo): delete last hypothesis
-        return g;
-    }
-
     // Split hyps into two "telescopes".
     //   - non_deps : hypotheses that do not depend on rhs
     //   - deps     : hypotheses that depend on rhs (directly or indirectly)
@@ -308,7 +303,13 @@ class inversion_tac {
         constraint_seq cs;
         if (m_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) {
             // deletion transition: t == t
-            return unify_eqs(clear_eq(g), neqs-1);
+            hyps.pop_back(); // remove t == t equality
+            expr new_type = g.get_type();
+            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
+            goal new_g(new_meta, new_type);
+            expr val      = g.abstract(new_meta);
+            m_subst.assign(g.get_name(), val);
+            return unify_eqs(new_g, neqs-1);
         }
         buffer<expr> lhs_args, rhs_args;
         expr const & lhs_fn = get_app_args(lhs, lhs_args);
diff --git a/tests/lean/inv_del.lean b/tests/lean/inv_del.lean
new file mode 100644
index 000000000..3c6c036fb
--- /dev/null
+++ b/tests/lean/inv_del.lean
@@ -0,0 +1,16 @@
+import logic data.nat.basic
+open nat
+
+inductive vec (A : Type) : nat → Type :=
+vnil : vec A zero,
+vone : A → vec A (succ zero),
+vtwo : A → A → vec A (succ (succ zero))
+
+namespace vec
+
+  theorem eone {A : Type} {P : vec A (succ zero) → Type} (H : Π a, P (vone a)) (v : vec A (succ zero)) : P v :=
+  begin
+    cases v,
+    -- apply (H a)
+  end
+end vec
diff --git a/tests/lean/inv_del.lean.expected.out b/tests/lean/inv_del.lean.expected.out
new file mode 100644
index 000000000..b2e3f5544
--- /dev/null
+++ b/tests/lean/inv_del.lean.expected.out
@@ -0,0 +1,10 @@
+inv_del.lean:15:2: error: unsolved subgoals
+A : Type,
+P : vec A (succ zero) → Type,
+H : Π (a : A), P (vone a),
+v : vec A (succ zero),
+a : A
+⊢ P (vone a)
+inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables
+  λ (A : Type) (P : vec A (succ zero) → Type) (H : Π (a : A), P (vone a)) (v : vec A (succ zero)),
+    ?M_1