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

fix(library/blast/forward/ematch): bug in the ematching procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-31 21:26:44 -08:00
parent 54f2c0f254
commit 712e19e22a
2 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/group.lean
View file

@ -200,7 +200,6 @@ section group
by inst_simp
theorem mul_inv [simp] (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
assert a * a⁻¹ = 1, by inst_simp, -- why do we need it?
inv_eq_of_mul_eq_one (by inst_simp)
theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
@ -266,7 +265,6 @@ section group
by inst_simp
lemma conj_one [simp] (g : A) : g ∘c 1 = 1 :=
assert g * g⁻¹ = 1, by inst_simp, -- why do we need it?
by inst_simp
lemma conj_inv_cancel [simp] (g : A) : ∀ a, g⁻¹ ∘c g ∘c a = a :=

16
src/library/blast/forward/ematch.cpp
View file

@ -274,10 +274,22 @@ struct ematch_fn {
}
bool is_eqv(name const & R, expr const & p, expr const & t) {
if (!has_expr_metavar(p))
if (!has_expr_metavar(p)) {
return m_cc.is_eqv(R, p, t) || m_ctx->is_def_eq(p, t);
else
} else if (is_meta(p)) {
expr const & m = get_app_fn(p);
if (!m_ctx->is_assigned(m)) {
return m_ctx->is_def_eq(p, t);
} else {
expr new_p = m_ctx->instantiate_uvars_mvars(p);
if (!has_expr_metavar(new_p))
return m_cc.is_eqv(R, new_p, t) || m_ctx->is_def_eq(new_p, t);
else
return m_ctx->is_def_eq(new_p, t);
}
} else {
return m_ctx->is_def_eq(p, t);
}
}
bool match_args(state & s, name const & R, buffer<expr> const & p_args, expr const & t) {