diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index a8c909cd8..a2cd0629d 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -700,6 +700,19 @@ class inversion_tac { } } + [[ noreturn ]] void throw_unify_eqs_failure(goal const & g) { + if (m_throw_tactic_exception) { + throw tactic_exception([=](formatter const & fmt) { + format r("invalid 'cases' tactic, unification failed"); + r += compose(line(), format("auxiliary goal at time of failure")); + r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt))); + return r; + }); + } else { + throw inversion_exception(); + } + } + // Remark: it also updates m_renames and m_imps optional unify_eqs(goal g, unsigned neqs) { if (neqs == 0) @@ -803,10 +816,19 @@ class inversion_tac { level eq_rec_lvl1 = sort_level(m_tc.ensure_type(deps_g_type).first); level eq_rec_lvl2 = sort_level(m_tc.ensure_type(A).first); expr tformer; - if (m_proof_irrel) + if (m_proof_irrel) { tformer = Fun(rhs, deps_g_type); - else + } else { + if (depends_on(lhs, rhs)) { + // tformer must be of the form + // fun x, fun (Heq : lhs = x, ...) + // If the lhs contains occurrences of rhs, then + // we would produce the following ill-typed tformer + // fun x, fun (Heq : lhs[x] = x, ...) + throw_unify_eqs_failure(g); + } tformer = Fun(rhs, Fun(Heq, deps_g_type)); + } expr eq_rec = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2}); eq_rec = mk_app(eq_rec, A, lhs, tformer); buffer new_hyps; @@ -877,16 +899,7 @@ class inversion_tac { return unify_eqs(new_g, neqs); } } - if (m_throw_tactic_exception) { - throw tactic_exception([=](formatter const & fmt) { - format r("invalid 'cases' tactic, unification failed"); - r += compose(line(), format("auxiliary goal at time of failure")); - r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt))); - return r; - }); - } else { - throw inversion_exception(); - } + throw_unify_eqs_failure(g); } auto unify_eqs(list const & gs, list> args, list imps) -> diff --git a/tests/lean/cases_failure.hlean b/tests/lean/cases_failure.hlean new file mode 100644 index 000000000..348b7a95e --- /dev/null +++ b/tests/lean/cases_failure.hlean @@ -0,0 +1,13 @@ +-- .hlean file +open eq + +inductive square {A : Type} {a₀₀ : A} + : Π{a₀₁ a₁₀ a₁₁ : A}, a₀₀ = a₀₁ → a₁₀ = a₁₁ → a₀₀ = a₁₀ → a₀₁ = a₁₁ → Type := +ids : square idp idp idp idp + +definition foo {A : Type} {x y z : A} {t : x = y} {b : z = y} {l : x = z} {r : y = y} + (s : square t b l r) : unit := +begin + cases s, + exact unit.star +end diff --git a/tests/lean/cases_failure.hlean.expected.out b/tests/lean/cases_failure.hlean.expected.out new file mode 100644 index 000000000..ced0aa679 --- /dev/null +++ b/tests/lean/cases_failure.hlean.expected.out @@ -0,0 +1,34 @@ +cases_failure.hlean:11:2: error:invalid 'cases' tactic, unification failed +auxiliary goal at time of failure + A : Type, + x y z : A, + b r t l : z = z, + s : square t b l r, + e_3 : z = z + ⊢ Π (e_4 : eq.rec t (refl z) = idp) (e_5 : eq.rec (eq.rec b (refl z)) e_3 = idp) (e_6 : eq.rec l (refl z) = idp) + (e_7 : eq.rec (eq.rec r (refl z)) e_3 = idp), + eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec s (refl z)) (refl z)) e_3) e_4) e_5) e_6) + e_7 = square.ids → + unit +proof state: +A : Type, +x y z : A, +t : x = y, +b : z = y, +l : x = z, +r : y = y, +s : square t b l r +⊢ unit +cases_failure.hlean:13:0: error: don't know how to synthesize placeholder +A : Type, +x y z : A, +t : x = y, +b : z = y, +l : x = z, +r : y = y, +s : square t b l r +⊢ unit +cases_failure.hlean:13:0: error: failed to add declaration 'foo' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + λ (A : Type) (x y z : A) (t : …) (b : …) (l : …) (r : …) (s : …), + ?M_1