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

fix(library/blast/congruence_closure): subsingleton propagation in the congruence closure module

Browse source 
We must normalize inferred type.
This commit is contained in:
Leonardo de Moura 2016-01-24 14:28:43 -08:00
parent 3d0ea4c9d1
commit 297ef10611
2 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/blast/congruence_closure.cpp
View file

@ -161,8 +161,8 @@ void congruence_closure::initialize() {
}
void congruence_closure::push_subsingleton_eq(expr const & a, expr const & b) {
expr A = infer_type(a);
expr B = infer_type(b);
expr A = normalize(infer_type(a));
expr B = normalize(infer_type(b));
if (is_def_eq(A, B)) {
// TODO(Leo): to improve performance we can create the following proof lazily
bool heq_proof = false;
@ -192,7 +192,7 @@ void congruence_closure::check_new_subsingleton_eq(expr const & old_root, expr c
void congruence_closure::process_subsingleton_elem(expr const & e) {
if (!g_propagate_subsingletons)
return;
expr type = infer_type(e);
expr type = normalize(infer_type(e));
optional<expr> ss = mk_subsingleton_instance(type);
if (!ss)
return; /* type is not a subsingleton */

19
tests/lean/run/blast_cc_subsingleton_normalization_issue.lean Normal file
View file

@ -0,0 +1,19 @@
import data.real
open real
namespace safe
definition pos (x : ℝ) := x > 0
constants (safe_log : Π (x : ℝ), pos x → ℝ)
lemma pos_add {x y : ℝ} : pos x → pos y → pos (x + y) := sorry
lemma pos_mul {x y : ℝ} : pos x → pos y → pos (x * y) := sorry
set_option blast.strategy "cc"
example (x y z w : ℝ)
(x_pos : pos x) (y_pos : pos y) (z_pos : pos z) (w_pos : pos w) :
x * y = z + w → @safe_log (z + w) (pos_add z_pos w_pos) = @safe_log (x * y) (pos_mul x_pos y_pos) :=
by blast -- fails
end safe