From 787fed95aa8302939cb1a5317813b801c879e87b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Feb 2015 16:10:49 -0800 Subject: [PATCH] fix(library/tactic/inversion_tactic): bug in simpler case (hypotheses were being lost) --- src/library/tactic/inversion_tactic.cpp | 12 ++++++++---- tests/lean/hott/def_bug1.hlean | 14 ++++++++++++++ 2 files changed, 22 insertions(+), 4 deletions(-) create mode 100644 tests/lean/hott/def_bug1.hlean diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 219fbea9a..a82715468 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -358,7 +358,7 @@ class inversion_tac { \remark This method assumes the indices j are local constants, and only h and j may depend on j. */ - std::pair, list> apply_cases_on(goal const & g, implementation_list const & imps) { + std::pair, list> apply_cases_on(goal const & g, implementation_list const & imps, bool has_indep_indices) { buffer hyps; g.get_hyps(hyps); expr const & h = hyps.back(); @@ -390,7 +390,11 @@ class inversion_tac { get_intro_rule_names(m_env, I_name, intro_names); lean_assert(m_nminors == intro_names.size()); buffer new_hyps; - new_hyps.append(hyps.size() - m_nindices - 1, hyps.data()); + if (has_indep_indices) + new_hyps.append(hyps.size() - 1, hyps.data()); + else + new_hyps.append(hyps.size() - m_nindices - 1, hyps.data()); + // add a subgoal for each minor premise of cases_on expr cases_on_type = whnf(infer_type(cases_on)); buffer new_goals; @@ -893,7 +897,7 @@ public: if (has_indep_indices(g, h, h_type)) { buffer deps; goal g1 = generalize_dependecies(g, h, deps); - auto gs_imps_pair = apply_cases_on(g1, imps); + auto gs_imps_pair = apply_cases_on(g1, imps, true); list gs2 = gs_imps_pair.first; list new_imps = gs_imps_pair.second; auto gs_args_pair = intros_minors_args(gs2); @@ -905,7 +909,7 @@ public: return optional(result(gs4, args, new_imps, rs, m_ngen, m_subst)); } else { goal g1 = generalize_indices(g, h, h_type); - auto gs_imps_pair = apply_cases_on(g1, imps); + auto gs_imps_pair = apply_cases_on(g1, imps, false); list gs2 = gs_imps_pair.first; list new_imps = gs_imps_pair.second; auto gs_args_pair = intros_minors_args(gs2); diff --git a/tests/lean/hott/def_bug1.hlean b/tests/lean/hott/def_bug1.hlean new file mode 100644 index 000000000..90602b41c --- /dev/null +++ b/tests/lean/hott/def_bug1.hlean @@ -0,0 +1,14 @@ +open eq eq.ops + +variable {A : Type} + +definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z, +trans (refl a) (refl a) := refl a + +set_option pp.purify_locals false + +definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q, +con_inv_cancel_left (refl a) (refl a) := refl (refl a) + +definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q, +inv_con_cancel_left (refl a) (refl a) := refl (refl a)