fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library

src/library/tactic/inversion_tactic.cpp

@@ -35,7 +35,7 @@ optional<expr> apply_eq_rec_eq(type_checker & tc, io_state const & ios, list<exp
     if (args.size() != 6)
         return none_expr();
     expr const & p = args[5];
-    if (!is_local(p) || !is_eq_a_a(mlocal_type(p)))
+    if (!is_local(p) || !is_eq_a_a(tc, mlocal_type(p)))
         return none_expr();
     expr const & A = args[0];
     auto is_hset_A = mk_hset_instance(tc, ios, ctx, A);

src/library/util.cpp

@@ -342,6 +342,17 @@ bool is_eq_a_a(expr const & e) {
     return args.size() == 3 && args[1] == args[2];
 }
 
+bool is_eq_a_a(type_checker & tc, expr const & e) {
+    if (!is_eq(e))
+        return false;
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() != 3)
+        return false;
+    pair<bool, constraint_seq> d = tc.is_def_eq(args[1], args[2]);
+    return d.first && !d.second;
+}
+
 void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs) {
     lean_assert(t.size() == s.size());
     lean_assert(std::all_of(s.begin(), s.end(), is_local));

src/library/util.h

@@ -101,7 +101,10 @@ expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
 expr mk_refl(type_checker & tc, expr const & a);
 bool is_eq_rec(expr const & e);
 bool is_eq(expr const & e);
+/** \brief Return true iff \c e is of the form (eq A a a) */
 bool is_eq_a_a(expr const & e);
+/** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
+bool is_eq_a_a(type_checker & tc, expr const & e);
 
 /** \brief Create a telescope equality for HoTT library.
     This procedure assumes eq supports dependent elimination.

tests/lean/hott/inv_bug.hlean

@@ -0,0 +1,24 @@
+open nat
+open eq.ops
+
+inductive even : nat → Type :=
+even_zero        : even zero,
+even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
+with odd : nat → Type :=
+odd_succ_of_even : ∀ {a}, even a → odd (succ a)
+
+example : even 1 → empty :=
+begin
+  intro He1,
+  cases He1 with (a, Ho0),
+  cases Ho0
+end
+
+example : even 3 → empty :=
+begin
+  intro He3,
+  cases He3 with (a, Ho2),
+  cases Ho2 with (a, He1),
+  cases He1 with (a, Ho0),
+  cases Ho0
+end