fix(library/tactic/inversion_tactic): complete 'deletion' transition

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);

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

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