From 5efadb09ccdf90df1d9090735eebbe63b2688823 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Dec 2014 15:19:25 -0800
Subject: [PATCH] feat(library/tactic/inversion_tactic): improve 'cases' tactic
 for HoTT library

This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.

The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
---
 src/library/tactic/inversion_tactic.cpp | 22 ++++++++++++++--------
 tests/lean/hott/cases_eq.hlean          | 21 +++++++++++++++++++++
 2 files changed, 35 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/hott/cases_eq.hlean

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index a2e9fac022..d42817c4bf 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -327,7 +327,7 @@ class inversion_tac {
     // when A is a hset
     // and then invoke intro_next_eq recursively.
     //
-    // \remark \c type is the type of \c g after whnf
+    // \remark \c type is the type of \c g after some normalization
     goal intro_next_eq_rec(goal const & g, expr const & type) {
         lean_assert(is_pi(type));
         buffer<expr> hyps;
@@ -365,10 +365,9 @@ class inversion_tac {
     // The idea is to reduce it to
     //        Ctx, H : a = b |- R
     // This method is only used if the environment has a proof irrelevant Prop.
-    //
-    // \remark \c type is the type of \c g after whnf
-    goal intro_next_heq(goal const & g, expr const & type) {
+    goal intro_next_heq(goal const & g) {
         lean_assert(m_proof_irrel);
+        expr const & type   = g.get_type();
         expr eq             = binding_domain(type);
         lean_assert(const_name(get_app_fn(eq)) == "heq");
         buffer<expr> args;
@@ -399,7 +398,7 @@ class inversion_tac {
     // The idea is to reduce it to
     //        Ctx, H : a = b |- R
     //
-    // \remark \c type is the type of \c g after whnf
+    // \remark \c type is the type of \c g after some normalization
     goal intro_next_eq_simple(goal const & g, expr const & type) {
         expr eq            = binding_domain(type);
         lean_assert(const_name(get_app_fn(eq)) == "eq");
@@ -416,7 +415,7 @@ class inversion_tac {
     }
 
     goal intro_next_eq(goal const & g) {
-        expr const & type  = m_tc->whnf(g.get_type()).first;
+        expr type          = g.get_type();
         if (!is_pi(type))
             throw_ill_formed_goal();
         expr eq            = binding_domain(type);
@@ -425,13 +424,20 @@ class inversion_tac {
             throw_ill_formed_goal();
         if (const_name(eq_fn) == "eq") {
             expr const & lhs = app_arg(app_fn(eq));
-            if (!m_proof_irrel && is_eq_rec(lhs)) {
+            expr const & rhs = app_arg(eq);
+            expr new_lhs     = m_tc->whnf(lhs).first;
+            expr new_rhs     = m_tc->whnf(rhs).first;
+            if (lhs != new_lhs || rhs != new_rhs) {
+                eq   = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs);
+                type = update_binding(type, eq, binding_body(type));
+            }
+            if (!m_proof_irrel && is_eq_rec(new_lhs)) {
                 return intro_next_eq_rec(g, type);
             } else {
                 return intro_next_eq_simple(g, type);
             }
         } else if (m_proof_irrel && const_name(eq_fn) == "heq") {
-            return intro_next_heq(g, type);
+            return intro_next_heq(g);
         } else {
             throw_ill_formed_goal();
         }
diff --git a/tests/lean/hott/cases_eq.hlean b/tests/lean/hott/cases_eq.hlean
new file mode 100644
index 0000000000..f1f19806b5
--- /dev/null
+++ b/tests/lean/hott/cases_eq.hlean
@@ -0,0 +1,21 @@
+open eq.ops
+
+theorem trans {A : Type} {a b c : A} (h₁ : a = b) (h₂ : b = c) : a = c :=
+begin
+  cases h₁, cases h₂, apply rfl
+end
+
+theorem symm {A : Type} {a b : A} (h₁ : a = b) : b = a :=
+begin
+  cases h₁, apply rfl
+end
+
+theorem congr {A B : Type} (f : A → B) {a₁ a₂ : A} (h : a₁ = a₂) : f a₁ = f a₂ :=
+begin
+  cases h, apply rfl
+end
+
+definition inv_pV_2 {A : Type} {x y z : A} (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ :=
+begin
+  cases p, cases q, apply rfl
+end