feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic

see discussion at:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc

src/library/tactic/inversion_tactic.cpp

@@ -212,12 +212,12 @@ class inversion_tac {
         - non_deps : hypotheses that do not depend on H
         - deps     : hypotheses that depend on H (directly or indirectly)
     */
-    void split_deps(buffer<expr> const & hyps, expr const & H, buffer<expr> & non_deps, buffer<expr> & deps) {
+    void split_deps(buffer<expr> const & hyps, expr const & H, buffer<expr> & non_deps, buffer<expr> & deps, bool clear_H = false) {
         for (expr const & hyp : hyps) {
             expr const & hyp_type = mlocal_type(hyp);
             if (depends_on(hyp_type, H) || std::any_of(deps.begin(), deps.end(), [&](expr const & dep) { return depends_on(hyp_type, dep); })) {
                 deps.push_back(hyp);
-            } else {
+            } else if (hyp != H || !clear_H) {
                 non_deps.push_back(hyp);
             }
         }
@@ -798,7 +798,8 @@ class inversion_tac {
             // Remark: A is the type of lhs and rhs
             hyps.pop_back(); // remove processed equality
             buffer<expr> non_deps, deps;
-            split_deps(hyps, rhs, non_deps, deps);
+            bool clear_rhs = true;
+            split_deps(hyps, rhs, non_deps, deps, clear_rhs);
             if (deps.empty() && !depends_on(g_type, rhs)) {
                 // eq.rec is not necessary
                 buffer<expr> & new_hyps = non_deps;

tests/lean/cases_failure.hlean.expected.out

@@ -1,7 +1,7 @@
 cases_failure.hlean:11:2: error:invalid 'cases' tactic, unification failed
 auxiliary goal at time of failure
   A : Type,
-  x y z : A,
+  z : A,
   b r t l : z = z,
   s : square t b l r,
   e_3 : z = z

tests/lean/cases_tac.lean

@@ -0,0 +1,19 @@
+inductive foo {A : Type} : A → Type :=
+mk : Π a : A, foo a
+
+example (A : Type) (B : A → Type) (a : A) (H : foo a) (Hb : B a) : A :=
+begin
+  cases H,
+  state,
+  assumption
+end
+
+inductive foo₂ {A : Type} : A → A → Type :=
+mk : Π a b : A, foo₂ a b
+
+example (A : Type) (B : A → Type) (f : A → A) (a : A) (H : foo₂ (f a) a) (Hb : H = H) (Hc : a = a) : A :=
+begin
+  cases H with [c, d],
+  state,
+  exact d
+end

tests/lean/cases_tac.lean.expected.out

@@ -0,0 +1,14 @@
+cases_tac.lean:7:2: proof state
+A : Type,
+B : A → Type,
+a_1 : A,
+Hb : B a_1
+⊢ A
+cases_tac.lean:17:2: proof state
+A : Type,
+B : A → Type,
+f : A → A,
+d : A,
+Hc : d = d,
+Hb : foo₂.mk (f d) d = foo₂.mk (f d) d
+⊢ A