feat(library/blast/subst): avoid unnecessary proof step

This commit is contained in:
Leonardo de Moura 2015-11-13 16:26:28 -08:00
parent 3849aff674
commit 29d472788f
3 changed files with 22 additions and 5 deletions

View file

@ -65,6 +65,8 @@ public:
m_buffer.push_back(h);
}
}
unsigned size() const { return m_buffer.size(); }
bool empty() const { return m_buffer.empty(); }
hypothesis_idx_buffer const & as_buffer() const {
return m_buffer;
}

View file

@ -61,12 +61,20 @@ bool subst_core(hypothesis_idx hidx) {
expr target = s.get_target();
expr new_target = abstract(target, h->get_self());
bool dep = !closed(new_target);
if (dep)
bool skip = to_revert.empty();
if (dep) {
skip = false;
new_target = instantiate(new_target, b.mk_eq_refl(lhs));
new_target = instantiate(abstract(new_target, rhs), lhs);
}
new_target = abstract(new_target, rhs);
if (!closed(new_target))
skip = false;
if (!skip) {
new_target = instantiate(new_target, lhs);
s.push_proof_step(new subst_proof_step_cell(target, h->get_self(), rhs, dep));
s.set_target(new_target);
lean_verify(intros_action(num));
}
lean_verify(s.del_hypothesis(hidx));
lean_verify(s.del_hypothesis(href_index(rhs)));
return true;

View file

@ -0,0 +1,7 @@
set_option blast.init_depth 10
lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=
by blast
reveal lemma1
print lemma1