michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic/inversion_tactic): bug in simpler case (hypotheses were being lost)

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-23 16:10:49 -08:00
parent 7adecaf494
commit 787fed95aa
2 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/tactic/inversion_tactic.cpp
View file

@ -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. \remark This method assumes the indices j are local constants, and only h and j may depend on j.
*/ */
std::pair<list<goal>, list<implementation_list>> apply_cases_on(goal const & g, implementation_list const & imps) { std::pair<list<goal>, list<implementation_list>> apply_cases_on(goal const & g, implementation_list const & imps, bool has_indep_indices) {
buffer<expr> hyps; buffer<expr> hyps;
g.get_hyps(hyps); g.get_hyps(hyps);
expr const & h = hyps.back(); expr const & h = hyps.back();
@ -390,7 +390,11 @@ class inversion_tac {
get_intro_rule_names(m_env, I_name, intro_names); get_intro_rule_names(m_env, I_name, intro_names);
lean_assert(m_nminors == intro_names.size()); lean_assert(m_nminors == intro_names.size());
buffer<expr> new_hyps; buffer<expr> 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 // add a subgoal for each minor premise of cases_on
expr cases_on_type = whnf(infer_type(cases_on)); expr cases_on_type = whnf(infer_type(cases_on));
buffer<goal> new_goals; buffer<goal> new_goals;
@ -893,7 +897,7 @@ public:
if (has_indep_indices(g, h, h_type)) { if (has_indep_indices(g, h, h_type)) {
buffer<expr> deps; buffer<expr> deps;
goal g1 = generalize_dependecies(g, h, 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<goal> gs2 = gs_imps_pair.first; list<goal> gs2 = gs_imps_pair.first;
list<implementation_list> new_imps = gs_imps_pair.second; list<implementation_list> new_imps = gs_imps_pair.second;
auto gs_args_pair = intros_minors_args(gs2); auto gs_args_pair = intros_minors_args(gs2);
@ -905,7 +909,7 @@ public:
return optional<result>(result(gs4, args, new_imps, rs, m_ngen, m_subst)); return optional<result>(result(gs4, args, new_imps, rs, m_ngen, m_subst));
} else { } else {
goal g1 = generalize_indices(g, h, h_type); 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<goal> gs2 = gs_imps_pair.first; list<goal> gs2 = gs_imps_pair.first;
list<implementation_list> new_imps = gs_imps_pair.second; list<implementation_list> new_imps = gs_imps_pair.second;
auto gs_args_pair = intros_minors_args(gs2); auto gs_args_pair = intros_minors_args(gs2);

14
tests/lean/hott/def_bug1.hlean Normal file
View file

@ -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)