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

feat(library/tactic/simp_lemmas): add both equational lemmas and the definition itself

Browse source
This commit is contained in:
Gabriel Ebner 2017-08-17 18:55:53 +02:00
parent 256ca9789f
commit 0d8e62ed40
2 changed files with 14 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -678,10 +678,6 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
expr const & e, expr const & h, unsigned priority) {
lean_assert(ctx.in_tmp_mode());
list<expr_pair> ceqvs = to_ceqvs(ctx, id, e, h);
if (is_nil(ceqvs)) {
report_failure(sstream() << "invalid simplification lemma '" << id << "' : " << e);
return s;
}
environment const & env = ctx.env();
simp_lemmas new_s = s;
for (expr_pair const & p : ceqvs) {
@ -779,16 +775,20 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons
/* Extended version. If cname is a definition with equational lemmas associated to it, then
add the equational lemmas. */
static simp_lemmas ext_add_core(type_context & ctx, simp_lemmas const & s, name const & cname, unsigned priority) {
simp_lemmas r = s;
// equational lemmas
buffer<name> eqn_lemmas;
get_ext_eqn_lemmas_for(ctx.env(), cname, eqn_lemmas);
if (eqn_lemmas.empty())
return add_core(ctx, s, cname, priority);
expr type = ctx.env().get(cname).get_type();
if (ctx.is_prop(type))
return add_core(ctx, s, cname, priority);
simp_lemmas r = s;
for (name const & eqn_lemma : eqn_lemmas)
r = add_core(ctx, r, eqn_lemma, priority);
// the definition itself
r = add_core(ctx, r, cname, priority);
if (is_eqp(r, s)) {
report_failure(sstream() << "invalid simplification lemma '" << cname << "'");
}
return r;
}

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

@ -119,6 +119,10 @@ public:
format pp_simp(formatter const & fmt) const;
format pp_congr(formatter const & fmt) const;
format pp(formatter const & fmt) const;
friend bool is_eqp(simp_lemmas const & a, simp_lemmas const & b) {
return is_eqp(a.m_sets, b.m_sets);
}
};
typedef unsigned simp_lemmas_token;