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

fix(library/tactic/inversion_tactic.cpp): remove unnecessary hypothesis in HoTT mode

Browse source 
partial solution for #468
This commit is contained in:
Leonardo de Moura 2015-03-11 19:23:41 -07:00
parent 737faecc65
commit ebdda67812
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -742,7 +742,7 @@ class inversion_tac {
if (const_name(lhs_fn) == const_name(rhs_fn)) {
// injectivity transition
expr new_type = binding_domain(whnf(infer_type(no_confusion)));
if (m_proof_irrel)
if (m_proof_irrel || !depends_on(g_type, hyps.back()))
hyps.pop_back(); // remove processed equality
expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
expr new_meta = mk_app(new_mvar, hyps);
@ -835,7 +835,7 @@ class inversion_tac {
}
} else if (is_local(lhs)) {
// flip equation and reduce to previous case
if (m_proof_irrel)
if (m_proof_irrel || !depends_on(g_type, hyps.back()))
hyps.pop_back(); // remove processed equality
expr symm_eq = mk_eq(rhs, lhs).first;
expr new_type = mk_arrow(symm_eq, g_type);