From cf30d310247772c5fb3fcb96818f32eaf6eae7e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Sep 2016 17:39:55 -0700 Subject: [PATCH] fix(library/tactic/cases_tactic): missing case --- src/library/tactic/cases_tactic.cpp | 6 +++++- tests/lean/run/cases_bug3.lean | 4 ++++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/cases_bug3.lean diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 1ee38b21ab..828eb8d84d 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -324,7 +324,11 @@ struct cases_tactic_fn { lean_cases_trace(mvar, tout() << "converted heq => eq\n";); return unify_eqs(mvar2, num_eqs, updating, new_intros, subst); } else if (is_eq(H_type, A, lhs, rhs)) { - if (is_local(rhs) || is_local(lhs)) { + if (ctx.is_def_eq(lhs, rhs)) { + lean_cases_trace(mvar, tout() << "skip\n";); + expr mvar2 = clear(m_mctx, *mvar1, H); + return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, subst); + } else if (is_local(rhs) || is_local(lhs)) { lean_cases_trace(mvar, tout() << "substitute\n";); hsubstitution extra_subst; bool symm = !is_local(lhs) && is_local(rhs); diff --git a/tests/lean/run/cases_bug3.lean b/tests/lean/run/cases_bug3.lean new file mode 100644 index 0000000000..f4bfd428b5 --- /dev/null +++ b/tests/lean/run/cases_bug3.lean @@ -0,0 +1,4 @@ +set_option new_elaborator true + +theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a' +| a .a (heq.refl .a) := eq.refl a