fix(library/blast/discr_tree): bug in the discrimination tree module
This commit is contained in:
parent
3c22a9d4e1
commit
27eea05da9
2 changed files with 20 additions and 2 deletions
|
@ -171,7 +171,7 @@ auto discr_tree::insert_erase_app(node && n, bool is_root, expr const & e, buffe
|
||||||
if (is_constant(fn) || is_local(fn)) {
|
if (is_constant(fn) || is_local(fn)) {
|
||||||
if (!is_root)
|
if (!is_root)
|
||||||
todo.push_back(mk_pair(*g_delimiter, false));
|
todo.push_back(mk_pair(*g_delimiter, false));
|
||||||
fun_info info = get_fun_info(fn);
|
fun_info info = get_fun_info(fn, args.size());
|
||||||
buffer<param_info> pinfos;
|
buffer<param_info> pinfos;
|
||||||
to_buffer(info.get_params_info(), pinfos);
|
to_buffer(info.get_params_info(), pinfos);
|
||||||
lean_assert(pinfos.size() == args.size());
|
lean_assert(pinfos.size() == args.size());
|
||||||
|
@ -281,7 +281,7 @@ bool discr_tree::find_app(node const & n, expr const & e, list<pair<expr, bool>>
|
||||||
buffer<expr> args;
|
buffer<expr> args;
|
||||||
expr const & f = get_app_args(e, args);
|
expr const & f = get_app_args(e, args);
|
||||||
if (is_constant(f) || is_local(f)) {
|
if (is_constant(f) || is_local(f)) {
|
||||||
fun_info info = get_fun_info(f);
|
fun_info info = get_fun_info(f, args.size());
|
||||||
buffer<param_info> pinfos;
|
buffer<param_info> pinfos;
|
||||||
to_buffer(info.get_params_info(), pinfos);
|
to_buffer(info.get_params_info(), pinfos);
|
||||||
lean_assert(pinfos.size() == args.size());
|
lean_assert(pinfos.size() == args.size());
|
||||||
|
|
18
tests/lean/run/blast_discr_tree_bug.lean
Normal file
18
tests/lean/run/blast_discr_tree_bug.lean
Normal file
|
@ -0,0 +1,18 @@
|
||||||
|
open subtype nat
|
||||||
|
|
||||||
|
constant f : Π (a : nat), {b : nat | b > a} → nat
|
||||||
|
|
||||||
|
definition f_flat (a : nat) (b : nat) (p : b > a) : nat :=
|
||||||
|
f a (tag b p)
|
||||||
|
|
||||||
|
definition greater [reducible] (a : nat) := {b : nat | b > a}
|
||||||
|
set_option blast.recursion.structure true
|
||||||
|
|
||||||
|
definition f_flat_def [simp] (a : nat) (b : nat) (p : b > a) : f a (tag b p) = f_flat a b p :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
definition has_property_tag [simp] {A : Type} {p : A → Prop} (a : A) (h : p a) : has_property (tag a h) = h :=
|
||||||
|
rfl
|
||||||
|
|
||||||
|
lemma to_f_flat : ∀ (a : nat) (b : greater a), f a b = f_flat a (elt_of b) (has_property b) :=
|
||||||
|
by rec_simp
|
Loading…
Reference in a new issue