From e6672b958ff4f24bb3e4e76b89c2e16183f40a0e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Dec 2014 19:08:56 -0800
Subject: [PATCH] fix(library/tactic/inversion_tactic): add missing case

---
 library/init/logic.lean                 |  2 +-
 src/library/tactic/inversion_tactic.cpp | 19 +++++++++++++++++--
 tests/lean/run/inv_bug.lean             | 17 ++++++++++++-----
 tests/lean/run/inv_bug2.lean            | 13 +++++++++++++
 4 files changed, 43 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/inv_bug2.lean

diff --git a/library/init/logic.lean b/library/init/logic.lean
index fda94906fc..d006c5a9e8 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -75,7 +75,7 @@ namespace eq
   theorem trans (H₁ : a = b) (H₂ : b = c) : a = c :=
   subst H₂ H₁
 
-  theorem symm (H : a = b) : b = a :=
+  definition symm (H : a = b) : b = a :=
   subst H (refl a)
 
   namespace ops
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index f111132fae..875a4d8e00 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -301,7 +301,7 @@ class inversion_tac {
         buffer<expr> hyps;
         g.get_hyps(hyps);
         lean_assert(!hyps.empty());
-        expr const & eq  = hyps.back();
+        expr eq = hyps.back();
         buffer<expr> eq_args;
         get_app_args(mlocal_type(eq), eq_args);
         expr const & A   = m_tc->whnf(eq_args[0]).first;
@@ -388,7 +388,8 @@ class inversion_tac {
             new_hyps.append(non_deps);
             expr new_type       = instantiate(abstract(deps_g_type, rhs), lhs);
             for (unsigned i = 0; i < deps.size(); i++) {
-                expr new_hyp = mk_local(m_ngen.next(), binding_name(new_type), binding_domain(new_type), binding_info(new_type));
+                expr new_hyp = mk_local(m_ngen.next(), binding_name(new_type), binding_domain(new_type),
+                                        binding_info(new_type));
                 new_hyps.push_back(new_hyp);
                 new_type     = instantiate(binding_body(new_type), new_hyp);
             }
@@ -400,6 +401,20 @@ class inversion_tac {
             expr val            = g.abstract(mk_app(eq_rec, deps));
             assign(g.get_name(), val);
             return unify_eqs(new_g, neqs-1);
+        } else if (is_local(lhs)) {
+            // flip equation and reduce to previous case
+            hyps.pop_back(); // remove processed equality
+            expr symm_eq  = mk_eq(rhs, lhs).first;
+            expr new_type = mk_arrow(symm_eq, g_type);
+            expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
+            expr new_meta = mk_app(new_mvar, hyps);
+            goal new_g(new_meta, new_type);
+            level eq_symm_lvl = sort_level(m_tc->ensure_type(A).first);
+            expr symm_pr  = mk_constant(name{"eq", "symm"}, {eq_symm_lvl});
+            symm_pr       = mk_app(symm_pr, A, lhs, rhs, eq);
+            expr val      = g.abstract(mk_app(new_meta, symm_pr));
+            assign(g.get_name(), val);
+            return unify_eqs(new_g, neqs);
         }
         // unification failed
         return optional<goal>(g);
diff --git a/tests/lean/run/inv_bug.lean b/tests/lean/run/inv_bug.lean
index 6d5d9fa5f7..9ddd36931a 100644
--- a/tests/lean/run/inv_bug.lean
+++ b/tests/lean/run/inv_bug.lean
@@ -9,9 +9,16 @@ odd_succ_of_even : ∀ {a}, even a → odd (succ a)
 
 example : even 1 → false :=
 begin
-  intro H,
-  cases H with (a, ho),
-  assert (Hz : odd zero),
-  apply (a_eq ▸ ho),
-  inversion Hz
+  intro He1,
+  cases He1 with (a, Ho0),
+  cases Ho0
+end
+
+example : even 3 → false :=
+begin
+  intro He3,
+  cases He3 with (a, Ho2),
+  cases Ho2 with (a, He1),
+  cases He1 with (a, Ho0),
+  cases Ho0
 end
diff --git a/tests/lean/run/inv_bug2.lean b/tests/lean/run/inv_bug2.lean
new file mode 100644
index 0000000000..501c78be1e
--- /dev/null
+++ b/tests/lean/run/inv_bug2.lean
@@ -0,0 +1,13 @@
+import data.vector
+open nat
+
+namespace vector
+ variables {A : Type} {n : nat}
+
+  protected definition destruct2 (v : vector A (succ (succ n))) {P : Π {n : nat}, vector A (succ n) → Type}
+                                 (H : Π {n : nat} (h : A) (t : vector A n), P (h :: t)) : P v :=
+  begin
+    cases v with (h', n', t'),
+    apply (H h' t')
+  end
+end vector