max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/simplify): store proof for refl lemmas and use them in simp

Browse source 
Before this commit, simp would not silently apply refl-lemmas, and use
reflexivity. This strategy produces compact proofs but may generate
performance problems. For example, the new test timeouts without this
commit.

I believe a similar performance problem is affecting the Certigrad
project developed by @dselsam.
This commit is contained in:
Leonardo de Moura 2017-06-21 16:21:11 -07:00
parent fd17a19a23
commit 9fcb3ae4b5
4 changed files with 32 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/library/tactic/simp_lemmas.cpp
View file

@ -38,6 +38,7 @@ struct simp_lemma_cell {
expr m_lhs;
expr m_rhs;
expr m_proof;
unsigned m_priority;
MK_LEAN_RC(); // Declare m_rc counter
void dealloc();
@ -45,38 +46,27 @@ struct simp_lemma_cell {
simp_lemma_cell(simp_lemma_kind k,
name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
unsigned priority):
expr const & proof, unsigned priority):
m_kind(k), m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances),
m_lhs(lhs), m_rhs(rhs), m_priority(priority), m_rc(0) {}
m_lhs(lhs), m_rhs(rhs), m_proof(proof), m_priority(priority), m_rc(0) {}
};
struct simp_lemma_with_proof_cell : public simp_lemma_cell {
expr m_proof;
simp_lemma_with_proof_cell(simp_lemma_kind k,
name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
expr const & proof, unsigned priority):
simp_lemma_cell(k, id, umetas, emetas, instances, lhs, rhs, priority),
m_proof(proof) {
}
};
struct regular_simp_lemma_cell : public simp_lemma_with_proof_cell {
struct regular_simp_lemma_cell : public simp_lemma_cell {
bool m_is_permutation;
regular_simp_lemma_cell(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
expr const & proof, bool is_perm, unsigned priority):
simp_lemma_with_proof_cell(simp_lemma_kind::Simp, id, umetas, emetas, instances, lhs, rhs, proof, priority),
simp_lemma_cell(simp_lemma_kind::Simp, id, umetas, emetas, instances, lhs, rhs, proof, priority),
m_is_permutation(is_perm) {
}
};
struct congr_lemma_cell : public simp_lemma_with_proof_cell {
struct congr_lemma_cell : public simp_lemma_cell {
list<expr> m_congr_hyps;
congr_lemma_cell(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
expr const & proof, list<expr> const & congr_hyps, unsigned priority):
simp_lemma_with_proof_cell(simp_lemma_kind::Congr, id, umetas, emetas, instances, lhs, rhs, proof, priority),
simp_lemma_cell(simp_lemma_kind::Congr, id, umetas, emetas, instances, lhs, rhs, proof, priority),
m_congr_hyps(congr_hyps) {
}
};
@ -84,7 +74,7 @@ struct congr_lemma_cell : public simp_lemma_with_proof_cell {
void simp_lemma_cell::dealloc() {
switch (m_kind) {
case simp_lemma_kind::Simp:
delete static_cast<simp_lemma_with_proof_cell*>(this);
delete static_cast<regular_simp_lemma_cell*>(this);
break;
case simp_lemma_kind::Congr:
delete static_cast<congr_lemma_cell*>(this);
@ -171,8 +161,7 @@ bool simp_lemma::is_permutation() const {
}
expr const & simp_lemma::get_proof() const {
lean_assert(kind() == simp_lemma_kind::Congr || kind() == simp_lemma_kind::Simp);
return static_cast<simp_lemma_with_proof_cell const *>(m_ptr)->m_proof;
return m_ptr->m_proof;
}
list<expr> const & simp_lemma::get_congr_hyps() const {
@ -221,10 +210,10 @@ simp_lemma mk_simp_lemma(name const & id, levels const & umetas, list<expr> cons
}
simp_lemma mk_rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
list<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
unsigned priority) {
return simp_lemma(new simp_lemma_cell(simp_lemma_kind::Refl, id, umetas, emetas,
instances, lhs, rhs, priority));
instances, lhs, rhs, proof, priority));
}
simp_lemma mk_congr_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
@ -751,6 +740,7 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
declaration const & d = env.get(cname);
levels ls = mk_tmp_levels_for(ctx, d);
expr type = instantiate_type_univ_params(d, ls);
expr proof = mk_constant(cname, ls);
if (is_rfl_lemma(env, cname)) {
buffer<expr> emetas;
buffer<bool> instances;
@ -759,15 +749,15 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
emetas.push_back(mvar);
instances.push_back(binding_info(type).is_inst_implicit());
type = instantiate(binding_body(type), mvar);
proof = mk_app(proof, mvar);
}
expr lhs, rhs;
lean_verify(is_eq(type, lhs, rhs));
simp_lemmas new_s = s;
new_s.insert(get_eq_name(), mk_rfl_lemma(cname, ls, to_list(emetas), to_list(instances),
lhs, rhs, priority));
lhs, rhs, proof, priority));
return new_s;
} else {
expr proof = mk_constant(cname, ls);
return add_core(ctx, s, cname, ls, type, proof, priority);
}
}

2
src/library/tactic/simp_lemmas.h
View file

@ -23,7 +23,7 @@ private:
list<bool> const & instances, expr const & lhs, expr const & rhs,
expr const & proof, bool is_perm, unsigned priority);
friend simp_lemma mk_rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,
list<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
unsigned priority);
friend simp_lemma mk_congr_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs,

8
src/library/tactic/simplify.cpp
View file

@ -591,12 +591,8 @@ simp_result simplify_core_fn::rewrite_core(expr const & e, simp_lemma const & sl
}
}
if (sl.is_refl()) {
return simp_result(new_rhs);
} else {
expr pf = tmp_ctx.instantiate_mvars(sl.get_proof());
return simp_result(new_rhs, pf);
}
expr pf = tmp_ctx.instantiate_mvars(sl.get_proof());
return simp_result(new_rhs, pf);
}
simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) {

15
tests/lean/run/simp_refl_lemma_perf_issue.lean Normal file
View file

@ -0,0 +1,15 @@
def foo (a : nat) (b : nat) := b
def g (a : nat) := foo (1000000000000 + 1) a
def f (a : nat) := foo (1 + 1000000000000) a
lemma foo_lemma (a b : nat) : foo b a = foo (1 + 1000000000000) a :=
rfl
lemma f_fold_lemma (a : nat) : foo (1 + 1000000000000) a = f a :=
rfl
lemma ex (a : nat) (p : nat → Prop) (h : p (f a)) : p (g a) :=
begin
simp only [g, foo_lemma, f_fold_lemma],
exact h,
end