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

fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-11 15:09:34 -08:00
parent 902a551048
commit f6889951c6
3 changed files with 20 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/inductive_cmd.cpp
View file

@ -654,9 +654,9 @@ struct inductive_cmd_fn {
save_def_info(name(n, "cases_on"), pos);
if (has_eq && has_heq) {
if (optional<environment> new_env = mk_no_confusion(env, inductive_decl_name(d))) {
env = *new_env;
save_def_info(name{n, "no_confusion_type"}, pos);
// save_def_info(name(n, "no_confusion"), pos);
env = *new_env;
save_def_info(name{n, "no_confusion_type"}, pos);
save_def_info(name(n, "no_confusion"), pos);
}
}
// if (has_prod) {

9
src/library/definitional/cases_on.cpp
View file

@ -125,7 +125,7 @@ environment mk_cases_on(environment const & env, name const & n) {
for (unsigned i = 0; i < num_idx_major; i++)
cases_on_params.push_back(rec_params[num_params + num_types + num_minors + i]);
// Ad minor premises to rec_params and rec_args
// Add minor premises to rec_params and rec_args
i = num_params + num_types;
for (auto const & d : idecls) {
bool is_main = inductive::inductive_decl_name(d) == n;
@ -139,8 +139,11 @@ environment mk_cases_on(environment const & env, name const & n) {
while (is_pi(minor_type)) {
expr local = mk_local(ngen.next(), binding_name(minor_type), binding_domain(minor_type),
binding_info(minor_type));
if (is_type_former_arg(C_names, binding_domain(minor_type))) {
if (mlocal_name(get_app_fn(binding_domain(minor_type))) == C_main) {
expr curr_type = mlocal_type(local);
while (is_pi(curr_type))
curr_type = binding_body(curr_type);
if (is_type_former_arg(C_names, curr_type)) {
if (mlocal_name(get_app_fn(curr_type)) == C_main) {
minor_params.push_back(local);
} else {
minor_params.push_back(update_mlocal(local, *unit));

11
tests/lean/run/ho.lean Normal file
View file

@ -0,0 +1,11 @@
import data.nat
inductive star : Type₁ :=
z : star,
s : (nat → star) → star
check @star.rec
check @star.cases_on
example (f : nat → star) : ¬ star.z = star.s f :=
assume H, star.no_confusion H